# 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.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.symm_image_subset {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) :
e.symm '' t s t e '' s
@[deprecated Equiv.symm_image_subset]
theorem Equiv.subset_image {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) :
e.symm '' t s t e '' s

Alias of Equiv.symm_image_subset.

@[simp]
theorem Equiv.subset_symm_image {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) :
s e.symm '' t e '' s t
@[deprecated Equiv.subset_symm_image]
theorem Equiv.subset_image' {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) :
s e.symm '' t e '' s t

Alias of Equiv.subset_symm_image.

@[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
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
theorem Equiv.setOf_apply_symm_eq_image_setOf {α : Type u_1} {β : Type u_2} (e : α β) (p : αProp) :
{b : β | p (e.symm b)} = e '' {a : α | p a}
@[simp]
theorem Equiv.prod_assoc_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {u : Set γ} :
() ⁻¹' 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 γ} :
().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 γ} :
() '' (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 γ} :
().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}.

Equations
• = { toFun := fun (x : s) => (x).1, (x).2, , invFun := fun (x : (x : α) × {y : β | (x, y) s}) => (x.fst, x.snd), , left_inv := , right_inv := }
Instances For
@[simp]
theorem Equiv.setCongr_apply {α : Type u_1} {s : Set α} {t : Set α} (h : s = t) (a : { a : α // (fun (x : α) => x s) a }) :
() a = a,
def Equiv.setCongr {α : Type u_1} {s : Set α} {t : Set α} (h : s = t) :
s t

The subtypes corresponding to equal sets are equivalent.

Equations
Instances For
@[simp]
theorem Equiv.image_symm_apply_coe {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (y : (e '' s)) :
((e.image s).symm y) = e.symm y
@[simp]
theorem Equiv.image_apply_coe {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (x : s) :
((e.image 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.

Equations
• e.image s = { toFun := fun (x : s) => e x, , invFun := fun (y : (e '' s)) => e.symm y, , left_inv := , right_inv := }
Instances For
def Equiv.Set.univ (α : Type u_1) :
Set.univ α

univ α is equivalent to α.

Equations
• = { toFun := Subtype.val, invFun := fun (a : α) => a, trivial, left_inv := , right_inv := }
Instances For
def Equiv.Set.empty (α : Type u_1) :

An empty set is equivalent to the Empty type.

Equations
Instances For
def Equiv.Set.pempty (α : Type u_1) :

An empty set is equivalent to a PEmpty type.

Equations
Instances For
def Equiv.Set.union' {α : Type u_1} {s : Set α} {t : Set α} (p : αProp) [] (hs : xs, p x) (ht : xt, ¬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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
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.

Equations
Instances For
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) :
() a = Sum.inl a, 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) :
() a = Sum.inr a, 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) :
().symm () = a,
@[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) :
().symm () = a,
def Equiv.Set.singleton {α : Type u_1} (a : α) :
{a} PUnit.{u}

A singleton set is equivalent to a PUnit type.

Equations
• = { toFun := fun (x : {a}) => PUnit.unit, invFun := fun (x : PUnit.{u}) => a, , left_inv := , right_inv := }
Instances For
@[simp]
theorem Equiv.Set.ofEq_symm_apply {α : Type u} {s : Set α} {t : Set α} (h : s = t) (b : { b : α // (fun (x : α) => x t) b }) :
().symm b = b,
@[simp]
theorem Equiv.Set.ofEq_apply {α : Type u} {s : Set α} {t : Set α} (h : s = t) (a : { a : α // (fun (x : α) => x s) a }) :
() a = a,
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!

Equations
Instances For
def Equiv.Set.insert {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x s] {a : α} (H : as) :
(insert a s)

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

Equations
Instances For
@[simp]
theorem Equiv.Set.insert_symm_apply_inl {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x s] {a : α} (H : as) (b : s) :
().symm () = b,
@[simp]
theorem Equiv.Set.insert_symm_apply_inr {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x s] {a : α} (H : as) (b : PUnit.{u + 1} ) :
().symm () = a,
@[simp]
theorem Equiv.Set.insert_apply_left {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x s] {a : α} (H : as) :
() a, =
@[simp]
theorem Equiv.Set.insert_apply_right {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x s] {a : α} (H : as) (b : s) :
() 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 α.

Equations
Instances For
@[simp]
theorem Equiv.Set.sumCompl_apply_inl {α : Type u} (s : Set α) [DecidablePred fun (x : α) => x s] (x : s) :
() = x
@[simp]
theorem Equiv.Set.sumCompl_apply_inr {α : Type u} (s : Set α) [DecidablePred fun (x : α) => x s] (x : s) :
() = x
theorem Equiv.Set.sumCompl_symm_apply_of_mem {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x s] {x : α} (hx : x s) :
.symm x = Sum.inl x, hx
theorem Equiv.Set.sumCompl_symm_apply_of_not_mem {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x s] {x : α} (hx : xs) :
.symm x = Sum.inr x, hx
@[simp]
theorem Equiv.Set.sumCompl_symm_apply {α : Type u_1} {s : Set α} [DecidablePred fun (x : α) => x s] {x : s} :
.symm x =
@[simp]
theorem Equiv.Set.sumCompl_symm_apply_compl {α : Type u_1} {s : Set α} [DecidablePred fun (x : α) => x s] {x : s} :
.symm 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.

Equations
Instances For
@[simp]
theorem Equiv.Set.sumDiffSubset_apply_inl {α : Type u_1} {s : Set α} {t : Set α} (h : s t) [DecidablePred fun (x : α) => x s] (x : s) :
() =
@[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)) :
() =
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) :
.symm x = Sum.inl x, 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 : xs) :
.symm x = Sum.inr x,
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
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ᶜ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
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.

Equations
• = Equiv.subtypeProdEquivProd
Instances For
@[simp]
theorem Equiv.Set.univPi_apply_coe {α : Type u_1} {β : αType u_2} (s : (a : α) → Set (β a)) (f : (Set.univ.pi s)) (a : α) :
(() f a) = f a
@[simp]
theorem Equiv.Set.univPi_symm_apply_coe {α : Type u_1} {β : αType u_2} (s : (a : α) → Set (β a)) (f : (a : α) → (s a)) (a : α) :
(().symm f) a = (f a)
def Equiv.Set.univPi {α : Type u_1} {β : αType u_2} (s : (a : α) → Set (β a)) :
(Set.univ.pi s) ((a : α) → (s a))

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

Equations
• = { toFun := fun (f : (Set.univ.pi s)) (a : α) => f a, , invFun := fun (f : (a : α) → (s a)) => fun (a : α) => (f a), , left_inv := , right_inv := }
Instances For
noncomputable def Equiv.Set.imageOfInjOn {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (H : ) :
s (f '' s)

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

Equations
• = { toFun := fun (p : s) => f p, , invFun := fun (p : (f '' s)) => ⟨, , left_inv := , right_inv := }
Instances For
@[simp]
theorem Equiv.Set.image_apply {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (H : ) (p : s) :
() p = f p,
noncomputable def Equiv.Set.image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (H : ) :
s (f '' s)

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

Equations
Instances For
@[simp]
theorem Equiv.Set.image_symm_apply {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (H : ) (x : α) (h : f x f '' s) :
().symm f x, h = x,
theorem Equiv.Set.image_symm_preimage {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (u : Set α) (s : Set α) :
(fun (x : (f '' s)) => ((Equiv.Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' (f '' u)
@[simp]
theorem Equiv.Set.congr_apply {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) :
() s = e '' s
@[simp]
theorem Equiv.Set.congr_symm_apply {α : Type u_1} {β : Type u_2} (e : α β) (t : Set β) :
().symm t = e.symm '' t
def Equiv.Set.congr {α : Type u_1} {β : Type u_2} (e : α β) :
Set α Set β

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

Equations
• = { toFun := fun (s : Set α) => e '' s, invFun := fun (t : Set β) => e.symm '' t, left_inv := , right_inv := }
Instances For
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.

Equations
• = .symm
Instances For
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.

Equations
• = { toFun := fun (x : (𝒫 S)) => Subtype.val ⁻¹' x, invFun := fun (x : Set S) => Subtype.val '' x, , left_inv := , right_inv := }
Instances For
@[simp]
theorem Equiv.Set.rangeSplittingImageEquiv_symm_apply_coe {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set ()) (x : s) :
(.symm x) =
@[simp]
theorem Equiv.Set.rangeSplittingImageEquiv_apply_coe_coe {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set ()) (x : ()) :
() = f x
noncomputable def Equiv.Set.rangeSplittingImageEquiv {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set ()) :
() s

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Equiv.Set.rangeInl_symm_apply_coe (α : Type u_1) (β : Type u_2) (x : α) :
(().symm x) =
def Equiv.Set.rangeInl (α : Type u_1) (β : Type u_2) :
(Set.range Sum.inl) α

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Equiv.Set.rangeInl_apply_inl {α : Type u_1} (β : Type u_2) (x : α) :
() , = x
@[simp]
theorem Equiv.Set.rangeInr_symm_apply_coe (α : Type u_1) (β : Type u_2) (x : β) :
(().symm x) =
def Equiv.Set.rangeInr (α : Type u_1) (β : Type u_2) :
(Set.range Sum.inr) β

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Equiv.Set.rangeInr_apply_inr (α : Type u_1) {β : Type u_2} (x : β) :
() , = x
@[simp]
theorem Equiv.ofLeftInverse_symm_apply {α : Sort u_1} {β : Type u_2} (f : αβ) (f_inv : βα) (hf : ∀ (h : ), Function.LeftInverse (f_inv h) f) (b : ()) :
(Equiv.ofLeftInverse f f_inv hf).symm b = f_inv b
@[simp]
theorem Equiv.ofLeftInverse_apply_coe {α : Sort u_1} {β : Type u_2} (f : αβ) (f_inv : βα) (hf : ∀ (h : ), Function.LeftInverse (f_inv h) f) (a : α) :
((Equiv.ofLeftInverse f f_inv hf) a) = f a
def Equiv.ofLeftInverse {α : Sort u_1} {β : Type u_2} (f : αβ) (f_inv : βα) (hf : ∀ (h : ), Function.LeftInverse (f_inv h) 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.

Equations
• Equiv.ofLeftInverse f f_inv hf = { toFun := fun (a : α) => f a, , invFun := fun (b : ()) => f_inv b, left_inv := , right_inv := }
Instances For
@[reducible, inline]
abbrev Equiv.ofLeftInverse' {α : Sort u_1} {β : Type u_2} (f : αβ) (f_inv : βα) (hf : Function.LeftInverse f_inv 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.

Equations
Instances For
@[simp]
theorem Equiv.ofInjective_apply {α : Sort u_1} {β : Type u_2} (f : αβ) (hf : ) (a : α) :
() a = f a,
noncomputable def Equiv.ofInjective {α : Sort u_1} {β : Type u_2} (f : αβ) (hf : ) :
α ()

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

Equations
Instances For
theorem Equiv.apply_ofInjective_symm {α : Sort u_1} {β : Type u_2} {f : αβ} (hf : ) (b : ()) :
f (().symm b) = b
@[simp]
theorem Equiv.ofInjective_symm_apply {α : Sort u_1} {β : Type u_2} {f : αβ} (hf : ) (a : α) :
().symm f a, = a
theorem Equiv.coe_ofInjective_symm {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) :
().symm =
@[simp]
theorem Equiv.self_comp_ofInjective_symm {α : Sort u_1} {β : Type u_2} {f : αβ} (hf : ) :
f ().symm = Subtype.val
theorem Equiv.ofLeftInverse_eq_ofInjective {α : Type u_1} {β : Type u_2} (f : αβ) (f_inv : βα) (hf : ∀ (h : ), Function.LeftInverse (f_inv h) f) :
theorem Equiv.ofLeftInverse'_eq_ofInjective {α : Type u_1} {β : Type u_2} (f : αβ) (f_inv : βα) (hf : Function.LeftInverse f_inv 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) [] (s : (i : α) → Set (β i)) :
.symm ⁻¹' Set.univ.pi s = (Set.univ.pi fun (i : { i : α // p i }) => s i) ×ˢ Set.univ.pi fun (i : { i : α // ¬p i }) => s i
@[simp]
theorem Equiv.sigmaPreimageEquiv_apply {α : Type u_1} {β : Type u_2} (f : αβ) (x : (y : β) × { x : α // f x = y }) :
= x.snd
@[simp]
theorem Equiv.sigmaPreimageEquiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
(.symm x).fst = f x
@[simp]
theorem Equiv.sigmaPreimageEquiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
(.symm x).snd = 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 α.

Equations
Instances For
@[simp]
theorem Equiv.ofPreimageEquiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αγ} {g : βγ} (e : (c : γ) → (f ⁻¹' {c}) (g ⁻¹' {c})) :
∀ (a : α), = ((e (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 : β), .symm a = (.symm (.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.

Equations
Instances For
theorem Equiv.ofPreimageEquiv_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αγ} {g : βγ} (e : (c : γ) → (f ⁻¹' {c}) (g ⁻¹' {c})) (a : α) :
g () = 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.

Equations
Instances For
theorem dite_comp_equiv_update {α : Type u_1} {β : Sort u_2} {γ : Sort u_3} {p : αProp} (e : β ) (v : βγ) (w : αγ) (j : β) (x : γ) [] [] [(j : α) → Decidable (p j)] :
(fun (i : α) => if h : p i then Function.update v j x (e.symm i, h) else w i) = Function.update (fun (i : α) => if h : p i then v (e.symm i, 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.

theorem Equiv.swap_bijOn_self {α : Type u_1} [] {a : α} {b : α} {s : Set α} (hs : a s b s) :
Set.BijOn (()) s s
theorem Equiv.swap_bijOn_exchange {α : Type u_1} [] {a : α} {b : α} {s : Set α} (ha : a s) (hb : bs) :
Set.BijOn (()) s (insert b (s \ {a}))