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 Equiv.range_eq_univ {α : Type u_1} {β : Type u_2} (e : α ≃ β) : Set.range ↑e = Set.univ

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

@[simp]

theorem Set.mem_image_equiv {α : Type u_1} {β : Type u_2} {S : Set α} {f : α ≃ β} {x : β} : x ∈ ↑f '' S ↔ ↑f.symm x ∈ S

theorem Set.image_equiv_eq_preimage_symm {α : Type u_1} {β : Type u_2} (S : Set α) (f : α ≃ β) : ↑f '' S = ↑f.symm ⁻¹' S

Alias for Equiv.image_eq_preimage

theorem Set.preimage_equiv_eq_image_symm {α : Type u_1} {β : Type u_2} (S : Set α) (f : β ≃ α) : ↑f ⁻¹' S = ↑f.symm '' S

Alias for Equiv.image_eq_preimage

@[simp]

theorem Equiv.subset_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β) : ↑e.symm '' t ⊆ s ↔ t ⊆ ↑e '' s

@[simp]

theorem Equiv.subset_image' {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β) : s ⊆ ↑e.symm '' t ↔ ↑e '' s ⊆ t

@[simp]

theorem Equiv.symm_image_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) : ↑e.symm '' (↑e '' s) = s

theorem Equiv.eq_image_iff_symm_image_eq {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β) : t = ↑e '' s ↔ ↑e.symm '' t = s

@[simp]

theorem Equiv.image_symm_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set β) : ↑e '' (↑e.symm '' s) = s

@[simp]

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

@[simp]

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

theorem Equiv.image_compl {α : Type u_1} {β : Type u_2} (f : α ≃ β) (s : Set α) : ↑f '' sᶜ = (↑f '' s)ᶜ

@[simp]

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

@[simp]

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

@[simp]

theorem Equiv.preimage_subset {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set β) (t : Set β) : ↑e ⁻¹' s ⊆ ↑e ⁻¹' t ↔ s ⊆ t

theorem Equiv.image_subset {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set α) : ↑e '' s ⊆ ↑e '' t ↔ s ⊆ t

@[simp]

theorem Equiv.image_eq_iff_eq {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set α) : ↑e '' s = ↑e '' t ↔ s = t

theorem Equiv.preimage_eq_iff_eq_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set β) (t : Set α) : ↑e ⁻¹' s = t ↔ s = ↑e '' t

theorem Equiv.eq_preimage_iff_image_eq {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β) : s = ↑e ⁻¹' t ↔ ↑e '' s = t

@[simp]

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

@[simp]

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

theorem Equiv.prod_assoc_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {u : Set γ} : ↑(Equiv.prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

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

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

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

@[simp]

theorem Equiv.setCongr_apply {α : Type u_1} {s : Set α} {t : Set α} (h : s = t) (a : { a // (fun a => (fun x => x ∈ s) a) a }) : ↑(Equiv.setCongr h) a = { val := ↑a, property := (_ : ↑(Equiv.refl α) ↑a ∈ t) }

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

The subtypes corresponding to equal sets are equivalent.

@[simp]

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

@[simp]

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

def Equiv.image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) : ↑s ≃ ↑(↑e '' s)

A set is equivalent to its image under an equivalence.

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

univ α is equivalent to α.

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

An empty set is equivalent to the Empty type.

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

An empty set is equivalent to a PEmpty type.

def Equiv.Set.union' {α : Type u_1} {s : Set α} {t : Set α} (p : α → Prop) [DecidablePred p] (hs : (x : α) → x ∈ s → p x) (ht : ∀ (x : α), 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_1} {s : Set α} {t : Set α} [DecidablePred fun x => x ∈ s] (H : 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_1} {s : Set α} {t : Set α} [DecidablePred fun x => x ∈ s] (H : s ∩ t ⊆ ∅) {a : ↑(s ∪ t)} (ha : ↑a ∈ s) : ↑(Equiv.Set.union H) a = Sum.inl { val := ↑a, property := ha }

theorem Equiv.Set.union_apply_right {α : Type u_1} {s : Set α} {t : Set α} [DecidablePred fun x => x ∈ s] (H : s ∩ t ⊆ ∅) {a : ↑(s ∪ t)} (ha : ↑a ∈ t) : ↑(Equiv.Set.union H) a = Sum.inr { val := ↑a, property := ha }

@[simp]

theorem Equiv.Set.union_symm_apply_left {α : Type u_1} {s : Set α} {t : Set α} [DecidablePred fun x => x ∈ s] (H : s ∩ t ⊆ ∅) (a : ↑s) : ↑(Equiv.Set.union H).symm (Sum.inl a) = { val := ↑a, property := (_ : ↑a ∈ s ∪ t) }

@[simp]

theorem Equiv.Set.union_symm_apply_right {α : Type u_1} {s : Set α} {t : Set α} [DecidablePred fun x => x ∈ s] (H : s ∩ t ⊆ ∅) (a : ↑t) : ↑(Equiv.Set.union H).symm (Sum.inr a) = { val := ↑a, property := (_ : ↑a ∈ s ∪ t) }

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

A singleton set is equivalent to a PUnit type.

@[simp]

theorem Equiv.Set.ofEq_apply {α : Type u} {s : Set α} {t : Set α} (h : s = t) (a : { a // (fun a => (fun x => x ∈ s) a) a }) : ↑(Equiv.Set.ofEq h) a = { val := ↑a, property := (_ : ↑(Equiv.refl α) ↑a ∈ t) }

@[simp]

theorem Equiv.Set.ofEq_symm_apply {α : Type u} {s : Set α} {t : Set α} (h : s = t) (b : { b // (fun b => (fun x => x ∈ t) b) b }) : ↑(Equiv.Set.ofEq h).symm b = { val := ↑b, property := (_ : ↑(Equiv.refl α).symm ↑b ∈ s) }

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

Equal sets are equivalent.

TODO: this is the same as Equiv.setCongr!

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) : ↑(Equiv.Set.insert H).symm (Sum.inl b) = { val := ↑b, property := (_ : ↑b = a ∨ ↑b ∈ s) }

@[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} ) : ↑(Equiv.Set.insert H).symm (Sum.inr b) = { val := a, property := (_ : a = a ∨ a ∈ s) }

@[simp]

theorem Equiv.Set.insert_apply_left {α : Type u} {s : Set α} [DecidablePred fun x => x ∈ s] {a : α} (H : ¬a ∈ s) : ↑(Equiv.Set.insert H) { val := a, property := (_ : a = a ∨ a ∈ s) } = 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) : ↑(Equiv.Set.insert H) { val := ↑b, property := (_ : ↑b = a ∨ ↑b ∈ s) } = Sum.inl b

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

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

@[simp]

theorem Equiv.Set.sumCompl_apply_inl {α : Type u} (s : Set α) [DecidablePred fun x => x ∈ s] (x : ↑s) : ↑(Equiv.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ᶜ) : ↑(Equiv.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) : ↑(Equiv.Set.sumCompl s).symm x = Sum.inl { val := x, property := hx }

theorem Equiv.Set.sumCompl_symm_apply_of_not_mem {α : Type u} {s : Set α} [DecidablePred fun x => x ∈ s] {x : α} (hx : ¬x ∈ s) : ↑(Equiv.Set.sumCompl s).symm x = Sum.inr { val := x, property := hx }

@[simp]

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

@[simp]

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

def Equiv.Set.sumDiffSubset {α : Type u_1} {s : Set α} {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_1} {s : Set α} {t : Set α} (h : s ⊆ t) [DecidablePred fun x => x ∈ s] (x : ↑s) : ↑(Equiv.Set.sumDiffSubset h) (Sum.inl x) = Set.inclusion h x

@[simp]

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

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

theorem Equiv.Set.sumDiffSubset_symm_apply_of_not_mem {α : Type u_1} {s : Set α} {t : Set α} (h : s ⊆ t) [DecidablePred fun x => x ∈ s] {x : ↑t} (hx : ¬↑x ∈ s) : ↑(Equiv.Set.sumDiffSubset h).symm x = Sum.inr { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) }

def Equiv.Set.unionSumInter {α : Type u} (s : Set α) (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_1} {β : Type u_2} (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.

@[simp]

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

@[simp]

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

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

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

noncomputable def Equiv.Set.imageOfInjOn {α : Type u_1} {β : Type u_2} (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.

@[simp]

theorem Equiv.Set.image_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (H : Function.Injective f) (p : ↑s) : ↑(Equiv.Set.image f s H) p = { val := f ↑p, property := (_ : f ↑p ∈ f '' s) }

noncomputable def Equiv.Set.image {α : Type u_1} {β : Type u_2} (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_symm_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (H : Function.Injective f) (x : α) (h : x ∈ s) : ↑(Equiv.Set.image f s H).symm { val := f x, property := (_ : ∃ a, a ∈ s ∧ f a = f x) } = { val := x, property := h }

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

@[simp]

theorem Equiv.Set.congr_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (t : Set β) : ↑(Equiv.Set.congr e).symm t = ↑e.symm '' t

@[simp]

theorem Equiv.Set.congr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) : ↑(Equiv.Set.congr e) s = ↑e '' s

def Equiv.Set.congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) : Set α ≃ Set β

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

def Equiv.Set.sep {α : Type u} (s : Set α) (t : α → Prop) : ↑{x | x ∈ s ∧ t x} ≃ ↑{x | 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_1} (S : Set α) : ↑(𝒫 S) ≃ Set ↑S

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

@[simp]

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

@[simp]

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

noncomputable def Equiv.Set.rangeSplittingImageEquiv {α : Type u_1} {β : Type u_2} (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.rangeInl_symm_apply_coe (α : Type u_1) (β : Type u_2) (x : α) : ↑(↑(Equiv.Set.rangeInl α β).symm x) = Sum.inl x

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

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

@[simp]

theorem Equiv.Set.rangeInl_apply_inl {α : Type u_1} (β : Type u_2) (x : α) : ↑(Equiv.Set.rangeInl α β) { val := Sum.inl x, property := (_ : Sum.inl x ∈ Set.range Sum.inl) } = x

@[simp]

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

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

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

@[simp]

theorem Equiv.Set.rangeInr_apply_inr (α : Type u_1) {β : Type u_2} (x : β) : ↑(Equiv.Set.rangeInr α β) { val := Sum.inr x, property := (_ : Sum.inr x ∈ Set.range Sum.inr) } = x

@[simp]

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

@[simp]

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

def Equiv.ofLeftInverse {α : Sort u_1} {β : Type u_2} (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.

@[inline, reducible]

abbrev Equiv.ofLeftInverse' {α : Sort u_1} {β : Type u_2} (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.

@[simp]

theorem Equiv.ofInjective_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : Function.Injective f) (a : α) : ↑(Equiv.ofInjective f hf) a = { val := f a, property := (_ : ∃ y, f y = f a) }

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

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

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

@[simp]

theorem Equiv.ofInjective_symm_apply {α : Sort u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (a : α) : ↑(Equiv.ofInjective f hf).symm { val := f a, property := (_ : ∃ y, f y = f a) } = a

theorem Equiv.coe_ofInjective_symm {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) : ↑(Equiv.ofInjective f hf).symm = Set.rangeSplitting f

@[simp]

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

theorem Equiv.ofLeftInverse_eq_ofInjective {α : Type u_1} {β : Type u_2} (f : α → β) (f_inv : Nonempty α → β → α) (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) : Equiv.ofLeftInverse f f_inv hf = Equiv.ofInjective f (_ : Function.Injective f)

theorem Equiv.ofLeftInverse'_eq_ofInjective {α : Type u_1} {β : Type u_2} (f : α → β) (f_inv : β → α) (hf : Function.LeftInverse f_inv f) : Equiv.ofLeftInverse' f f_inv hf = Equiv.ofInjective f (_ : Function.Injective f)

theorem Equiv.set_forall_iff {α : Type u_1} {β : Type u_2} (e : α ≃ β) {p : Set α → Prop} : ((a : Set α) → p a) ↔ (a : Set β) → p (↑e ⁻¹' a)

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

@[simp]

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

@[simp]

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

@[simp]

theorem Equiv.sigmaPreimageEquiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : (↑(Equiv.sigmaPreimageEquiv f).symm x).fst = f x

def Equiv.sigmaPreimageEquiv {α : Type u_1} {β : Type u_2} (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.ofPreimageEquiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})) : ∀ (a : α), ↑(Equiv.ofPreimageEquiv e) a = ↑(↑(e (f a)) (↑(Equiv.sigmaFiberEquiv fun a => f a).symm a).snd)

@[simp]

theorem Equiv.ofPreimageEquiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})) : ∀ (a : β), ↑(Equiv.ofPreimageEquiv e).symm a = ↑(↑(Equiv.sigmaCongrRight e).symm (↑(Equiv.sigmaFiberEquiv fun b => g b).symm a)).snd

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

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

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

noncomputable def Set.BijOn.equiv {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (f : α → β) (h : Set.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} {β : Sort u_2} {γ : Sort u_3} {p : α → Prop} (e : β ≃ Subtype p) (v : β → γ) (w : α → γ) (j : β) (x : γ) [DecidableEq β] [DecidableEq α] [(j : α) → Decidable (p j)] : (fun i => if h : p i then Function.update v j x (↑e.symm { val := i, property := h }) else w i) = Function.update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x

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