mathlib3 documentation

logic.equiv.defs

Equivalence between types #

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

In this file we define two types:

Then we define

Many more such isomorphisms and operations are defined in logic/equiv/basic.

Tags #

equivalence, congruence, bijective map

@[protected, instance]
def equiv.has_coe_t {α : Sort u} {β : Sort v} {F : Sort u_1} [equiv_like F α β] :
has_coe_t F β)
Equations
@[reducible]
def equiv.perm (α : Sort u_1) :
Sort (max 1 u_1)

perm α is the type of bijections from α to itself.

Equations
@[protected, instance]
def equiv.equiv_like {α : Sort u} {β : Sort v} :
equiv_like β) α β
Equations
@[protected, instance]
def equiv.has_coe_to_fun {α : Sort u} {β : Sort v} :
has_coe_to_fun β) (λ (_x : α β), α β)
Equations
@[simp]
theorem equiv.coe_fn_mk {α : Sort u} {β : Sort v} (f : α β) (g : β α) (l : function.left_inverse g f) (r : function.right_inverse g f) :
{to_fun := f, inv_fun := g, left_inv := l, right_inv := r} = f

The map coe_fn : (r ≃ s) → (r → s) is injective.

@[protected]
theorem equiv.coe_inj {α : Sort u} {β : Sort v} {e₁ e₂ : α β} :
e₁ = e₂ e₁ = e₂
@[ext]
theorem equiv.ext {α : Sort u} {β : Sort v} {f g : α β} (H : (x : α), f x = g x) :
f = g
@[protected]
theorem equiv.congr_arg {α : Sort u} {β : Sort v} {f : α β} {x x' : α} :
x = x' f x = f x'
@[protected]
theorem equiv.congr_fun {α : Sort u} {β : Sort v} {f g : α β} (h : f = g) (x : α) :
f x = g x
theorem equiv.ext_iff {α : Sort u} {β : Sort v} {f g : α β} :
f = g (x : α), f x = g x
@[ext]
theorem equiv.perm.ext {α : Sort u} {σ τ : equiv.perm α} (H : (x : α), σ x = τ x) :
σ = τ
@[protected]
theorem equiv.perm.congr_arg {α : Sort u} {f : equiv.perm α} {x x' : α} :
x = x' f x = f x'
@[protected]
theorem equiv.perm.congr_fun {α : Sort u} {f g : equiv.perm α} (h : f = g) (x : α) :
f x = g x
theorem equiv.perm.ext_iff {α : Sort u} {σ τ : equiv.perm α} :
σ = τ (x : α), σ x = τ x
@[protected, refl]
def equiv.refl (α : Sort u_1) :
α α

Any type is equivalent to itself.

Equations
@[protected, instance]
def equiv.inhabited' {α : Sort u} :
inhabited α)
Equations
@[protected, symm]
def equiv.symm {α : Sort u} {β : Sort v} (e : α β) :
β α

Inverse of an equivalence e : α ≃ β.

Equations
def equiv.simps.symm_apply {α : Sort u} {β : Sort v} (e : α β) :
β α

See Note [custom simps projection]

Equations
@[protected, trans]
def equiv.trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
α γ

Composition of equivalences e₁ : α ≃ β and e₂ : β ≃ γ.

Equations
@[simp]
theorem equiv.to_fun_as_coe {α : Sort u} {β : Sort v} (e : α β) :
@[simp]
theorem equiv.inv_fun_as_coe {α : Sort u} {β : Sort v} (e : α β) :
@[protected]
theorem equiv.injective {α : Sort u} {β : Sort v} (e : α β) :
@[protected]
theorem equiv.surjective {α : Sort u} {β : Sort v} (e : α β) :
@[protected]
theorem equiv.bijective {α : Sort u} {β : Sort v} (e : α β) :
@[protected]
theorem equiv.subsingleton {α : Sort u} {β : Sort v} (e : α β) [subsingleton β] :
@[protected]
theorem equiv.subsingleton.symm {α : Sort u} {β : Sort v} (e : α β) [subsingleton α] :
theorem equiv.subsingleton_congr {α : Sort u} {β : Sort v} (e : α β) :
@[protected, instance]
def equiv.equiv_subsingleton_cod {α : Sort u} {β : Sort v} [subsingleton β] :
@[protected, instance]
def equiv.equiv_subsingleton_dom {α : Sort u} {β : Sort v} [subsingleton α] :
@[protected, instance]
Equations
@[protected]
def equiv.decidable_eq {α : Sort u} {β : Sort v} (e : α β) [decidable_eq β] :

Transfer decidable_eq across an equivalence.

Equations
theorem equiv.nonempty_congr {α : Sort u} {β : Sort v} (e : α β) :
@[protected]
theorem equiv.nonempty {α : Sort u} {β : Sort v} (e : α β) [nonempty β] :
@[protected]
def equiv.inhabited {α : Sort u} {β : Sort v} [inhabited β] (e : α β) :

If α ≃ β and β is inhabited, then so is α.

Equations
@[protected]
def equiv.unique {α : Sort u} {β : Sort v} [unique β] (e : α β) :

If α ≃ β and β is a singleton type, then so is α.

Equations
@[protected]
def equiv.cast {α β : Sort u_1} (h : α = β) :
α β

Equivalence between equal types.

Equations
@[simp]
theorem equiv.coe_fn_symm_mk {α : Sort u} {β : Sort v} (f : α β) (g : β α) (l : function.left_inverse g f) (r : function.right_inverse g f) :
({to_fun := f, inv_fun := g, left_inv := l, right_inv := r}.symm) = g
@[simp]
theorem equiv.coe_refl {α : Sort u} :
theorem equiv.perm.coe_subsingleton {α : Type u_1} [subsingleton α] (e : equiv.perm α) :

This cannot be a simp lemmas as it incorrectly matches against e : α ≃ synonym α, when synonym α is semireducible. This makes a mess of multiplicative.of_add etc.

theorem equiv.refl_apply {α : Sort u} (x : α) :
(equiv.refl α) x = x
@[simp]
theorem equiv.coe_trans {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) :
(f.trans g) = g f
theorem equiv.trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : α) :
(f.trans g) a = g (f a)
@[simp]
theorem equiv.apply_symm_apply {α : Sort u} {β : Sort v} (e : α β) (x : β) :
e ((e.symm) x) = x
@[simp]
theorem equiv.symm_apply_apply {α : Sort u} {β : Sort v} (e : α β) (x : α) :
(e.symm) (e x) = x
@[simp]
theorem equiv.symm_comp_self {α : Sort u} {β : Sort v} (e : α β) :
@[simp]
theorem equiv.self_comp_symm {α : Sort u} {β : Sort v} (e : α β) :
@[simp]
theorem equiv.symm_trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : γ) :
((f.trans g).symm) a = (f.symm) ((g.symm) a)
@[simp, nolint]
theorem equiv.symm_symm_apply {α : Sort u} {β : Sort v} (f : α β) (b : α) :
(f.symm.symm) b = f b
theorem equiv.apply_eq_iff_eq {α : Sort u} {β : Sort v} (f : α β) {x y : α} :
f x = f y x = y
theorem equiv.apply_eq_iff_eq_symm_apply {α : Sort u_1} {β : Sort u_2} (f : α β) {x : α} {y : β} :
f x = y x = (f.symm) y
@[simp]
theorem equiv.cast_apply {α β : Sort u_1} (h : α = β) (x : α) :
(equiv.cast h) x = cast h x
@[simp]
theorem equiv.cast_symm {α β : Sort u_1} (h : α = β) :
@[simp]
theorem equiv.cast_refl {α : Sort u_1} (h : α = α := rfl) :
@[simp]
theorem equiv.cast_trans {α β γ : Sort u_1} (h : α = β) (h2 : β = γ) :
theorem equiv.cast_eq_iff_heq {α β : Sort u_1} (h : α = β) {a : α} {b : β} :
(equiv.cast h) a = b a == b
theorem equiv.symm_apply_eq {α : Sort u_1} {β : Sort u_2} (e : α β) {x : β} {y : α} :
(e.symm) x = y x = e y
theorem equiv.eq_symm_apply {α : Sort u_1} {β : Sort u_2} (e : α β) {x : β} {y : α} :
y = (e.symm) x e y = x
@[simp]
theorem equiv.symm_symm {α : Sort u} {β : Sort v} (e : α β) :
e.symm.symm = e
@[simp]
theorem equiv.trans_refl {α : Sort u} {β : Sort v} (e : α β) :
e.trans (equiv.refl β) = e
@[simp]
theorem equiv.refl_symm {α : Sort u} :
@[simp]
theorem equiv.refl_trans {α : Sort u} {β : Sort v} (e : α β) :
(equiv.refl α).trans e = e
@[simp]
theorem equiv.symm_trans_self {α : Sort u} {β : Sort v} (e : α β) :
@[simp]
theorem equiv.self_trans_symm {α : Sort u} {β : Sort v} (e : α β) :
theorem equiv.trans_assoc {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (bc : β γ) (cd : γ δ) :
(ab.trans bc).trans cd = ab.trans (bc.trans cd)
theorem equiv.left_inverse_symm {α : Sort u} {β : Sort v} (f : α β) :
theorem equiv.right_inverse_symm {α : Sort u} {β : Sort v} (f : α β) :
theorem equiv.injective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : β γ) :
theorem equiv.comp_injective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (e : β γ) :
theorem equiv.surjective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : β γ) :
theorem equiv.comp_surjective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (e : β γ) :
theorem equiv.bijective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : β γ) :
theorem equiv.comp_bijective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (e : β γ) :
def equiv.equiv_congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) :
α γ δ)

If α is equivalent to β and γ is equivalent to δ, then the type of equivalences α ≃ γ is equivalent to the type of equivalences β ≃ δ.

Equations
@[simp]
theorem equiv.equiv_congr_refl {α : Sort u_1} {β : Sort u_2} :
@[simp]
theorem equiv.equiv_congr_symm {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) :
@[simp]
theorem equiv.equiv_congr_trans {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} {ε : Sort u_2} {ζ : Sort u_3} (ab : α β) (de : δ ε) (bc : β γ) (ef : ε ζ) :
(ab.equiv_congr de).trans (bc.equiv_congr ef) = (ab.trans bc).equiv_congr (de.trans ef)
@[simp]
theorem equiv.equiv_congr_refl_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (bg : β γ) (e : α β) :
((equiv.refl α).equiv_congr bg) e = e.trans bg
@[simp]
theorem equiv.equiv_congr_refl_right {α : Sort u_1} {β : Sort u_2} (ab e : α β) :
@[simp]
theorem equiv.equiv_congr_apply_apply {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) (e : α γ) (x : β) :
((ab.equiv_congr cd) e) x = cd (e ((ab.symm) x))
def equiv.perm_congr {α' : Type u_1} {β' : Type u_2} (e : α' β') :

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

Equations
theorem equiv.perm_congr_def {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : equiv.perm α') :
@[simp]
theorem equiv.perm_congr_refl {α' : Type u_1} {β' : Type u_2} (e : α' β') :
@[simp]
theorem equiv.perm_congr_symm {α' : Type u_1} {β' : Type u_2} (e : α' β') :
@[simp]
theorem equiv.perm_congr_apply {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : equiv.perm α') (x : β') :
((e.perm_congr) p) x = e (p ((e.symm) x))
theorem equiv.perm_congr_symm_apply {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : equiv.perm β') (x : α') :
((e.perm_congr.symm) p) x = (e.symm) (p (e x))
theorem equiv.perm_congr_trans {α' : Type u_1} {β' : Type u_2} (e : α' β') (p p' : equiv.perm α') :
def equiv.equiv_of_is_empty (α : Sort u_1) (β : Sort u_2) [is_empty α] [is_empty β] :
α β

Two empty types are equivalent.

Equations
def equiv.equiv_empty (α : Sort u) [is_empty α] :

If α is an empty type, then it is equivalent to the empty type.

Equations
def equiv.equiv_pempty (α : Sort v) [is_empty α] :

If α is an empty type, then it is equivalent to the pempty type in any universe.

Equations

α is equivalent to an empty type iff α is empty.

Equations
def equiv.prop_equiv_pempty {p : Prop} (h : ¬p) :

The Sort of proofs of a false proposition is equivalent to pempty.

Equations
def equiv.equiv_of_unique (α : Sort u_1) (β : Sort u_2) [unique α] [unique β] :
α β

If both α and β have a unique element, then α ≃ β.

Equations
def equiv.equiv_punit (α : Sort u_1) [unique α] :

If α has a unique element, then it is equivalent to any punit.

Equations
def equiv.prop_equiv_punit {p : Prop} (h : p) :

The Sort of proofs of a true proposition is equivalent to punit.

Equations
@[simp]
theorem equiv.ulift_symm_apply {α : Type v} :
(equiv.ulift.symm) = ulift.up
@[protected]
def equiv.ulift {α : Type v} :
ulift α α

ulift α is equivalent to α.

Equations
@[simp]
@[simp]
@[protected]
def equiv.plift {α : Sort u} :
plift α α

plift α is equivalent to α.

Equations
@[simp]
theorem equiv.plift_symm_apply {α : Sort u} :
(equiv.plift.symm) = plift.up
def equiv.of_iff {P Q : Prop} (h : P Q) :
P Q

equivalence of propositions is the same as iff

Equations
@[simp]
theorem equiv.arrow_congr_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) (f : α₁ β₁) (ᾰ : α₂) :
(e₁.arrow_congr e₂) f = (e₂ f (e₁.symm))
def equiv.arrow_congr {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(α₁ β₁) (α₂ β₂)

If α₁ is equivalent to α₂ and β₁ is equivalent to β₂, then the type of maps α₁ → β₁ is equivalent to the type of maps α₂ → β₂.

Equations
theorem equiv.arrow_congr_comp {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} (ea : α₁ α₂) (eb : β₁ β₂) (ec : γ₁ γ₂) (f : α₁ β₁) (g : β₁ γ₁) :
(ea.arrow_congr ec) (g f) = (eb.arrow_congr ec) g (ea.arrow_congr eb) f
@[simp]
theorem equiv.arrow_congr_refl {α : Sort u_1} {β : Sort u_2} :
@[simp]
theorem equiv.arrow_congr_trans {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} {α₃ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
(e₁.trans e₂).arrow_congr (e₁'.trans e₂') = (e₁.arrow_congr e₁').trans (e₂.arrow_congr e₂')
@[simp]
theorem equiv.arrow_congr_symm {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(e₁.arrow_congr e₂).symm = e₁.symm.arrow_congr e₂.symm
def equiv.arrow_congr' {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ α₂) (hβ : β₁ β₂) :
(α₁ β₁) (α₂ β₂)

A version of equiv.arrow_congr in Type, rather than Sort.

The equiv_rw tactic is not able to use the default Sort level equiv.arrow_congr, because Lean's universe rules will not unify ?l_1 with imax (1 ?m_1).

Equations
@[simp]
theorem equiv.arrow_congr'_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ α₂) (hβ : β₁ β₂) (f : α₁ β₁) (ᾰ : α₂) :
(hα.arrow_congr' hβ) f = (f ((hα.symm) ᾰ))
@[simp]
theorem equiv.arrow_congr'_refl {α : Type u_1} {β : Type u_2} :
@[simp]
theorem equiv.arrow_congr'_trans {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {α₃ : Type u_5} {β₃ : Type u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
(e₁.trans e₂).arrow_congr' (e₁'.trans e₂') = (e₁.arrow_congr' e₁').trans (e₂.arrow_congr' e₂')
@[simp]
theorem equiv.arrow_congr'_symm {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(e₁.arrow_congr' e₂).symm = e₁.symm.arrow_congr' e₂.symm
def equiv.conj {α : Sort u} {β : Sort v} (e : α β) :
α) β)

Conjugate a map f : α → α by an equivalence α ≃ β.

Equations
@[simp]
theorem equiv.conj_apply {α : Sort u} {β : Sort v} (e : α β) (f : α α) (ᾰ : β) :
(e.conj) f = e (f ((e.symm) ᾰ))
@[simp]
theorem equiv.conj_refl {α : Sort u} :
@[simp]
theorem equiv.conj_symm {α : Sort u} {β : Sort v} (e : α β) :
@[simp]
theorem equiv.conj_trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
(e₁.trans e₂).conj = e₁.conj.trans e₂.conj
theorem equiv.conj_comp {α : Sort u} {β : Sort v} (e : α β) (f₁ f₂ : α α) :
(e.conj) (f₁ f₂) = (e.conj) f₁ (e.conj) f₂
theorem equiv.eq_comp_symm {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : β γ) (g : α γ) :
f = g (e.symm) f e = g
theorem equiv.comp_symm_eq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : β γ) (g : α γ) :
g (e.symm) = f g = f e
theorem equiv.eq_symm_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : γ α) (g : γ β) :
f = (e.symm) g e f = g
theorem equiv.symm_comp_eq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : γ α) (g : γ β) :
(e.symm) g = f g = e f

punit sorts in any two universes are equivalent.

Equations
noncomputable def equiv.Prop_equiv_bool  :
Prop bool

Prop is noncomputably equivalent to bool.

Equations

The sort of maps to punit.{v} is equivalent to punit.{w}.

Equations
def equiv.Pi_subsingleton {α : Sort u_1} (β : α Sort u_2) [subsingleton α] (a : α) :
(Π (a' : α), β a') β a

If α is subsingleton and a : α, then the type of dependent functions Π (i : α), β i is equivalent to β i.

Equations
@[simp]
theorem equiv.Pi_subsingleton_symm_apply {α : Sort u_1} (β : α Sort u_2) [subsingleton α] (a : α) (x : β a) (b : α) :
@[simp]
theorem equiv.Pi_subsingleton_apply {α : Sort u_1} (β : α Sort u_2) [subsingleton α] (a : α) (f : Π (x : α), (λ (a' : α), β a') x) :
def equiv.fun_unique (α : Sort u_1) (β : Sort u_2) [unique α] :
β) β

If α has a unique term, then the type of function α → β is equivalent to β.

Equations
@[simp]
theorem equiv.fun_unique_symm_apply (α : Sort u_1) (β : Sort u_2) [unique α] :
((equiv.fun_unique α β).symm) = λ (x : β) (b : α), x
@[simp]
def equiv.punit_arrow_equiv (α : Sort u_1) :
(punit α) α

The sort of maps from punit is equivalent to the codomain.

Equations
def equiv.true_arrow_equiv (α : Sort u_1) :
(true α) α

The sort of maps from true is equivalent to the codomain.

Equations
def equiv.arrow_punit_of_is_empty (α : Sort u_1) (β : Sort u_2) [is_empty α] :
β) punit

The sort of maps from a type that is_empty is equivalent to punit.

Equations

The sort of maps from empty is equivalent to punit.

Equations

The sort of maps from pempty is equivalent to punit.

Equations

The sort of maps from false is equivalent to punit.

Equations
def equiv.psigma_equiv_sigma {α : Type u_1} (β : α Type u_2) :
(Σ' (i : α), β i) Σ (i : α), β i

A psigma-type is equivalent to the corresponding sigma-type.

Equations
@[simp]
theorem equiv.psigma_equiv_sigma_symm_apply {α : Type u_1} (β : α Type u_2) (a : Σ (i : α), β i) :
@[simp]
theorem equiv.psigma_equiv_sigma_apply {α : Type u_1} (β : α Type u_2) (a : Σ' (i : α), β i) :
def equiv.psigma_equiv_sigma_plift {α : Sort u_1} (β : α Sort u_2) :
(Σ' (i : α), β i) Σ (i : plift α), plift (β i.down)

A psigma-type is equivalent to the corresponding sigma-type.

Equations
@[simp]
theorem equiv.psigma_equiv_sigma_plift_apply {α : Sort u_1} (β : α Sort u_2) (a : Σ' (i : α), β i) :
@[simp]
theorem equiv.psigma_equiv_sigma_plift_symm_apply {α : Sort u_1} (β : α Sort u_2) (a : Σ (i : plift α), plift (β i.down)) :
@[simp]
theorem equiv.psigma_congr_right_apply {α : Sort u_1} {β₁ : α Sort u_2} {β₂ : α Sort u_3} (F : Π (a : α), β₁ a β₂ a) (a : Σ' (a : α), β₁ a) :
def equiv.psigma_congr_right {α : Sort u_1} {β₁ : α Sort u_2} {β₂ : α Sort u_3} (F : Π (a : α), β₁ a β₂ a) :
(Σ' (a : α), β₁ a) Σ' (a : α), β₂ a

A family of equivalences Π a, β₁ a ≃ β₂ a generates an equivalence between Σ' a, β₁ a and Σ' a, β₂ a.

Equations
@[simp]
theorem equiv.psigma_congr_right_trans {α : Sort u_1} {β₁ : α Sort u_2} {β₂ : α Sort u_3} {β₃ : α Sort u_4} (F : Π (a : α), β₁ a β₂ a) (G : Π (a : α), β₂ a β₃ a) :
@[simp]
theorem equiv.psigma_congr_right_symm {α : Sort u_1} {β₁ : α Sort u_2} {β₂ : α Sort u_3} (F : Π (a : α), β₁ a β₂ a) :
@[simp]
theorem equiv.psigma_congr_right_refl {α : Sort u_1} {β : α Sort u_2} :
equiv.psigma_congr_right (λ (a : α), equiv.refl (β a)) = equiv.refl (Σ' (a : α), β a)
@[simp]
theorem equiv.sigma_congr_right_apply {α : Type u_1} {β₁ : α Type u_2} {β₂ : α Type u_3} (F : Π (a : α), β₁ a β₂ a) (a : Σ (a : α), β₁ a) :
def equiv.sigma_congr_right {α : Type u_1} {β₁ : α Type u_2} {β₂ : α Type u_3} (F : Π (a : α), β₁ a β₂ a) :
(Σ (a : α), β₁ a) Σ (a : α), β₂ a

A family of equivalences Π a, β₁ a ≃ β₂ a generates an equivalence between Σ a, β₁ a and Σ a, β₂ a.

Equations
@[simp]
theorem equiv.sigma_congr_right_trans {α : Type u_1} {β₁ : α Type u_2} {β₂ : α Type u_3} {β₃ : α Type u_4} (F : Π (a : α), β₁ a β₂ a) (G : Π (a : α), β₂ a β₃ a) :
@[simp]
theorem equiv.sigma_congr_right_symm {α : Type u_1} {β₁ : α Type u_2} {β₂ : α Type u_3} (F : Π (a : α), β₁ a β₂ a) :
@[simp]
theorem equiv.sigma_congr_right_refl {α : Type u_1} {β : α Type u_2} :
equiv.sigma_congr_right (λ (a : α), equiv.refl (β a)) = equiv.refl (Σ (a : α), β a)
def equiv.psigma_equiv_subtype {α : Type v} (P : α Prop) :
(Σ' (i : α), P i) subtype P

A psigma with Prop fibers is equivalent to the subtype.

Equations
def equiv.sigma_plift_equiv_subtype {α : Type v} (P : α Prop) :
(Σ (i : α), plift (P i)) subtype P

A sigma with plift fibers is equivalent to the subtype.

Equations
def equiv.sigma_ulift_plift_equiv_subtype {α : Type v} (P : α Prop) :
(Σ (i : α), ulift (plift (P i))) subtype P

A sigma with λ i, ulift (plift (P i)) fibers is equivalent to { x // P x }. Variant of sigma_plift_equiv_subtype.

Equations
@[reducible]
def equiv.perm.sigma_congr_right {α : Type u_1} {β : α Type u_2} (F : Π (a : α), equiv.perm (β a)) :
equiv.perm (Σ (a : α), β a)

A family of permutations Π a, perm (β a) generates a permuation perm (Σ a, β₁ a).

Equations
@[simp]
@[simp]
theorem equiv.perm.sigma_congr_right_symm {α : Type u_1} {β : α Type u_2} (F : Π (a : α), equiv.perm (β a)) :
@[simp]
theorem equiv.perm.sigma_congr_right_refl {α : Type u_1} {β : α Type u_2} :
equiv.perm.sigma_congr_right (λ (a : α), equiv.refl (β a)) = equiv.refl (Σ (a : α), β a)
@[simp]
theorem equiv.sigma_congr_left_apply {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ Type u_3} (e : α₁ α₂) (a : Σ (a : α₁), β (e a)) :
def equiv.sigma_congr_left {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ Type u_3} (e : α₁ α₂) :
(Σ (a : α₁), β (e a)) Σ (a : α₂), β a

An equivalence f : α₁ ≃ α₂ generates an equivalence between Σ a, β (f a) and Σ a, β a.

Equations
def equiv.sigma_congr_left' {α₁ : Type u_1} {α₂ : Type u_2} {β : α₁ Type u_3} (f : α₁ α₂) :
(Σ (a : α₁), β a) Σ (a : α₂), β ((f.symm) a)

Transporting a sigma type through an equivalence of the base

Equations
def equiv.sigma_congr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁ Type u_3} {β₂ : α₂ Type u_4} (f : α₁ α₂) (F : Π (a : α₁), β₁ a β₂ (f a)) :
sigma β₁ sigma β₂

Transporting a sigma type through an equivalence of the base and a family of equivalences of matching fibers

Equations
def equiv.sigma_equiv_prod (α : Type u_1) (β : Type u_2) :
(Σ (_x : α), β) α × β

sigma type with a constant fiber is equivalent to the product.

Equations
@[simp]
theorem equiv.sigma_equiv_prod_apply (α : Type u_1) (β : Type u_2) (a : Σ (_x : α), β) :
@[simp]
theorem equiv.sigma_equiv_prod_symm_apply (α : Type u_1) (β : Type u_2) (a : α × β) :
def equiv.sigma_equiv_prod_of_equiv {α : Type u_1} {β : Type u_2} {β₁ : α Type u_3} (F : Π (a : α), β₁ a β) :
sigma β₁ α × β

If each fiber of a sigma type is equivalent to a fixed type, then the sigma type is equivalent to the product.

Equations
def equiv.sigma_assoc {α : Type u_1} {β : α Type u_2} (γ : Π (a : α), β a Type u_3) :
(Σ (ab : Σ (a : α), β a), γ ab.fst ab.snd) Σ (a : α) (b : β a), γ a b

Dependent product of types is associative up to an equivalence.

Equations
@[protected]
theorem equiv.exists_unique_congr {α : Sort u} {β : Sort v} {p : α Prop} {q : β Prop} (f : α β) (h : {x : α}, p x q (f x)) :
(∃! (x : α), p x) ∃! (y : β), q y
@[protected]
theorem equiv.exists_unique_congr_left' {α : Sort u} {β : Sort v} {p : α Prop} (f : α β) :
(∃! (x : α), p x) ∃! (y : β), p ((f.symm) y)
@[protected]
theorem equiv.exists_unique_congr_left {α : Sort u} {β : Sort v} {p : β Prop} (f : α β) :
(∃! (x : α), p (f x)) ∃! (y : β), p y
@[protected]
theorem equiv.forall_congr {α : Sort u} {β : Sort v} {p : α Prop} {q : β Prop} (f : α β) (h : {x : α}, p x q (f x)) :
( (x : α), p x) (y : β), q y
@[protected]
theorem equiv.forall_congr' {α : Sort u} {β : Sort v} {p : α Prop} {q : β Prop} (f : α β) (h : {x : β}, p ((f.symm) x) q x) :
( (x : α), p x) (y : β), q y
@[protected]
theorem equiv.forall₂_congr {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {p : α₁ β₁ Prop} {q : α₂ β₂ Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (h : {x : α₁} {y : β₁}, p x y q (eα x) (eβ y)) :
( (x : α₁) (y : β₁), p x y) (x : α₂) (y : β₂), q x y
@[protected]
theorem equiv.forall₂_congr' {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {p : α₁ β₁ Prop} {q : α₂ β₂ Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (h : {x : α₂} {y : β₂}, p ((eα.symm) x) ((eβ.symm) y) q x y) :
( (x : α₁) (y : β₁), p x y) (x : α₂) (y : β₂), q x y
@[protected]
theorem equiv.forall₃_congr {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {γ₁ : Sort ug1} {γ₂ : Sort ug2} {p : α₁ β₁ γ₁ Prop} {q : α₂ β₂ γ₂ Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (eγ : γ₁ γ₂) (h : {x : α₁} {y : β₁} {z : γ₁}, p x y z q (eα x) (eβ y) (eγ z)) :
( (x : α₁) (y : β₁) (z : γ₁), p x y z) (x : α₂) (y : β₂) (z : γ₂), q x y z
@[protected]
theorem equiv.forall₃_congr' {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {γ₁ : Sort ug1} {γ₂ : Sort ug2} {p : α₁ β₁ γ₁ Prop} {q : α₂ β₂ γ₂ Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (eγ : γ₁ γ₂) (h : {x : α₂} {y : β₂} {z : γ₂}, p ((eα.symm) x) ((eβ.symm) y) ((eγ.symm) z) q x y z) :
( (x : α₁) (y : β₁) (z : γ₁), p x y z) (x : α₂) (y : β₂) (z : γ₂), q x y z
@[protected]
theorem equiv.forall_congr_left' {α : Sort u} {β : Sort v} {p : α Prop} (f : α β) :
( (x : α), p x) (y : β), p ((f.symm) y)
@[protected]
theorem equiv.forall_congr_left {α : Sort u} {β : Sort v} {p : β Prop} (f : α β) :
( (x : α), p (f x)) (y : β), p y
@[protected]
theorem equiv.exists_congr_left {α : Sort u_1} {β : Sort u_2} (f : α β) {p : α Prop} :
( (a : α), p a) (b : β), p ((f.symm) b)
@[protected]
def quot.congr {α : Sort u} {β : Sort v} {ra : α α Prop} {rb : β β Prop} (e : α β) (eq : (a₁ a₂ : α), ra a₁ a₂ rb (e a₁) (e a₂)) :
quot ra quot rb

An equivalence e : α ≃ β generates an equivalence between quotient spaces, if `ra a₁ a₂ ↔ rb (e a₁) (e a₂).

Equations
@[simp]
theorem quot.congr_mk {α : Sort u} {β : Sort v} {ra : α α Prop} {rb : β β Prop} (e : α β) (eq : (a₁ a₂ : α), ra a₁ a₂ rb (e a₁) (e a₂)) (a : α) :
(quot.congr e eq) (quot.mk ra a) = quot.mk rb (e a)
@[protected]
def quot.congr_right {α : Sort u} {r r' : α α Prop} (eq : (a₁ a₂ : α), r a₁ a₂ r' a₁ a₂) :
quot r quot r'

Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with eq, but then computational proofs get stuck.

Equations
@[protected]
def quot.congr_left {α : Sort u} {β : Sort v} {r : α α Prop} (e : α β) :
quot r quot (λ (b b' : β), r ((e.symm) b) ((e.symm) b'))

An equivalence e : α ≃ β generates an equivalence between the quotient space of α by a relation ra and the quotient space of β by the image of this relation under e.

Equations
@[protected]
def quotient.congr {α : Sort u} {β : Sort v} {ra : setoid α} {rb : setoid β} (e : α β) (eq : (a₁ a₂ : α), setoid.r a₁ a₂ setoid.r (e a₁) (e a₂)) :

An equivalence e : α ≃ β generates an equivalence between quotient spaces, if `ra a₁ a₂ ↔ rb (e a₁) (e a₂).

Equations
@[simp]
theorem quotient.congr_mk {α : Sort u} {β : Sort v} {ra : setoid α} {rb : setoid β} (e : α β) (eq : (a₁ a₂ : α), setoid.r a₁ a₂ setoid.r (e a₁) (e a₂)) (a : α) :
@[protected]
def quotient.congr_right {α : Sort u} {r r' : setoid α} (eq : (a₁ a₂ : α), setoid.r a₁ a₂ setoid.r a₁ a₂) :

Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with eq, but then computational proofs get stuck.

Equations