Equivalences and sets

In this file we provide lemmas linking equivalences to sets.

Some notable definitions are:

• Equiv.ofInjective: an injective function is (noncomputably) equivalent to its range.
• Equiv.setCongr: two equal sets are equivalent as types.
• Equiv.Set.union: a disjoint union of sets is equivalent to their Sum.

This file is separate from Equiv/Basic such that we do not require the full lattice structure on sets before defining what an equivalence is.

@[simp]

theorem EquivLike.range_eq_univ {α : Type u_1} {β : Type u_2} {E : Type u_3} [EquivLike E α β] (e : E) : Set.range ⇑e = Set.univ

theorem Equiv.range_eq_univ {α : Type u_1} {β : Type u_2} (e : α ≃ β) : Set.range ⇑e = _root_.Set.univ

theorem Equiv.image_symm_eq_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set β) : ⇑e.symm '' s = ⇑e ⁻¹' s

theorem Equiv.image_eq_preimage_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) : ⇑e '' s = ⇑e.symm ⁻¹' s

@[deprecated Equiv.image_eq_preimage_symm (since := "2025-11-05")]

theorem Equiv.image_eq_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) : ⇑e '' s = ⇑e.symm ⁻¹' s

Alias of Equiv.image_eq_preimage_symm.

@[simp]

theorem Set.mem_image_equiv {α : Type u_3} {β : Type u_4} {S : Set α} {f : α ≃ β} {x : β} : x ∈ ⇑f '' S ↔ f.symm x ∈ S

@[deprecated Equiv.image_eq_preimage_symm (since := "2025-10-31")]

theorem Set.image_equiv_eq_preimage_symm {α : Type u_3} {β : Type u_4} (S : Set α) (f : α ≃ β) : ⇑f '' S = ⇑f.symm ⁻¹' S

@[deprecated Equiv.image_symm_eq_preimage (since := "2025-10-31")]

theorem Set.preimage_equiv_eq_image_symm {α : Type u_3} {β : Type u_4} (S : Set α) (f : β ≃ α) : ⇑f ⁻¹' S = ⇑f.symm '' S

@[simp]

theorem Equiv.symm_image_subset {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (t : Set β) : ⇑e.symm '' t ⊆ s ↔ t ⊆ ⇑e '' s

@[simp]

theorem Equiv.subset_symm_image {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (t : Set β) : s ⊆ ⇑e.symm '' t ↔ ⇑e '' s ⊆ t

@[simp]

theorem Equiv.symm_image_image {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) : ⇑e.symm '' (⇑e '' s) = s

theorem Equiv.eq_image_iff_symm_image_eq {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (t : Set β) : t = ⇑e '' s ↔ ⇑e.symm '' t = s

@[simp]

theorem Equiv.image_symm_image {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set β) : ⇑e '' (⇑e.symm '' s) = s

@[simp]

theorem Equiv.image_preimage {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set β) : ⇑e '' (⇑e ⁻¹' s) = s

@[simp]

theorem Equiv.preimage_image {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) : ⇑e ⁻¹' (⇑e '' s) = s

theorem Equiv.image_compl {α : Type u_3} {β : Type u_4} (f : α ≃ β) (s : Set α) : ⇑f '' sᶜ = (⇑f '' s)ᶜ

@[simp]

theorem Equiv.symm_preimage_preimage {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set β) : ⇑e.symm ⁻¹' (⇑e ⁻¹' s) = s

@[simp]

theorem Equiv.preimage_symm_preimage {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) : ⇑e ⁻¹' (⇑e.symm ⁻¹' s) = s

theorem Equiv.preimage_subset {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s t : Set β) : ⇑e ⁻¹' s ⊆ ⇑e ⁻¹' t ↔ s ⊆ t

theorem Equiv.image_subset {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s t : Set α) : ⇑e '' s ⊆ ⇑e '' t ↔ s ⊆ t

@[simp]

theorem Equiv.image_eq_iff_eq {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s t : Set α) : ⇑e '' s = ⇑e '' t ↔ s = t

theorem Equiv.preimage_eq_iff_eq_image {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set β) (t : Set α) : ⇑e ⁻¹' s = t ↔ s = ⇑e '' t

theorem Equiv.eq_preimage_iff_image_eq {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (t : Set β) : s = ⇑e ⁻¹' t ↔ ⇑e '' s = t

theorem Equiv.setOf_apply_symm_eq_image_setOf {α : Type u_3} {β : Type u_4} (e : α ≃ β) (p : α → Prop) : {b : β | p (e.symm b)} = ⇑e '' {a : α | p a}

@[simp]

theorem Equiv.prod_assoc_preimage {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ} : ⇑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

@[simp]

theorem Equiv.prod_assoc_symm_preimage {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ} : ⇑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

theorem Equiv.prod_assoc_image {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ} : ⇑(prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

theorem Equiv.prod_assoc_symm_image {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ} : ⇑(prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

def Equiv.setProdEquivSigma {α : Type u_3} {β : Type u_4} (s : Set (α × β)) : ↑s ≃ (x : α) × ↑{y : β | (x, y) ∈ s}

A set s in α × β is equivalent to the sigma-type Σ x, {y | (x, y) ∈ s}.

def Equiv.setCongr {α : Type u_3} {s t : Set α} (h : s = t) : ↑s ≃ ↑t

The subtypes corresponding to equal sets are equivalent.

@[simp]

theorem Equiv.setCongr_symm_apply {α : Type u_3} {s t : Set α} (h : s = t) (b : { b : α // (fun (x : α) => x ∈ t) b }) : (setCongr h).symm b = ⟨↑b, ⋯⟩

@[simp]

theorem Equiv.setCongr_apply {α : Type u_3} {s t : Set α} (h : s = t) (a : { a : α // (fun (x : α) => x ∈ s) a }) : (setCongr h) a = ⟨↑a, ⋯⟩

def Equiv.image {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) : ↑s ≃ ↑(⇑e '' s)

A set is equivalent to its image under an equivalence.

@[simp]

theorem Equiv.image_symm_apply_coe {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (y : ↑(⇑e '' s)) : ↑((e.image s).symm y) = e.symm ↑y

@[simp]

theorem Equiv.image_apply_coe {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (x : ↑s) : ↑((e.image s) x) = e ↑x

theorem Equiv.image_monotone {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {e : α ≃ β} (s : Set α) (hs : Monotone ⇑e) : Monotone ⇑(e.image s)

theorem Equiv.image_antitone {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {e : α ≃ β} (s : Set α) (hs : Antitone ⇑e) : Antitone ⇑(e.image s)

theorem Equiv.image_strictMono {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {e : α ≃ β} (s : Set α) (hs : StrictMono ⇑e) : StrictMono ⇑(e.image s)

theorem Equiv.image_strictAnti {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {e : α ≃ β} (s : Set α) (hs : StrictAnti ⇑e) : StrictAnti ⇑(e.image s)

def Equiv.Set.univ (α : Type u_3) : ↑_root_.Set.univ ≃ α

univ α is equivalent to α.

@[simp]

theorem Equiv.Set.univ_apply (α : Type u_3) (self : { x : α // x ∈ _root_.Set.univ }) : (Set.univ α) self = ↑self

@[simp]

theorem Equiv.Set.univ_symm_apply (α : Type u_3) (a : α) : (Set.univ α).symm a = ⟨a, trivial⟩

def Equiv.Set.empty (α : Type u_3) : ↑∅ ≃ Empty

An empty set is equivalent to the Empty type.

def Equiv.Set.pempty (α : Type u_3) : ↑∅ ≃ PEmpty.{u_4}

An empty set is equivalent to a PEmpty type.

def Equiv.Set.union' {α : Type u_3} {s t : Set α} (p : α → Prop) [DecidablePred p] (hs : ∀ x ∈ s, p x) (ht : ∀ x ∈ t, ¬p x) : ↑(s ∪ t) ≃ ↑s ⊕ ↑t

If sets s and t are separated by a decidable predicate, then s ∪ t is equivalent to s ⊕ t.

def Equiv.Set.union {α : Type u_3} {s t : Set α} [DecidablePred fun (x : α) => x ∈ s] (H : Disjoint s t) : ↑(s ∪ t) ≃ ↑s ⊕ ↑t

If sets s and t are disjoint, then s ∪ t is equivalent to s ⊕ t.

theorem Equiv.Set.union_apply_left {α : Type u_3} {s t : Set α} [DecidablePred fun (x : α) => x ∈ s] (H : Disjoint s t) {a : ↑(s ∪ t)} (ha : ↑a ∈ s) : (Set.union H) a = Sum.inl ⟨↑a, ha⟩

theorem Equiv.Set.union_apply_right {α : Type u_3} {s t : Set α} [DecidablePred fun (x : α) => x ∈ s] (H : Disjoint s t) {a : ↑(s ∪ t)} (ha : ↑a ∈ t) : (Set.union H) a = Sum.inr ⟨↑a, ha⟩

@[simp]

theorem Equiv.Set.union_symm_apply_left {α : Type u_3} {s t : Set α} [DecidablePred fun (x : α) => x ∈ s] (H : Disjoint s t) (a : ↑s) : (Set.union H).symm (Sum.inl a) = ⟨↑a, ⋯⟩

@[simp]

theorem Equiv.Set.union_symm_apply_right {α : Type u_3} {s t : Set α} [DecidablePred fun (x : α) => x ∈ s] (H : Disjoint s t) (a : ↑t) : (Set.union H).symm (Sum.inr a) = ⟨↑a, ⋯⟩

def Equiv.Set.singleton {α : Type u_3} (a : α) : ↑{a} ≃ PUnit.{u}

A singleton set is equivalent to a PUnit type.

theorem Equiv.Set.Equiv.strictMono_setCongr {α : Type u_3} [Preorder α] {S T : Set α} (h : S = T) : StrictMono ⇑(setCongr h)

def Equiv.Set.insert {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {a : α} (H : a ∉ s) : ↑(insert a s) ≃ ↑s ⊕ PUnit.{u + 1}

If a ∉ s, then insert a s is equivalent to s ⊕ PUnit.

@[simp]

theorem Equiv.Set.insert_symm_apply_inl {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {a : α} (H : a ∉ s) (b : ↑s) : (Set.insert H).symm (Sum.inl b) = ⟨↑b, ⋯⟩

@[simp]

theorem Equiv.Set.insert_symm_apply_inr {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {a : α} (H : a ∉ s) (b : PUnit.{u + 1}) : (Set.insert H).symm (Sum.inr b) = ⟨a, ⋯⟩

@[simp]

theorem Equiv.Set.insert_apply_left {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {a : α} (H : a ∉ s) : (Set.insert H) ⟨a, ⋯⟩ = Sum.inr PUnit.unit

@[simp]

theorem Equiv.Set.insert_apply_right {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {a : α} (H : a ∉ s) (b : ↑s) : (Set.insert H) ⟨↑b, ⋯⟩ = Sum.inl b

def Equiv.Set.sumCompl {α : Type u_3} (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : ↑s ⊕ ↑sᶜ ≃ α

If s : Set α is a set with decidable membership, then s ⊕ sᶜ is equivalent to α.

See also Equiv.sumCompl.

@[simp]

theorem Equiv.Set.sumCompl_apply_inl {α : Type u} (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (x : ↑s) : (Set.sumCompl s) (Sum.inl x) = ↑x

@[simp]

theorem Equiv.Set.sumCompl_apply_inr {α : Type u} (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (x : ↑sᶜ) : (Set.sumCompl s) (Sum.inr x) = ↑x

theorem Equiv.Set.sumCompl_symm_apply_of_mem {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {x : α} (hx : x ∈ s) : (Set.sumCompl s).symm x = Sum.inl ⟨x, hx⟩

theorem Equiv.Set.sumCompl_symm_apply_of_notMem {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {x : α} (hx : x ∉ s) : (Set.sumCompl s).symm x = Sum.inr ⟨x, hx⟩

@[simp]

theorem Equiv.Set.sumCompl_symm_apply {α : Type u_3} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (x : ↑s) : (Set.sumCompl s).symm ↑x = Sum.inl x

@[simp]

theorem Equiv.Set.sumCompl_symm_apply_compl {α : Type u_3} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (x : ↑sᶜ) : (Set.sumCompl s).symm ↑x = Sum.inr x

def Equiv.Set.sumDiffSubset {α : Type u_3} {s t : Set α} (h : s ⊆ t) [DecidablePred fun (x : α) => x ∈ s] : ↑s ⊕ ↑(t \ s) ≃ ↑t

sumDiffSubset s t is the natural equivalence between s ⊕ (t \ s) and t, where s and t are two sets.

@[simp]

theorem Equiv.Set.sumDiffSubset_apply_inl {α : Type u_3} {s t : Set α} (h : s ⊆ t) [DecidablePred fun (x : α) => x ∈ s] (x : ↑s) : (Set.sumDiffSubset h) (Sum.inl x) = Set.inclusion h x

@[simp]

theorem Equiv.Set.sumDiffSubset_apply_inr {α : Type u_3} {s t : Set α} (h : s ⊆ t) [DecidablePred fun (x : α) => x ∈ s] (x : ↑(t \ s)) : (Set.sumDiffSubset h) (Sum.inr x) = Set.inclusion ⋯ x

theorem Equiv.Set.sumDiffSubset_symm_apply_of_mem {α : Type u_3} {s t : Set α} (h : s ⊆ t) [DecidablePred fun (x : α) => x ∈ s] {x : ↑t} (hx : ↑x ∈ s) : (Set.sumDiffSubset h).symm x = Sum.inl ⟨↑x, hx⟩

theorem Equiv.Set.sumDiffSubset_symm_apply_of_notMem {α : Type u_3} {s t : Set α} (h : s ⊆ t) [DecidablePred fun (x : α) => x ∈ s] {x : ↑t} (hx : ↑x ∉ s) : (Set.sumDiffSubset h).symm x = Sum.inr ⟨↑x, ⋯⟩

def Equiv.Set.unionSumInter {α : Type u} (s t : Set α) [DecidablePred fun (x : α) => x ∈ s] : ↑(s ∪ t) ⊕ ↑(s ∩ t) ≃ ↑s ⊕ ↑t

If s is a set with decidable membership, then the sum of s ∪ t and s ∩ t is equivalent to s ⊕ t.

def Equiv.Set.compl {α : Type u} {β : Type v} {s : Set α} {t : Set β} [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : β) => x ∈ t] (e₀ : ↑s ≃ ↑t) : { e : α ≃ β // ∀ (x : ↑s), e ↑x = ↑(e₀ x) } ≃ (↑sᶜ ≃ ↑tᶜ)

Given an equivalence e₀ between sets s : Set α and t : Set β, the set of equivalences e : α ≃ β such that e ↑x = ↑(e₀ x) for each x : s is equivalent to the set of equivalences between sᶜ and tᶜ.

def Equiv.Set.prod {α : Type u_3} {β : Type u_4} (s : Set α) (t : Set β) : ↑(s ×ˢ t) ≃ ↑s × ↑t

The set product of two sets is equivalent to the type product of their coercions to types.

def Equiv.Set.univPi {α : Type u_3} {β : α → Type u_4} (s : (a : α) → Set (β a)) : ↑(_root_.Set.univ.pi s) ≃ ((a : α) → ↑(s a))

The set Set.pi Set.univ s is equivalent to Π a, s a.

@[simp]

theorem Equiv.Set.univPi_symm_apply_coe {α : Type u_3} {β : α → Type u_4} (s : (a : α) → Set (β a)) (f : (a : α) → ↑(s a)) (a : α) : ↑((Set.univPi s).symm f) a = ↑(f a)

@[simp]

theorem Equiv.Set.univPi_apply_coe {α : Type u_3} {β : α → Type u_4} (s : (a : α) → Set (β a)) (f : ↑(_root_.Set.univ.pi s)) (a : α) : ↑((Set.univPi s) f a) = ↑f a

noncomputable def Equiv.Set.imageOfInjOn {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set α) (H : Set.InjOn f s) : ↑s ≃ ↑(f '' s)

If a function f is injective on a set s, then s is equivalent to f '' s.

noncomputable def Equiv.Set.image {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set α) (H : Function.Injective f) : ↑s ≃ ↑(f '' s)

If f is an injective function, then s is equivalent to f '' s.

@[simp]

theorem Equiv.Set.image_apply {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set α) (H : Function.Injective f) (p : ↑s) : (Set.image f s H) p = ⟨f ↑p, ⋯⟩

@[simp]

theorem Equiv.Set.image_symm_apply {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set α) (H : Function.Injective f) (x : α) (h : f x ∈ f '' s) : (Set.image f s H).symm ⟨f x, h⟩ = ⟨x, ⋯⟩

theorem Equiv.Set.image_symm_preimage {α : Type u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) (u s : Set α) : (fun (x : ↑(f '' s)) => ↑((Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' (f '' u)

def Equiv.Set.congr {α : Type u_3} {β : Type u_4} (e : α ≃ β) : Set α ≃ Set β

If α is equivalent to β, then Set α is equivalent to Set β.

@[simp]

theorem Equiv.Set.congr_apply {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) : (Set.congr e) s = ⇑e '' s

@[simp]

theorem Equiv.Set.congr_symm_apply {α : Type u_3} {β : Type u_4} (e : α ≃ β) (t : Set β) : (Set.congr e).symm t = ⇑e.symm '' t

def Equiv.Set.sep {α : Type u} (s : Set α) (t : α → Prop) : ↑{x : α | x ∈ s ∧ t x} ≃ ↑{x : ↑s | t ↑x}

The set {x ∈ s | t x} is equivalent to the set of x : s such that t x.

def Equiv.Set.powerset {α : Type u_3} (S : Set α) : ↑(𝒫 S) ≃ Set ↑S

The set 𝒫 S := {x | x ⊆ S} is equivalent to the type Set S.

noncomputable def Equiv.Set.rangeSplittingImageEquiv {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set ↑(Set.range f)) : ↑(Set.rangeSplitting f '' s) ≃ ↑s

If s is a set in range f, then its image under rangeSplitting f is in bijection (via f) with s.

@[simp]

theorem Equiv.Set.rangeSplittingImageEquiv_apply_coe_coe {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set ↑(Set.range f)) (x : ↑(Set.rangeSplitting f '' s)) : ↑↑((rangeSplittingImageEquiv f s) x) = f ↑x

@[simp]

theorem Equiv.Set.rangeSplittingImageEquiv_symm_apply_coe {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set ↑(Set.range f)) (x : ↑s) : ↑((rangeSplittingImageEquiv f s).symm x) = Set.rangeSplitting f ↑x

def Equiv.Set.rangeInl (α : Type u_3) (β : Type u_4) : ↑(Set.range Sum.inl) ≃ α

Equivalence between the range of Sum.inl : α → α ⊕ β and α.

@[simp]

theorem Equiv.Set.rangeInl_symm_apply_coe (α : Type u_3) (β : Type u_4) (x : α) : ↑((rangeInl α β).symm x) = Sum.inl x

@[simp]

theorem Equiv.Set.rangeInl_apply_inl {α : Type u_3} (β : Type u_4) (x : α) : (rangeInl α β) ⟨Sum.inl x, ⋯⟩ = x

def Equiv.Set.rangeInr (α : Type u_3) (β : Type u_4) : ↑(Set.range Sum.inr) ≃ β

Equivalence between the range of Sum.inr : β → α ⊕ β and β.

@[simp]

theorem Equiv.Set.rangeInr_symm_apply_coe (α : Type u_3) (β : Type u_4) (x : β) : ↑((rangeInr α β).symm x) = Sum.inr x

@[simp]

theorem Equiv.Set.rangeInr_apply_inr (α : Type u_3) {β : Type u_4} (x : β) : (rangeInr α β) ⟨Sum.inr x, ⋯⟩ = x

def Equiv.ofLeftInverse {α : Sort u_3} {β : Type u_4} (f : α → β) (f_inv : Nonempty α → β → α) (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) : α ≃ ↑(Set.range f)

If f : α → β has a left-inverse when α is nonempty, then α is computably equivalent to the range of f.

While awkward, the Nonempty α hypothesis on f_inv and hf allows this to be used when α is empty too. This hypothesis is absent on analogous definitions on stronger Equivs like LinearEquiv.ofLeftInverse and RingEquiv.ofLeftInverse as their typeclass assumptions are already sufficient to ensure non-emptiness.

@[simp]

theorem Equiv.ofLeftInverse_apply_coe {α : Sort u_3} {β : Type u_4} (f : α → β) (f_inv : Nonempty α → β → α) (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) (a : α) : ↑((ofLeftInverse f f_inv hf) a) = f a

@[simp]

theorem Equiv.ofLeftInverse_symm_apply {α : Sort u_3} {β : Type u_4} (f : α → β) (f_inv : Nonempty α → β → α) (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) (b : ↑(Set.range f)) : (ofLeftInverse f f_inv hf).symm b = f_inv ⋯ ↑b

@[reducible, inline]

abbrev Equiv.ofLeftInverse' {α : Sort u_3} {β : Type u_4} (f : α → β) (f_inv : β → α) (hf : Function.LeftInverse f_inv f) : α ≃ ↑(Set.range f)

If f : α → β has a left-inverse, then α is computably equivalent to the range of f.

Note that if α is empty, no such f_inv exists and so this definition can't be used, unlike the stronger but less convenient ofLeftInverse.

noncomputable def Equiv.ofInjective {α : Sort u_3} {β : Type u_4} (f : α → β) (hf : Function.Injective f) : α ≃ ↑(Set.range f)

If f : α → β is an injective function, then domain α is equivalent to the range of f.

@[simp]

theorem Equiv.ofInjective_apply {α : Sort u_3} {β : Type u_4} (f : α → β) (hf : Function.Injective f) (a : α) : (ofInjective f hf) a = ⟨f a, ⋯⟩

theorem Equiv.apply_ofInjective_symm {α : Sort u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) (b : ↑(Set.range f)) : f ((ofInjective f hf).symm b) = ↑b

@[simp]

theorem Equiv.ofInjective_symm_apply {α : Sort u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) (a : α) : (ofInjective f hf).symm ⟨f a, ⋯⟩ = a

theorem Equiv.coe_ofInjective_symm {α : Type u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) : ⇑(ofInjective f hf).symm = Set.rangeSplitting f

@[simp]

theorem Equiv.self_comp_ofInjective_symm {α : Sort u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) : f ∘ ⇑(ofInjective f hf).symm = Subtype.val

theorem Equiv.ofLeftInverse_eq_ofInjective {α : Type u_3} {β : Type u_4} (f : α → β) (f_inv : Nonempty α → β → α) (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) : ofLeftInverse f f_inv hf = ofInjective f ⋯

theorem Equiv.ofLeftInverse'_eq_ofInjective {α : Type u_3} {β : Type u_4} (f : α → β) (f_inv : β → α) (hf : Function.LeftInverse f_inv f) : ofLeftInverse' f f_inv hf = ofInjective f ⋯

theorem Equiv.set_forall_iff {α : Type u_3} {β : Type u_4} (e : α ≃ β) {p : Set α → Prop} : (∀ (a : Set α), p a) ↔ ∀ (a : Set β), p (⇑e ⁻¹' a)

theorem Equiv.preimage_piEquivPiSubtypeProd_symm_pi {α : Type u_3} {β : α → Type u_4} (p : α → Prop) [DecidablePred p] (s : (i : α) → Set (β i)) : ⇑(piEquivPiSubtypeProd p β).symm ⁻¹' _root_.Set.univ.pi s = (_root_.Set.univ.pi fun (i : { i : α // p i }) => s ↑i) ×ˢ _root_.Set.univ.pi fun (i : { i : α // ¬p i }) => s ↑i

def Equiv.sigmaPreimageEquiv {α : Type u_3} {β : Type u_4} (f : α → β) : (b : β) × ↑(f ⁻¹' {b}) ≃ α

sigmaPreimageEquiv f for f : α → β is the natural equivalence between the type of all preimages of points under f and the total space α.

@[simp]

theorem Equiv.sigmaPreimageEquiv_symm_apply_snd_coe {α : Type u_3} {β : Type u_4} (f : α → β) (x : α) : ↑((sigmaPreimageEquiv f).symm x).snd = x

@[simp]

theorem Equiv.sigmaPreimageEquiv_apply {α : Type u_3} {β : Type u_4} (f : α → β) (x : (y : β) × { x : α // f x = y }) : (sigmaPreimageEquiv f) x = ↑x.snd

@[simp]

theorem Equiv.sigmaPreimageEquiv_symm_apply_fst {α : Type u_3} {β : Type u_4} (f : α → β) (x : α) : ((sigmaPreimageEquiv f).symm x).fst = f x

def Equiv.ofPreimageEquiv {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})) : α ≃ β

A family of equivalences between preimages of points gives an equivalence between domains.

@[simp]

theorem Equiv.ofPreimageEquiv_symm_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})) (a✝ : β) : (ofPreimageEquiv e).symm a✝ = ↑((sigmaCongrRight e).symm ((sigmaFiberEquiv g).symm a✝)).snd

@[simp]

theorem Equiv.ofPreimageEquiv_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})) (a✝ : α) : (ofPreimageEquiv e) a✝ = ↑((e (f a✝)) ((sigmaFiberEquiv f).symm a✝).snd)

theorem Equiv.ofPreimageEquiv_map {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})) (a : α) : g ((ofPreimageEquiv e) a) = f a

noncomputable def Set.BijOn.equiv {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (f : α → β) (h : BijOn f s t) : ↑s ≃ ↑t

If a function is a bijection between two sets s and t, then it induces an equivalence between the types ↥s and ↥t.

theorem dite_comp_equiv_update {α : Type u_1} {E : Type u_2} {β : Sort u_3} {γ : Sort u_4} {p : α → Prop} [EquivLike E { x : α // p x } β] (e : E) (v : β → γ) (w : α → γ) (j : β) (x : γ) [DecidableEq β] [DecidableEq α] [(j : α) → Decidable (p j)] : (fun (i : α) => if h : p i then Function.update v j x (e ⟨i, h⟩) else w i) = Function.update (fun (i : α) => if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x

The composition of an updated function with an equiv on a subtype can be expressed as an updated function.

theorem Equiv.swap_bijOn_self {α : Type u_1} [DecidableEq α] {a b : α} {s : Set α} (hs : a ∈ s ↔ b ∈ s) : Set.BijOn (⇑(swap a b)) s s

theorem Equiv.swap_bijOn_exchange {α : Type u_1} [DecidableEq α] {a b : α} {s : Set α} (ha : a ∈ s) (hb : b ∉ s) : Set.BijOn (⇑(swap a b)) s (insert b (s \ {a}))