logic.equiv.set

# Equivalences and sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we provide lemmas linking equivalences to sets.

Some notable definitions are:

• equiv.of_injective: an injective function is (noncomputably) equivalent to its range.
• equiv.set_congr: 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 : α β) :
@[protected]
theorem equiv.image_eq_preimage {α : Type u_1} {β : Type u_2} (e : α β) (s : set α) :
e '' s = (e.symm) ⁻¹' s
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

@[protected, simp]
theorem equiv.subset_image {α : Type u_1} {β : Type u_2} (e : α β) (s : set α) (t : set β) :
(e.symm) '' t s t e '' s
@[protected, 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
@[protected]
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 β) :
@[simp]
theorem equiv.preimage_symm_preimage {α : Type u_1} {β : Type u_2} (e : α β) (s : set α) :
@[simp]
theorem equiv.preimage_subset {α : Type u_1} {β : Type u_2} (e : α β) (s t : set β) :
@[simp]
theorem equiv.image_subset {α : Type u_1} {β : Type u_2} (e : α β) (s t : set α) :
e '' s e '' t s t
@[simp]
theorem equiv.image_eq_iff_eq {α : Type u_1} {β : Type u_2} (e : α β) (s 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 γ} :
β γ) ⁻¹' 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.set_prod_equiv_sigma {α : 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
def equiv.set_congr {α : Type u_1} {s t : set α} (h : s = t) :

The subtypes corresponding to equal sets are equivalent.

Equations
@[simp]
theorem equiv.set_congr_apply {α : Type u_1} {s t : set α} (h : s = t) (a : {a // (λ (a : α), (λ (x : α), x s) a) a}) :
a = a, _⟩
@[simp]
theorem equiv.image_apply_coe {α : Type u_1} {β : Type u_2} (e : α β) (s : set α) (x : s) :
((e.image s) x) = e x.val
def equiv.image {α : Type u_1} {β : Type u_2} (e : α β) (s : set α) :

A set is equivalent to its image under an equivalence.

Equations
@[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.val
@[simp]
theorem equiv.set.univ_symm_apply (α : Type u_1) (a : α) :
@[protected]
def equiv.set.univ (α : Type u_1) :

univ α is equivalent to α.

Equations
@[simp]
theorem equiv.set.univ_apply (α : Type u_1) (ᾰ : set.univ) :
=
@[protected]
def equiv.set.empty (α : Type u_1) :

An empty set is equivalent to the empty type.

Equations
@[protected]
def equiv.set.pempty (α : Type u_1) :

An empty set is equivalent to a pempty type.

Equations
@[protected]
def equiv.set.union' {α : Type u_1} {s t : set α} (p : α Prop) (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.

Equations
@[protected]
def equiv.set.union {α : Type u_1} {s t : set α} [decidable_pred (λ (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
theorem equiv.set.union_apply_left {α : Type u_1} {s t : set α} [decidable_pred (λ (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 t : set α} [decidable_pred (λ (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 t : set α} [decidable_pred (λ (x : α), x s)] (H : s t ) (a : s) :
@[simp]
theorem equiv.set.union_symm_apply_right {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] (H : s t ) (a : t) :
@[protected]
def equiv.set.singleton {α : Type u_1} (a : α) :

A singleton set is equivalent to a punit type.

Equations
@[simp]
theorem equiv.set.of_eq_apply {α : Type u} {s t : set α} (h : s = t) (a : {a // (λ (a : α), (λ (x : α), x s) a) a}) :
a = a, _⟩
@[protected]
def equiv.set.of_eq {α : Type u} {s t : set α} (h : s = t) :

Equal sets are equivalent.

TODO: this is the same as equiv.set_congr!

Equations
@[simp]
theorem equiv.set.of_eq_symm_apply {α : Type u} {s t : set α} (h : s = t) (b : {b // (λ (b : α), (λ (x : α), x t) b) b}) :
@[protected]
def equiv.set.insert {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x s)] {a : α} (H : a s) :
s)

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

Equations
@[simp]
theorem equiv.set.insert_symm_apply_inl {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x s)] {a : α} (H : a s) (b : s) :
@[simp]
theorem equiv.set.insert_symm_apply_inr {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x s)] {a : α} (H : a s) (b : punit) :
@[simp]
theorem equiv.set.insert_apply_left {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x s)] {a : α} (H : a s) :
a, _⟩ = sum.inr punit.star
@[simp]
theorem equiv.set.insert_apply_right {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x s)] {a : α} (H : a s) (b : s) :
b, _⟩ =
@[protected]
def equiv.set.sum_compl {α : Type u_1} (s : set α) [decidable_pred (λ (_x : α), _x s)] :

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

Equations
@[simp]
theorem equiv.set.sum_compl_apply_inl {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x s)] (x : s) :
(sum.inl x) = x
@[simp]
theorem equiv.set.sum_compl_apply_inr {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x s)] (x : s) :
(sum.inr x) = x
theorem equiv.set.sum_compl_symm_apply_of_mem {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x s)] {x : α} (hx : x s) :
.symm) x = sum.inl x, hx⟩
theorem equiv.set.sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x s)] {x : α} (hx : x s) :
.symm) x = sum.inr x, hx⟩
@[simp]
theorem equiv.set.sum_compl_symm_apply {α : Type u_1} {s : set α} [decidable_pred (λ (_x : α), _x s)] {x : s} :
@[simp]
theorem equiv.set.sum_compl_symm_apply_compl {α : Type u_1} {s : set α} [decidable_pred (λ (_x : α), _x s)] {x : s} :
@[protected]
def equiv.set.sum_diff_subset {α : Type u_1} {s t : set α} (h : s t) [decidable_pred (λ (_x : α), _x s)] :
s (t \ s) t

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

Equations
@[simp]
theorem equiv.set.sum_diff_subset_apply_inl {α : Type u_1} {s t : set α} (h : s t) [decidable_pred (λ (_x : α), _x s)] (x : s) :
=
@[simp]
theorem equiv.set.sum_diff_subset_apply_inr {α : Type u_1} {s t : set α} (h : s t) [decidable_pred (λ (_x : α), _x s)] (x : (t \ s)) :
=
theorem equiv.set.sum_diff_subset_symm_apply_of_mem {α : Type u_1} {s t : set α} (h : s t) [decidable_pred (λ (_x : α), _x s)] {x : t} (hx : x.val s) :
x = sum.inl x, hx⟩
theorem equiv.set.sum_diff_subset_symm_apply_of_not_mem {α : Type u_1} {s t : set α} (h : s t) [decidable_pred (λ (_x : α), _x s)] {x : t} (hx : x.val s) :
x = sum.inr x, _⟩
@[protected]
def equiv.set.union_sum_inter {α : Type u} (s t : set α) [decidable_pred (λ (_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
@[protected]
def equiv.set.compl {α : Type u} {β : Type v} {s : set α} {t : set β} [decidable_pred (λ (_x : α), _x s)] [decidable_pred (λ (_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
@[protected]
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
@[protected]
def equiv.set.univ_pi {α : 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
@[simp]
theorem equiv.set.univ_pi_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.univ_pi_symm_apply_coe {α : Type u_1} {β : α Type u_2} (s : Π (a : α), set (β a)) (f : Π (a : α), (s a)) (a : α) :
(.symm) f) a = (f a)
@[protected]
noncomputable def equiv.set.image_of_inj_on {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) (H : s) :
s (f '' s)

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

Equations
@[protected]
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.

Equations
• H =
@[simp]
theorem equiv.set.image_apply {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) (H : function.injective f) (p : s) :
s H) p = f p, _⟩
@[protected, simp]
theorem equiv.set.image_symm_apply {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) (H : function.injective f) (x : α) (h : x s) :
s H).symm) f x, _⟩ = x, h⟩
theorem equiv.set.image_symm_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) (u s : set α) :
(λ (x : (f '' s)), ( s hf).symm) x)) ⁻¹' u = coe ⁻¹' (f '' u)
@[simp]
theorem equiv.set.congr_apply {α : Type u_1} {β : Type u_2} (e : α β) (s : set α) :
s = e '' s
@[protected]
def equiv.set.congr {α : Type u_1} {β : Type u_2} (e : α β) :
set α set β

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

Equations
@[simp]
theorem equiv.set.congr_symm_apply {α : Type u_1} {β : Type u_2} (e : α β) (t : set β) :
@[protected]
def equiv.set.sep {α : Type u} (s : set α) (t : α Prop) :
{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
@[protected]
def equiv.set.powerset {α : Type u_1} (S : set α) :

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

Equations
@[simp]
theorem equiv.set.range_splitting_image_equiv_symm_apply_coe {α : Type u_1} {β : Type u_2} (f : α β) (s : set (set.range f)) (x : s) :
x) =
noncomputable def equiv.set.range_splitting_image_equiv {α : Type u_1} {β : Type u_2} (f : α β) (s : set (set.range f)) :

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

Equations
@[simp]
theorem equiv.set.range_splitting_image_equiv_apply_coe_coe {α : Type u_1} {β : Type u_2} (f : α β) (s : set (set.range f)) (x : ) :
@[simp]
theorem equiv.of_left_inverse_symm_apply {α : Sort u_1} {β : Type u_2} (f : α β) (f_inv : β α) (hf : (h : nonempty α), function.left_inverse (f_inv h) f) (b : (set.range f)) :
f_inv hf).symm) b = f_inv _ b
def equiv.of_left_inverse {α : Sort u_1} {β : Type u_2} (f : α β) (f_inv : β α) (hf : (h : nonempty α), function.left_inverse (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 linear_equiv.of_left_inverse and ring_equiv.of_left_inverse as their typeclass assumptions are already sufficient to ensure non-emptiness.

Equations
@[simp]
theorem equiv.of_left_inverse_apply_coe {α : Sort u_1} {β : Type u_2} (f : α β) (f_inv : β α) (hf : (h : nonempty α), function.left_inverse (f_inv h) f) (a : α) :
( f_inv hf) a) = f a
@[reducible]
def equiv.of_left_inverse' {α : Sort u_1} {β : Type u_2} (f : α β) (f_inv : β α) (hf : 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 of_left_inverse.

@[simp]
theorem equiv.of_injective_apply {α : Sort u_1} {β : Type u_2} (f : α β) (hf : function.injective f) (a : α) :
hf) a = f a, _⟩
noncomputable def equiv.of_injective {α : Sort u_1} {β : Type u_2} (f : α β) (hf : function.injective f) :

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

Equations
theorem equiv.apply_of_injective_symm {α : Sort u_1} {β : Type u_2} {f : α β} (hf : function.injective f) (b : (set.range f)) :
f ( hf).symm) b) = b
@[simp]
theorem equiv.of_injective_symm_apply {α : Sort u_1} {β : Type u_2} {f : α β} (hf : function.injective f) (a : α) :
hf).symm) f a, _⟩ = a
theorem equiv.coe_of_injective_symm {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) :
hf).symm) =
@[simp]
theorem equiv.self_comp_of_injective_symm {α : Sort u_1} {β : Type u_2} {f : α β} (hf : function.injective f) :
f hf).symm) = coe
theorem equiv.of_left_inverse_eq_of_injective {α : Type u_1} {β : Type u_2} (f : α β) (f_inv : β α) (hf : (h : nonempty α), function.left_inverse (f_inv h) f) :
f_inv hf =
theorem equiv.of_left_inverse'_eq_of_injective {α : Type u_1} {β : Type u_2} (f : α β) (f_inv : β α) (hf : f) :
f_inv hf =
@[protected]
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_pi_equiv_pi_subtype_prod_symm_pi {α : Type u_1} {β : α Type u_2} (p : α Prop) (s : Π (i : α), set (β i)) :
.symm) ⁻¹' = set.univ.pi (λ (i : {i // p i}), s i) ×ˢ set.univ.pi (λ (i : {i // ¬p i}), s i)
@[simp]
theorem equiv.sigma_preimage_equiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
( x).fst = f x
def equiv.sigma_preimage_equiv {α : Type u_1} {β : Type u_2} (f : α β) :
(Σ (b : β), (f ⁻¹' {b})) α

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

Equations
@[simp]
theorem equiv.sigma_preimage_equiv_apply {α : Type u_1} {β : Type u_2} (f : α β) (x : Σ (y : β), {x // f x = y}) :
= (x.snd)
@[simp]
theorem equiv.sigma_preimage_equiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
(( x).snd) = x
def equiv.of_preimage_equiv {α : 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
@[simp]
theorem equiv.of_preimage_equiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α γ} {g : β γ} (e : Π (c : γ), (f ⁻¹' {c}) (g ⁻¹' {c})) (ᾰ : α) :
= ((e (f ᾰ)) (.symm) ᾰ).snd)
@[simp]
theorem equiv.of_preimage_equiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α γ} {g : β γ} (e : Π (c : γ), (f ⁻¹' {c}) (g ⁻¹' {c})) (ᾰ : β) :
.symm) = ((.symm) (.symm) ᾰ)).snd)
theorem equiv.of_preimage_equiv_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α γ} {g : β γ} (e : Π (c : γ), (f ⁻¹' {c}) (g ⁻¹' {c})) (a : α) :
g a) = f a
noncomputable def set.bij_on.equiv {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} (f : α β) (h : 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
theorem dite_comp_equiv_update {α : Type u_1} {β : Sort u_2} {γ : Sort u_3} {s : set α} (e : β s) (v : β γ) (w : α γ) (j : β) (x : γ) [decidable_eq β] [decidable_eq α] [Π (j : α), decidable (j s)] :
(λ (i : α), dite (i s) (λ (h : i s), x ((e.symm) i, h⟩)) (λ (h : i s), w i)) = function.update (λ (i : α), dite (i s) (λ (h : i s), v ((e.symm) i, h⟩)) (λ (h : i s), w i)) (e j) x

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