mathlib3 documentation

logic.equiv.basic

Equivalence between types #

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

In this file we continue the work on equivalences begun in logic/equiv/defs.lean, defining

Tags #

equivalence, congruence, bijective map

@[simp]
theorem equiv.pprod_equiv_prod_symm_apply {α : Type u_1} {β : Type u_2} (x : α × β) :
@[simp]
theorem equiv.pprod_equiv_prod_apply {α : Type u_1} {β : Type u_2} (x : pprod α β) :
def equiv.pprod_equiv_prod {α : Type u_1} {β : Type u_2} :
pprod α β α × β

pprod α β is equivalent to α × β

Equations
def equiv.pprod_congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort z} (e₁ : α β) (e₂ : γ δ) :
pprod α γ pprod β δ

Product of two equivalences, in terms of pprod. If α ≃ β and γ ≃ δ, then pprod α γ ≃ pprod β δ.

Equations
@[simp]
theorem equiv.pprod_congr_apply {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort z} (e₁ : α β) (e₂ : γ δ) (x : pprod α γ) :
(e₁.pprod_congr e₂) x = e₁ x.fst, e₂ x.snd
@[simp]
theorem equiv.pprod_prod_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Type u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) (ᾰ : pprod α₁ β₁) :
(ea.pprod_prod eb) = (ea ᾰ.fst, eb ᾰ.snd)
@[simp]
theorem equiv.pprod_prod_symm_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Type u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) (ᾰ : α₂ × β₂) :
((ea.pprod_prod eb).symm) = ((ea.pprod_congr eb).symm) ᾰ.fst, ᾰ.snd
def equiv.pprod_prod {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Type u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
pprod α₁ β₁ α₂ × β₂

Combine two equivalences using pprod in the domain and prod in the codomain.

Equations
def equiv.prod_pprod {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
α₁ × β₁ pprod α₂ β₂

Combine two equivalences using pprod in the codomain and prod in the domain.

Equations
@[simp]
theorem equiv.prod_pprod_symm_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (ea : α₁ α₂) (eb : β₁ β₂) (ᾰ : pprod α₂ β₂) :
((ea.prod_pprod eb).symm) = ((ea.symm) ᾰ.fst, (eb.symm) ᾰ.snd)
@[simp]
theorem equiv.prod_pprod_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (ea : α₁ α₂) (eb : β₁ β₂) (ᾰ : α₁ × β₁) :
(ea.prod_pprod eb) = ((ea.symm.pprod_congr eb.symm).symm) ᾰ.fst, ᾰ.snd
def equiv.pprod_equiv_prod_plift {α : Sort u_1} {β : Sort u_2} :
pprod α β plift α × plift β

pprod α β is equivalent to plift α × plift β

Equations
@[simp]
theorem equiv.pprod_equiv_prod_plift_apply {α : Sort u_1} {β : Sort u_2} (ᾰ : pprod α β) :
def equiv.prod_congr {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
α₁ × β₁ α₂ × β₂

Product of two equivalences. If α₁ ≃ α₂ and β₁ ≃ β₂, then α₁ × β₁ ≃ α₂ × β₂. This is prod.map as an equivalence.

Equations
@[simp]
theorem equiv.prod_congr_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(e₁.prod_congr e₂) = prod.map e₁ e₂
@[simp]
theorem equiv.prod_congr_symm {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(e₁.prod_congr e₂).symm = e₁.symm.prod_congr e₂.symm
def equiv.prod_comm (α : Type u_1) (β : Type u_2) :
α × β β × α

Type product is commutative up to an equivalence: α × β ≃ β × α. This is prod.swap as an equivalence.

Equations
@[simp]
theorem equiv.coe_prod_comm (α : Type u_1) (β : Type u_2) :
@[simp]
theorem equiv.prod_comm_apply {α : Type u_1} {β : Type u_2} (x : α × β) :
@[simp]
theorem equiv.prod_comm_symm (α : Type u_1) (β : Type u_2) :
@[simp]
theorem equiv.prod_assoc_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ) :
((equiv.prod_assoc α β γ).symm) p = ((p.fst, p.snd.fst), p.snd.snd)
def equiv.prod_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
× β) × γ α × β × γ

Type product is associative up to an equivalence.

Equations
@[simp]
theorem equiv.prod_assoc_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : × β) × γ) :
(equiv.prod_assoc α β γ) p = (p.fst.fst, p.fst.snd, p.snd)
@[simp]
theorem equiv.prod_prod_prod_comm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (δ : Type u_4) (abcd : × β) × γ × δ) :
(equiv.prod_prod_prod_comm α β γ δ) abcd = ((abcd.fst.fst, abcd.snd.fst), abcd.fst.snd, abcd.snd.snd)
def equiv.prod_prod_prod_comm (α : Type u_1) (β : Type u_2) (γ : Type u_3) (δ : Type u_4) :
× β) × γ × δ × γ) × β × δ

Four-way commutativity of prod. The name matches mul_mul_mul_comm.

Equations
@[simp]
theorem equiv.prod_prod_prod_comm_symm (α : Type u_1) (β : Type u_2) (γ : Type u_3) (δ : Type u_4) :
@[simp]
theorem equiv.curry_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
def equiv.curry (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
× β γ) β γ)

Functions on α × β are equivalent to functions α → β → γ.

Equations
@[simp]
theorem equiv.curry_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
def equiv.prod_punit (α : Type u_1) :
α × punit α

punit is a right identity for type product up to an equivalence.

Equations
@[simp]
theorem equiv.prod_punit_apply (α : Type u_1) (p : α × punit) :
@[simp]
theorem equiv.prod_punit_symm_apply (α : Type u_1) (a : α) :
((equiv.prod_punit α).symm) a = (a, punit.star)
def equiv.punit_prod (α : Type u_1) :
punit × α α

punit is a left identity for type product up to an equivalence.

Equations
@[simp]
theorem equiv.punit_prod_symm_apply (α : Type u_1) (ᾰ : α) :
((equiv.punit_prod α).symm) = (punit.star, ᾰ)
@[simp]
theorem equiv.punit_prod_apply (α : Type u_1) (ᾰ : punit × α) :
def equiv.prod_unique (α : Type u_1) (β : Type u_2) [unique β] :
α × β α

Any unique type is a right identity for type product up to equivalence.

Equations
@[simp]
theorem equiv.coe_prod_unique {α : Type u_1} {β : Type u_2} [unique β] :
theorem equiv.prod_unique_apply {α : Type u_1} {β : Type u_2} [unique β] (x : α × β) :
@[simp]
theorem equiv.prod_unique_symm_apply {α : Type u_1} {β : Type u_2} [unique β] (x : α) :
def equiv.unique_prod (α : Type u_1) (β : Type u_2) [unique β] :
β × α α

Any unique type is a left identity for type product up to equivalence.

Equations
@[simp]
theorem equiv.coe_unique_prod {α : Type u_1} {β : Type u_2} [unique β] :
theorem equiv.unique_prod_apply {α : Type u_1} {β : Type u_2} [unique β] (x : β × α) :
@[simp]
theorem equiv.unique_prod_symm_apply {α : Type u_1} {β : Type u_2} [unique β] (x : α) :
def equiv.prod_empty (α : Type u_1) :

empty type is a right absorbing element for type product up to an equivalence.

Equations
def equiv.empty_prod (α : Type u_1) :

empty type is a left absorbing element for type product up to an equivalence.

Equations
def equiv.prod_pempty (α : Type u_1) :

pempty type is a right absorbing element for type product up to an equivalence.

Equations
def equiv.pempty_prod (α : Type u_1) :

pempty type is a left absorbing element for type product up to an equivalence.

Equations
def equiv.psum_equiv_sum (α : Type u_1) (β : Type u_2) :
psum α β α β

psum is equivalent to sum.

Equations
@[simp]
theorem equiv.sum_congr_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) (ᾰ : α₁ β₁) :
(ea.sum_congr eb) = sum.map ea eb
def equiv.sum_congr {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
α₁ β₁ α₂ β₂

If α ≃ α' and β ≃ β', then α ⊕ β ≃ α' ⊕ β'. This is sum.map as an equivalence.

Equations
def equiv.psum_congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort z} (e₁ : α β) (e₂ : γ δ) :
psum α γ psum β δ

If α ≃ α' and β ≃ β', then psum α β ≃ psum α' β'.

Equations
def equiv.psum_sum {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Type u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
psum α₁ β₁ α₂ β₂

Combine two equivs using psum in the domain and sum in the codomain.

Equations
def equiv.sum_psum {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
α₁ β₁ psum α₂ β₂

Combine two equivs using sum in the domain and psum in the codomain.

Equations
@[simp]
theorem equiv.sum_congr_trans {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} (e : α₁ β₁) (f : α₂ β₂) (g : β₁ γ₁) (h : β₂ γ₂) :
(e.sum_congr f).trans (g.sum_congr h) = (e.trans g).sum_congr (f.trans h)
@[simp]
theorem equiv.sum_congr_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α β) (f : γ δ) :
@[simp]
theorem equiv.sum_congr_refl {α : Type u_1} {β : Type u_2} :
@[reducible]
def equiv.perm.sum_congr {α : Type u_1} {β : Type u_2} (ea : equiv.perm α) (eb : equiv.perm β) :
equiv.perm β)

Combine a permutation of α and of β into a permutation of α ⊕ β.

Equations
@[simp]
theorem equiv.perm.sum_congr_apply {α : Type u_1} {β : Type u_2} (ea : equiv.perm α) (eb : equiv.perm β) (x : α β) :
(ea.sum_congr eb) x = sum.map ea eb x
@[simp]
theorem equiv.perm.sum_congr_trans {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (f : equiv.perm β) (g : equiv.perm α) (h : equiv.perm β) :
@[simp]
theorem equiv.perm.sum_congr_symm {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (f : equiv.perm β) :
@[simp]
theorem equiv.perm.sum_congr_refl {α : Type u_1} {β : Type u_2} :

bool is equivalent the sum of two punits.

Equations
@[simp]
theorem equiv.sum_comm_apply (α : Type u_1) (β : Type u_2) :
def equiv.sum_comm (α : Type u_1) (β : Type u_2) :
α β β α

Sum of types is commutative up to an equivalence. This is sum.swap as an equivalence.

Equations
@[simp]
theorem equiv.sum_comm_symm (α : Type u_1) (β : Type u_2) :
def equiv.sum_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
β) γ α β γ

Sum of types is associative up to an equivalence.

Equations
@[simp]
theorem equiv.sum_assoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) :
@[simp]
theorem equiv.sum_assoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :
@[simp]
theorem equiv.sum_assoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :
@[simp]
theorem equiv.sum_assoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) :
@[simp]
theorem equiv.sum_assoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :
@[simp]
theorem equiv.sum_assoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :
def equiv.sum_empty (α : Type u_1) (β : Type u_2) [is_empty β] :
α β α

Sum with empty is equivalent to the original type.

Equations
@[simp]
theorem equiv.sum_empty_symm_apply (α : Type u_1) (β : Type u_2) [is_empty β] (val : α) :
((equiv.sum_empty α β).symm) val = sum.inl val
@[simp]
theorem equiv.sum_empty_apply_inl {α : Type u_1} {β : Type u_2} [is_empty β] (a : α) :
def equiv.empty_sum (α : Type u_1) (β : Type u_2) [is_empty α] :
α β β

The sum of empty with any Sort* is equivalent to the right summand.

Equations
@[simp]
theorem equiv.empty_sum_symm_apply (α : Type u_1) (β : Type u_2) [is_empty α] (ᾰ : β) :
((equiv.empty_sum α β).symm) = sum.inr
@[simp]
theorem equiv.empty_sum_apply_inr {α : Type u_1} {β : Type u_2} [is_empty α] (b : β) :

option α is equivalent to α ⊕ punit

Equations
@[simp]
def equiv.option_is_some_equiv (α : Type u_1) :
{x // (x.is_some)} α

The set of x : option α such that is_some x is equivalent to α.

Equations
@[simp]
theorem equiv.pi_option_equiv_prod_apply {α : Type u_1} {β : option α Type u_2} (f : Π (a : option α), β a) :
@[simp]
theorem equiv.pi_option_equiv_prod_symm_apply {α : Type u_1} {β : option α Type u_2} (x : β option.none × Π (a : α), β (option.some a)) (a : option α) :
def equiv.pi_option_equiv_prod {α : Type u_1} {β : option α Type u_2} :
(Π (a : option α), β a) β option.none × Π (a : α), β (option.some a)

The product over option α of β a is the binary product of the product over α of β (some α) and β none

Equations
def equiv.sum_equiv_sigma_bool (α β : Type u) :
α β Σ (b : bool), cond b α β

α ⊕ β is equivalent to a sigma-type over bool. Note that this definition assumes α and β to be types from the same universe, so it cannot by used directly to transfer theorems about sigma types to theorems about sum types. In many cases one can use ulift to work around this difficulty.

Equations
@[simp]
theorem equiv.sigma_fiber_equiv_apply {α : Type u_1} {β : Type u_2} (f : α β) (x : Σ (y : β), {x // f x = y}) :
@[simp]
theorem equiv.sigma_fiber_equiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
@[simp]
theorem equiv.sigma_fiber_equiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
def equiv.sigma_fiber_equiv {α : Type u_1} {β : Type u_2} (f : α β) :
(Σ (y : β), {x // f x = y}) α

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

Equations
def equiv.sum_compl {α : Type u_1} (p : α Prop) [decidable_pred p] :
{a // p a} {a // ¬p a} α

For any predicate p on α, the sum of the two subtypes {a // p a} and its complement {a // ¬ p a} is naturally equivalent to α.

See subtype_or_equiv for sum types over subtypes {x // p x} and {x // q x} that are not necessarily is_compl p q.

Equations
@[simp]
theorem equiv.sum_compl_apply_inl {α : Type u_1} (p : α Prop) [decidable_pred p] (x : {a // p a}) :
@[simp]
theorem equiv.sum_compl_apply_inr {α : Type u_1} (p : α Prop) [decidable_pred p] (x : {a // ¬p a}) :
@[simp]
theorem equiv.sum_compl_apply_symm_of_pos {α : Type u_1} (p : α Prop) [decidable_pred p] (a : α) (h : p a) :
@[simp]
theorem equiv.sum_compl_apply_symm_of_neg {α : Type u_1} (p : α Prop) [decidable_pred p] (a : α) (h : ¬p a) :
def equiv.subtype_congr {α : Type u_1} {p q : α Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} {x // q x}) (f : {x // ¬p x} {x // ¬q x}) :

Combines an equiv between two subtypes with an equiv between their complements to form a permutation.

Equations
def equiv.perm.subtype_congr {ε : Type u_1} {p : ε Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) :

Combining permutations on ε that permute only inside or outside the subtype split induced by p : ε → Prop constructs a permutation on ε.

Equations
theorem equiv.perm.subtype_congr.apply {ε : Type u_1} {p : ε Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) (a : ε) :
(ep.subtype_congr en) a = dite (p a) (λ (h : p a), (ep a, h⟩)) (λ (h : ¬p a), (en a, h⟩))
@[simp]
theorem equiv.perm.subtype_congr.left_apply {ε : Type u_1} {p : ε Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) {a : ε} (h : p a) :
(ep.subtype_congr en) a = (ep a, h⟩)
@[simp]
theorem equiv.perm.subtype_congr.left_apply_subtype {ε : Type u_1} {p : ε Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) (a : {a // p a}) :
(ep.subtype_congr en) a = (ep a)
@[simp]
theorem equiv.perm.subtype_congr.right_apply {ε : Type u_1} {p : ε Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) {a : ε} (h : ¬p a) :
(ep.subtype_congr en) a = (en a, h⟩)
@[simp]
theorem equiv.perm.subtype_congr.right_apply_subtype {ε : Type u_1} {p : ε Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) (a : {a // ¬p a}) :
(ep.subtype_congr en) a = (en a)
@[simp]
theorem equiv.perm.subtype_congr.refl {ε : Type u_1} {p : ε Prop} [decidable_pred p] :
@[simp]
theorem equiv.perm.subtype_congr.symm {ε : Type u_1} {p : ε Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) :
@[simp]
theorem equiv.perm.subtype_congr.trans {ε : Type u_1} {p : ε Prop} [decidable_pred p] (ep ep' : equiv.perm {a // p a}) (en en' : equiv.perm {a // ¬p a}) :
@[simp]
theorem equiv.subtype_preimage_symm_apply_coe {α : Sort u} {β : Sort v} (p : α Prop) [decidable_pred p] (x₀ : {a // p a} β) (x : {a // ¬p a} β) (a : α) :
(((equiv.subtype_preimage p x₀).symm) x) a = dite (p a) (λ (h : p a), x₀ a, h⟩) (λ (h : ¬p a), x a, h⟩)
@[simp]
theorem equiv.subtype_preimage_apply {α : Sort u} {β : Sort v} (p : α Prop) [decidable_pred p] (x₀ : {a // p a} β) (x : {x // x coe = x₀}) (a : {a // ¬p a}) :
def equiv.subtype_preimage {α : Sort u} {β : Sort v} (p : α Prop) [decidable_pred p] (x₀ : {a // p a} β) :
{x // x coe = x₀} ({a // ¬p a} β)

For a fixed function x₀ : {a // p a} → β defined on a subtype of α, the subtype of functions x : α → β that agree with x₀ on the subtype {a // p a} is naturally equivalent to the type of functions {a // ¬ p a} → β.

Equations
theorem equiv.subtype_preimage_symm_apply_coe_pos {α : Sort u} {β : Sort v} (p : α Prop) [decidable_pred p] (x₀ : {a // p a} β) (x : {a // ¬p a} β) (a : α) (h : p a) :
(((equiv.subtype_preimage p x₀).symm) x) a = x₀ a, h⟩
theorem equiv.subtype_preimage_symm_apply_coe_neg {α : Sort u} {β : Sort v} (p : α Prop) [decidable_pred p] (x₀ : {a // p a} β) (x : {a // ¬p a} β) (a : α) (h : ¬p a) :
(((equiv.subtype_preimage p x₀).symm) x) a = x a, h⟩
def equiv.Pi_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
def equiv.Pi_comm {α : Sort u_1} {β : Sort u_2} (φ : α β Sort u_3) :
(Π (a : α) (b : β), φ a b) Π (b : β) (a : α), φ a b

Given φ : α → β → Sort*, we have an equivalence between Π a b, φ a b and Π b a, φ a b. This is function.swap as an equiv.

Equations
@[simp]
theorem equiv.Pi_comm_apply {α : Sort u_1} {β : Sort u_2} (φ : α β Sort u_3) (f : Π (x : α) (y : β), (λ (a : α) (b : β), φ a b) x y) (y : β) (x : α) :
@[simp]
theorem equiv.Pi_comm_symm {α : Sort u_1} {β : Sort u_2} {φ : α β Sort u_3} :
def equiv.Pi_curry {α : Type u_1} {β : α Type u_2} (γ : Π (a : α), β a Type u_3) :
(Π (x : Σ (i : α), β i), γ x.fst x.snd) Π (a : α) (b : β a), γ a b

Dependent curry equivalence: the type of dependent functions on Σ i, β i is equivalent to the type of dependent functions of two arguments (i.e., functions to the space of functions).

This is sigma.curry and sigma.uncurry together as an equiv.

Equations
def equiv.prod_congr_left {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) :
β₁ × α₁ β₂ × α₁

A family of equivalences Π (a : α₁), β₁ ≃ β₂ generates an equivalence between β₁ × α₁ and β₂ × α₁.

Equations
@[simp]
theorem equiv.prod_congr_left_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) (b : β₁) (a : α₁) :
(equiv.prod_congr_left e) (b, a) = ((e a) b, a)
theorem equiv.prod_congr_refl_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : β₁ β₂) :
e.prod_congr (equiv.refl α₁) = equiv.prod_congr_left (λ (_x : α₁), e)
def equiv.prod_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) :
α₁ × β₁ α₁ × β₂

A family of equivalences Π (a : α₁), β₁ ≃ β₂ generates an equivalence between α₁ × β₁ and α₁ × β₂.

Equations
@[simp]
theorem equiv.prod_congr_right_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) (a : α₁) (b : β₁) :
(equiv.prod_congr_right e) (a, b) = (a, (e a) b)
theorem equiv.prod_congr_refl_left {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : β₁ β₂) :
(equiv.refl α₁).prod_congr e = equiv.prod_congr_right (λ (_x : α₁), e)
@[simp]
theorem equiv.prod_congr_left_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) :
@[simp]
theorem equiv.prod_congr_right_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) :
theorem equiv.sigma_congr_right_sigma_equiv_prod {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) :
theorem equiv.sigma_equiv_prod_sigma_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) :
@[simp]
theorem equiv.of_fiber_equiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α γ} {g : β γ} (e : Π (c : γ), {a // f a = c} {b // g b = c}) (ᾰ : β) :
@[simp]
theorem equiv.of_fiber_equiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α γ} {g : β γ} (e : Π (c : γ), {a // f a = c} {b // g b = c}) (ᾰ : α) :
def equiv.of_fiber_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α γ} {g : β γ} (e : Π (c : γ), {a // f a = c} {b // g b = c}) :
α β

A family of equivalences between fibers gives an equivalence between domains.

Equations
theorem equiv.of_fiber_equiv_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α γ} {g : β γ} (e : Π (c : γ), {a // f a = c} {b // g b = c}) (a : α) :
@[simp]
theorem equiv.prod_shear_symm_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : α₁ β₁ β₂) :
((e₁.prod_shear e₂).symm) = λ (y : α₂ × β₂), ((e₁.symm) y.fst, ((e₂ ((e₁.symm) y.fst)).symm) y.snd)
@[simp]
theorem equiv.prod_shear_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : α₁ β₁ β₂) :
(e₁.prod_shear e₂) = λ (x : α₁ × β₁), (e₁ x.fst, (e₂ x.fst) x.snd)
def equiv.prod_shear {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : α₁ β₁ β₂) :
α₁ × β₁ α₂ × β₂

A variation on equiv.prod_congr where the equivalence in the second component can depend on the first component. A typical example is a shear mapping, explaining the name of this declaration.

Equations
def equiv.perm.prod_extend_right {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) :
equiv.perm (α₁ × β₁)

prod_extend_right a e extends e : perm β to perm (α × β) by sending (a, b) to (a, e b) and keeping the other (a', b) fixed.

Equations
@[simp]
theorem equiv.perm.prod_extend_right_apply_eq {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (b : β₁) :
theorem equiv.perm.prod_extend_right_apply_ne {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (e : equiv.perm β₁) {a a' : α₁} (h : a' a) (b : β₁) :
(equiv.perm.prod_extend_right a e) (a', b) = (a', b)
theorem equiv.perm.eq_of_prod_extend_right_ne {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] {e : equiv.perm β₁} {a a' : α₁} {b : β₁} (h : (equiv.perm.prod_extend_right a e) (a', b) (a', b)) :
a' = a
@[simp]
theorem equiv.perm.fst_prod_extend_right {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (ab : α₁ × β₁) :
def equiv.arrow_prod_equiv_prod_arrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
α × β) α) × β)

The type of functions to a product α × β is equivalent to the type of pairs of functions γ → α and γ → β.

Equations
def equiv.sum_arrow_equiv_prod_arrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
β γ) γ) × γ)

The type of functions on a sum type α ⊕ β is equivalent to the type of pairs of functions on α and on β.

Equations
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_apply_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) (a : α) :
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_apply_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) (b : β) :
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α γ) (g : β γ) (a : α) :
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_symm_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α γ) (g : β γ) (b : β) :
def equiv.sum_prod_distrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
β) × γ α × γ β × γ

Type product is right distributive with respect to type sum up to an equivalence.

Equations
@[simp]
theorem equiv.sum_prod_distrib_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (c : γ) :
(equiv.sum_prod_distrib α β γ) (sum.inl a, c) = sum.inl (a, c)
@[simp]
theorem equiv.sum_prod_distrib_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) (c : γ) :
(equiv.sum_prod_distrib α β γ) (sum.inr b, c) = sum.inr (b, c)
@[simp]
theorem equiv.sum_prod_distrib_symm_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α × γ) :
@[simp]
theorem equiv.sum_prod_distrib_symm_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β × γ) :
def equiv.prod_sum_distrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
α × γ) α × β α × γ

Type product is left distributive with respect to type sum up to an equivalence.

Equations
@[simp]
theorem equiv.prod_sum_distrib_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (b : β) :
(equiv.prod_sum_distrib α β γ) (a, sum.inl b) = sum.inl (a, b)
@[simp]
theorem equiv.prod_sum_distrib_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (c : γ) :
(equiv.prod_sum_distrib α β γ) (a, sum.inr c) = sum.inr (a, c)
@[simp]
theorem equiv.prod_sum_distrib_symm_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α × β) :
@[simp]
theorem equiv.prod_sum_distrib_symm_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α × γ) :
@[simp]
theorem equiv.sigma_sum_distrib_apply {ι : Type u_1} (α : ι Type u_2) (β : ι Type u_3) (p : Σ (i : ι), α i β i) :
def equiv.sigma_sum_distrib {ι : Type u_1} (α : ι Type u_2) (β : ι Type u_3) :
(Σ (i : ι), α i β i) (Σ (i : ι), α i) Σ (i : ι), β i

An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums.

Equations
@[simp]
theorem equiv.sigma_sum_distrib_symm_apply {ι : Type u_1} (α : ι Type u_2) (β : ι Type u_3) (ᾰ : (Σ (i : ι), α i) Σ (i : ι), β i) :
((equiv.sigma_sum_distrib α β).symm) = sum.elim (sigma.map id (λ (_x : ι), sum.inl)) (sigma.map id (λ (_x : ι), sum.inr))
def equiv.sigma_prod_distrib {ι : Type u_1} (α : ι Type u_2) (β : Type u_3) :
(Σ (i : ι), α i) × β Σ (i : ι), α i × β

The product of an indexed sum of types (formally, a sigma-type Σ i, α i) by a type β is equivalent to the sum of products Σ i, (α i × β).

Equations
def equiv.sigma_nat_succ (f : Type u) :
(Σ (n : ), f n) f 0 Σ (n : ), f (n + 1)

An equivalence that separates out the 0th fiber of (Σ (n : ℕ), f n).

Equations
def equiv.bool_prod_equiv_sum (α : Type u) :
bool × α α α

The product bool × α is equivalent to α ⊕ α.

Equations
def equiv.bool_arrow_equiv_prod (α : Type u) :
(bool α) α × α

The function type bool → α is equivalent to α × α.

Equations
@[simp]
theorem equiv.bool_arrow_equiv_prod_symm_apply (α : Type u) (p : α × α) (b : bool) :

The set of natural numbers is equivalent to ℕ ⊕ punit.

Equations

The type of integer numbers is equivalent to ℕ ⊕ ℕ.

Equations
def equiv.list_equiv_of_equiv {α : Type u_1} {β : Type u_2} (e : α β) :
list α list β

An equivalence between α and β generates an equivalence between list α and list β.

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

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

Equations
theorem equiv.is_empty_congr {α : Sort u} {β : Sort v} (e : α β) :

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

@[protected]
theorem equiv.is_empty {α : Sort u} {β : Sort v} (e : α β) [is_empty β] :
def equiv.subtype_equiv {α : Sort u} {β : Sort v} {p : α Prop} {q : β Prop} (e : α β) (h : (a : α), p a q (e a)) :
{a // p a} {b // q b}

If α is equivalent to β and the predicates p : α → Prop and q : β → Prop are equivalent at corresponding points, then {a // p a} is equivalent to {b // q b}. For the statement where α = β, that is, e : perm α, see perm.subtype_perm.

Equations
@[simp]
theorem equiv.subtype_equiv_refl {α : Sort u} {p : α Prop} (h : ( (a : α), p a p ((equiv.refl α) a)) := _) :
@[simp]
theorem equiv.subtype_equiv_symm {α : Sort u} {β : Sort v} {p : α Prop} {q : β Prop} (e : α β) (h : (a : α), p a q (e a)) :
@[simp]
theorem equiv.subtype_equiv_trans {α : Sort u} {β : Sort v} {γ : Sort w} {p : α Prop} {q : β Prop} {r : γ Prop} (e : α β) (f : β γ) (h : (a : α), p a q (e a)) (h' : (b : β), q b r (f b)) :
@[simp]
theorem equiv.subtype_equiv_apply {α : Sort u} {β : Sort v} {p : α Prop} {q : β Prop} (e : α β) (h : (a : α), p a q (e a)) (x : {x // p x}) :
(e.subtype_equiv h) x = e x, _⟩
@[simp]
theorem equiv.subtype_equiv_right_symm_apply_coe {α : Sort u} {p q : α Prop} (e : (x : α), p x q x) (b : {b // (λ (x : α), q x) b}) :
def equiv.subtype_equiv_right {α : Sort u} {p q : α Prop} (e : (x : α), p x q x) :
{x // p x} {x // q x}

If two predicates p and q are pointwise equivalent, then {x // p x} is equivalent to {x // q x}.

Equations
@[simp]
theorem equiv.subtype_equiv_right_apply_coe {α : Sort u} {p q : α Prop} (e : (x : α), p x q x) (a : {a // (λ (x : α), p x) a}) :
def equiv.subtype_equiv_of_subtype {α : Sort u} {β : Sort v} {p : β Prop} (e : α β) :
{a // p (e a)} {b // p b}

If α ≃ β, then for any predicate p : β → Prop the subtype {a // p (e a)} is equivalent to the subtype {b // p b}.

Equations
def equiv.subtype_equiv_of_subtype' {α : Sort u} {β : Sort v} {p : α Prop} (e : α β) :
{a // p a} {b // p ((e.symm) b)}

If α ≃ β, then for any predicate p : α → Prop the subtype {a // p a} is equivalent to the subtype {b // p (e.symm b)}. This version is used by equiv_rw.

Equations
def equiv.subtype_equiv_prop {α : Sort u_1} {p q : α Prop} (h : p = q) :

If two predicates are equal, then the corresponding subtypes are equivalent.

Equations
def equiv.subtype_subtype_equiv_subtype_exists {α : Sort u} (p : α Prop) (q : subtype p Prop) :
subtype q {a // (h : p a), q a, h⟩}

A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. This version allows the “inner” predicate to depend on h : p a.

Equations
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_exists_symm_apply_coe_coe {α : Sort u} (p : α Prop) (q : subtype p Prop) (a : {a // (h : p a), q a, h⟩}) :
def equiv.subtype_subtype_equiv_subtype_inter {α : Sort u} (p q : α Prop) :
{x // q x.val} {x // p x q x}

A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates.

Equations
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_inter_apply_coe {α : Sort u} (p q : α Prop) (ᾰ : {x // q x.val}) :
@[simp]
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_symm_apply_coe_coe {α : Type u} {p q : α Prop} (h : {x : α}, q x p x) (ᾰ : subtype q) :
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_apply_coe {α : Type u} {p q : α Prop} (h : {x : α}, q x p x) (ᾰ : {x // q x.val}) :
def equiv.subtype_subtype_equiv_subtype {α : Type u} {p q : α Prop} (h : {x : α}, q x p x) :
{x // q x.val} subtype q

If the outer subtype has more restrictive predicate than the inner one, then we can drop the latter.

Equations
def equiv.subtype_univ_equiv {α : Type u} {p : α Prop} (h : (x : α), p x) :

If a proposition holds for all elements, then the subtype is equivalent to the original type.

Equations
@[simp]
theorem equiv.subtype_univ_equiv_symm_apply {α : Type u} {p : α Prop} (h : (x : α), p x) (x : α) :
@[simp]
theorem equiv.subtype_univ_equiv_apply {α : Type u} {p : α Prop} (h : (x : α), p x) (x : subtype p) :
def equiv.subtype_sigma_equiv {α : Type u} (p : α Type v) (q : α Prop) :
{y // q y.fst} Σ (x : subtype q), p x.val

A subtype of a sigma-type is a sigma-type over a subtype.

Equations
def equiv.sigma_subtype_equiv_of_subset {α : Type u} (p : α Type v) (q : α Prop) (h : (x : α), p x q x) :
(Σ (x : subtype q), p x) Σ (x : α), p x

A sigma type over a subtype is equivalent to the sigma set over the original type, if the fiber is empty outside of the subset

Equations
def equiv.sigma_subtype_fiber_equiv {α : Type u} {β : Type v} (f : α β) (p : β Prop) (h : (x : α), p (f x)) :
(Σ (y : subtype p), {x // f x = y}) α

If a predicate p : β → Prop is true on the range of a map f : α → β, then Σ y : {y // p y}, {x // f x = y} is equivalent to α.

Equations
def equiv.sigma_subtype_fiber_equiv_subtype {α : Type u} {β : Type v} (f : α β) {p : α Prop} {q : β Prop} (h : (x : α), p x q (f x)) :
(Σ (y : subtype q), {x // f x = y}) subtype p

If for each x we have p x ↔ q (f x), then Σ y : {y // q y}, f ⁻¹' {y} is equivalent to {x // p x}.

Equations
def equiv.sigma_option_equiv_of_some {α : Type u} (p : option α Type v) (h : p option.none false) :
(Σ (x : option α), p x) Σ (x : α), p (option.some x)

A sigma type over an option is equivalent to the sigma set over the original type, if the fiber is empty at none.

Equations
def equiv.pi_equiv_subtype_sigma (ι : Type u_1) (π : ι Type u_2) :
(Π (i : ι), π i) {f // (i : ι), (f i).fst = i}

The pi-type Π i, π i is equivalent to the type of sections f : ι → Σ i, π i of the sigma type such that for all i we have (f i).fst = i.

Equations
def equiv.subtype_pi_equiv_pi {α : Sort u} {β : α Sort v} {p : Π (a : α), β a Prop} :
{f // (a : α), p a (f a)} Π (a : α), {b // p a b}

The set of functions f : Π a, β a such that for all a we have p a (f a) is equivalent to the set of functions Π a, {b : β a // p a b}.

Equations
def equiv.subtype_prod_equiv_prod {α : Type u} {β : Type v} {p : α Prop} {q : β Prop} :
{c // p c.fst q c.snd} {a // p a} × {b // q b}

A subtype of a product defined by componentwise conditions is equivalent to a product of subtypes.

Equations
def equiv.subtype_prod_equiv_sigma_subtype {α : Type u_1} {β : Type u_2} (p : α β Prop) :
{x // p x.fst x.snd} Σ (a : α), {b // p a b}

A subtype of a prod is equivalent to a sigma type whose fibers are subtypes.

Equations
def equiv.pi_equiv_pi_subtype_prod {α : Type u_1} (p : α Prop) (β : α Type u_2) [decidable_pred p] :
(Π (i : α), β i) (Π (i : {x // p x}), β i) × Π (i : {x // ¬p x}), β i

The type Π (i : α), β i can be split as a product by separating the indices in α depending on whether they satisfy a predicate p or not.

Equations
@[simp]
theorem equiv.pi_equiv_pi_subtype_prod_symm_apply {α : Type u_1} (p : α Prop) (β : α Type u_2) [decidable_pred p] (f : (Π (i : {x // p x}), β i) × Π (i : {x // ¬p x}), β i) (x : α) :
((equiv.pi_equiv_pi_subtype_prod p β).symm) f x = dite (p x) (λ (h : p x), f.fst x, h⟩) (λ (h : ¬p x), f.snd x, h⟩)
@[simp]
theorem equiv.pi_equiv_pi_subtype_prod_apply {α : Type u_1} (p : α Prop) (β : α Type u_2) [decidable_pred p] (f : Π (i : α), β i) :
(equiv.pi_equiv_pi_subtype_prod p β) f = (λ (x : {x // p x}), f x, λ (x : {x // ¬p x}), f x)
@[simp]
theorem equiv.pi_split_at_symm_apply {α : Type u_1} [decidable_eq α] (i : α) (β : α Type u_2) (f : β i × Π (j : {j // j i}), β j) (j : α) :
((equiv.pi_split_at i β).symm) f j = dite (j = i) (λ (h : j = i), eq.rec f.fst _) (λ (h : ¬j = i), f.snd j, h⟩)
def equiv.pi_split_at {α : Type u_1} [decidable_eq α] (i : α) (β : α Type u_2) :
(Π (j : α), β j) β i × Π (j : {j // j i}), β j

A product of types can be split as the binary product of one of the types and the product of all the remaining types.

Equations
@[simp]
theorem equiv.pi_split_at_apply {α : Type u_1} [decidable_eq α] (i : α) (β : α Type u_2) (f : Π (j : α), β j) :
(equiv.pi_split_at i β) f = (f i, λ (j : {j // j i}), f j)
def equiv.fun_split_at {α : Type u_1} [decidable_eq α] (i : α) (β : Type u_2) :
β) β × ({j // j i} β)

A product of copies of a type can be split as the binary product of one copy and the product of all the remaining copies.

Equations
@[simp]
theorem equiv.fun_split_at_symm_apply {α : Type u_1} [decidable_eq α] (i : α) (β : Type u_2) (f : (λ (ᾰ : α), β) i × Π (j : {j // j i}), (λ (ᾰ : α), β) j) (j : α) :
((equiv.fun_split_at i β).symm) f j = dite (j = i) (λ (h : j = i), f.fst) (λ (h : ¬j = i), f.snd j, h⟩)
@[simp]
theorem equiv.fun_split_at_apply {α : Type u_1} [decidable_eq α] (i : α) (β : Type u_2) (f : Π (j : α), (λ (ᾰ : α), β) j) :
(equiv.fun_split_at i β) f = (f i, λ (j : {j // ¬j = i}), f j)
def equiv.subtype_equiv_codomain {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} Y) :
{g // g coe = f} Y

The type of all functions X → Y with prescribed values for all x' ≠ x is equivalent to the codomain Y.

Equations
@[simp]
theorem equiv.coe_subtype_equiv_codomain {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} Y) :
(equiv.subtype_equiv_codomain f) = λ (g : {g // g coe = f}), g x
@[simp]
theorem equiv.subtype_equiv_codomain_apply {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} Y) (g : {g // g coe = f}) :
theorem equiv.coe_subtype_equiv_codomain_symm {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} Y) :
((equiv.subtype_equiv_codomain f).symm) = λ (y : Y), λ (x' : X), dite (x' x) (λ (h : x' x), f x', h⟩) (λ (h : ¬x' x), y), _⟩
@[simp]
theorem equiv.subtype_equiv_codomain_symm_apply {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} Y) (y : Y) (x' : X) :
(((equiv.subtype_equiv_codomain f).symm) y) x' = dite (x' x) (λ (h : x' x), f x', h⟩) (λ (h : ¬x' x), y)
@[simp]
theorem equiv.subtype_equiv_codomain_symm_apply_eq {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} Y) (y : Y) :
theorem equiv.subtype_equiv_codomain_symm_apply_ne {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} Y) (y : Y) (x' : X) (h : x' x) :
noncomputable def equiv.of_bijective {α : Sort u} {β : Sort v} (f : α β) (hf : function.bijective f) :
α β

If f is a bijective function, then its domain is equivalent to its codomain.

Equations
@[simp]
theorem equiv.of_bijective_apply {α : Sort u} {β : Sort v} (f : α β) (hf : function.bijective f) (ᾰ : α) :
(equiv.of_bijective f hf) = f ᾰ
theorem equiv.of_bijective_apply_symm_apply {α : Sort u} {β : Sort v} (f : α β) (hf : function.bijective f) (x : β) :
f (((equiv.of_bijective f hf).symm) x) = x
@[simp]
theorem equiv.of_bijective_symm_apply_apply {α : Sort u} {β : Sort v} (f : α β) (hf : function.bijective f) (x : α) :
((equiv.of_bijective f hf).symm) (f x) = x
@[protected, instance]
Equations
def equiv.perm.extend_domain {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' Prop} [decidable_pred p] (f : α' subtype p) :

Extend the domain of e : equiv.perm α to one that is over β via f : α → subtype p, where p : β → Prop, permuting only the b : β that satisfy p b. This can be used to extend the domain across a function f : α → β, keeping everything outside of set.range f fixed. For this use-case equiv given by f can be constructed by equiv.of_left_inverse' or equiv.of_left_inverse when there is a known inverse, or equiv.of_injective in the general case.`.

Equations
@[simp]
theorem equiv.perm.extend_domain_apply_image {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' Prop} [decidable_pred p] (f : α' subtype p) (a : α') :
(e.extend_domain f) (f a) = (f (e a))
theorem equiv.perm.extend_domain_apply_subtype {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' Prop} [decidable_pred p] (f : α' subtype p) {b : β'} (h : p b) :
(e.extend_domain f) b = (f (e ((f.symm) b, h⟩)))
theorem equiv.perm.extend_domain_apply_not_subtype {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' Prop} [decidable_pred p] (f : α' subtype p) {b : β'} (h : ¬p b) :
@[simp]
theorem equiv.perm.extend_domain_refl {α' : Type u_1} {β' : Type u_2} {p : β' Prop} [decidable_pred p] (f : α' subtype p) :
@[simp]
theorem equiv.perm.extend_domain_symm {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' Prop} [decidable_pred p] (f : α' subtype p) :
theorem equiv.perm.extend_domain_trans {α' : Type u_1} {β' : Type u_2} {p : β' Prop} [decidable_pred p] (f : α' subtype p) (e e' : equiv.perm α') :
def equiv.subtype_quotient_equiv_quotient_subtype {α : Sort u} (p₁ : α Prop) [s₁ : setoid α] [s₂ : setoid (subtype p₁)] (p₂ : quotient s₁ Prop) (hp₂ : (a : α), p₁ a p₂ a) (h : (x y : subtype p₁), setoid.r x y x y) :
{x // p₂ x} quotient s₂

Subtype of the quotient is equivalent to the quotient of the subtype. Let α be a setoid with equivalence relation ~. Let p₂ be a predicate on the quotient type α/~, and p₁ be the lift of this predicate to α: p₁ a ↔ p₂ ⟦a⟧. Let ~₂ be the restriction of ~ to {x // p₁ x}. Then {x // p₂ x} is equivalent to the quotient of {x // p₁ x} by ~₂.

Equations
@[simp]
theorem equiv.subtype_quotient_equiv_quotient_subtype_mk {α : Sort u} (p₁ : α Prop) [s₁ : setoid α] [s₂ : setoid (subtype p₁)] (p₂ : quotient s₁ Prop) (hp₂ : (a : α), p₁ a p₂ a) (h : (x y : subtype p₁), setoid.r x y x y) (x : α) (hx : p₂ x) :
@[simp]
theorem equiv.subtype_quotient_equiv_quotient_subtype_symm_mk {α : Sort u} (p₁ : α Prop) [s₁ : setoid α] [s₂ : setoid (subtype p₁)] (p₂ : quotient s₁ Prop) (hp₂ : (a : α), p₁ a p₂ a) (h : (x y : subtype p₁), setoid.r x y x y) (x : subtype p₁) :
def equiv.swap_core {α : Sort u} [decidable_eq α] (a b r : α) :
α

A helper function for equiv.swap.

Equations
theorem equiv.swap_core_self {α : Sort u} [decidable_eq α] (r a : α) :
theorem equiv.swap_core_swap_core {α : Sort u} [decidable_eq α] (r a b : α) :
theorem equiv.swap_core_comm {α : Sort u} [decidable_eq α] (r a b : α) :
def equiv.swap {α : Sort u} [decidable_eq α] (a b : α) :

swap a b is the permutation that swaps a and b and leaves other values as is.

Equations
@[simp]
theorem equiv.swap_self {α : Sort u} [decidable_eq α] (a : α) :
theorem equiv.swap_comm {α : Sort u} [decidable_eq α] (a b : α) :
theorem equiv.swap_apply_def {α : Sort u} [decidable_eq α] (a b x : α) :
(equiv.swap a b) x = ite (x = a) b (ite (x = b) a x)
@[simp]
theorem equiv.swap_apply_left {α : Sort u} [decidable_eq α] (a b : α) :
(equiv.swap a b) a = b
@[simp]
theorem equiv.swap_apply_right {α : Sort u} [decidable_eq α] (a b : α) :
(equiv.swap a b) b = a
theorem equiv.swap_apply_of_ne_of_ne {α : Sort u} [decidable_eq α] {a b x : α} :
x a x b (equiv.swap a b) x = x
@[simp]
theorem equiv.swap_swap {α : Sort u} [decidable_eq α] (a b : α) :
@[simp]
theorem equiv.symm_swap {α : Sort u} [decidable_eq α] (a b : α) :
@[simp]
theorem equiv.swap_eq_refl_iff {α : Sort u} [decidable_eq α] {x y : α} :
theorem equiv.swap_comp_apply {α : Sort u} [decidable_eq α] {a b x : α} (π : equiv.perm α) :
(equiv.trans π (equiv.swap a b)) x = ite (π x = a) b (ite (π x = b) a (π x))
theorem equiv.swap_eq_update {α : Sort u} [decidable_eq α] (i j : α) :
theorem equiv.comp_swap_eq_update {α : Sort u} {β : Sort v} [decidable_eq α] (i j : α) (f : α β) :
f (equiv.swap i j) = function.update (function.update f j (f i)) i (f j)
@[simp]
theorem equiv.symm_trans_swap_trans {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] (a b : α) (e : α β) :
(e.symm.trans (equiv.swap a b)).trans e = equiv.swap (e a) (e b)
@[simp]
theorem equiv.trans_swap_trans_symm {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] (a b : β) (e : α β) :
(e.trans (equiv.swap a b)).trans e.symm = equiv.swap ((e.symm) a) ((e.symm) b)
@[simp]
theorem equiv.swap_apply_self {α : Sort u} [decidable_eq α] (i j a : α) :
(equiv.swap i j) ((equiv.swap i j) a) = a
theorem equiv.apply_swap_eq_self {α : Sort u} {β : Sort v} [decidable_eq α] {v : α β} {i j : α} (hv : v i = v j) (k : α) :
v ((equiv.swap i j) k) = v k

A function is invariant to a swap if it is equal at both elements

theorem equiv.swap_apply_eq_iff {α : Sort u} [decidable_eq α] {x y z w : α} :
(equiv.swap x y) z = w z = (equiv.swap x y) w
theorem equiv.swap_apply_ne_self_iff {α : Sort u} [decidable_eq α] {a b x : α} :
(equiv.swap a b) x x a b (x = a x = b)
@[simp]
theorem equiv.perm.sum_congr_swap_refl {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (i j : α) :
@[simp]
theorem equiv.perm.sum_congr_refl_swap {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (i j : β) :
def equiv.set_value {α : Sort u} {β : Sort v} [decidable_eq α] (f : α β) (a : α) (b : β) :
α β

Augment an equivalence with a prescribed mapping f a = b

Equations
@[simp]
theorem equiv.set_value_eq {α : Sort u} {β : Sort v} [decidable_eq α] (f : α β) (a : α) (b : β) :
(f.set_value a b) a = b
def function.involutive.to_perm {α : Sort u} (f : α α) (h : function.involutive f) :

Convert an involutive function f to a permutation with to_fun = inv_fun = f.

Equations
@[simp]
theorem plift.eq_up_iff_down_eq {α : Sort u} {x : plift α} {y : α} :
x = {down := y} x.down = y
theorem function.injective.map_swap {α : Sort u_1} {β : Sort u_2} [decidable_eq α] [decidable_eq β] {f : α β} (hf : function.injective f) (x y z : α) :
f ((equiv.swap x y) z) = (equiv.swap (f x) (f y)) (f z)
@[simp]
theorem equiv.Pi_congr_left'_apply {α : Sort u} {β : Sort v} (P : α Sort w) (e : α β) (f : Π (a : α), P a) (x : β) :
(equiv.Pi_congr_left' P e) f x = f ((e.symm) x)
def equiv.Pi_congr_left' {α : Sort u} {β : Sort v} (P : α Sort w) (e : α β) :
(Π (a : α), P a) Π (b : β), P ((e.symm) b)

Transport dependent functions through an equivalence of the base space.

Equations
@[simp]
theorem equiv.Pi_congr_left'_symm_apply {α : Sort u} {β : Sort v} (P : α Sort w) (e : α β) (f : Π (b : β), P ((e.symm) b)) (x : α) :
((equiv.Pi_congr_left' P e).symm) f x = _.mpr (f (e x))
def equiv.Pi_congr_left {α : Sort u} {β : Sort v} (P : β Sort w) (e : α β) :
(Π (a : α), P (e a)) Π (b : β), P b

Transporting dependent functions through an equivalence of the base, expressed as a "simplification".

Equations
def equiv.Pi_congr {α : Sort u} {β : Sort v} {W : α Sort w} {Z : β Sort z} (h₁ : α β) (h₂ : Π (a : α), W a Z (h₁ a)) :
(Π (a : α), W a) Π (b : β), Z b

Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibers.

Equations
@[simp]
theorem equiv.coe_Pi_congr_symm {α : Sort u} {β : Sort v} {W : α Sort w} {Z : β Sort z} (h₁ : α β) (h₂ : Π (a : α), W a Z (h₁ a)) :
((h₁.Pi_congr h₂).symm) = λ (f : Π (b : β), Z b) (a : α), ((h₂ a).symm) (f (h₁ a))
theorem equiv.Pi_congr_symm_apply {α : Sort u} {β : Sort v} {W : α Sort w} {Z : β Sort z} (h₁ : α β) (h₂ : Π (a : α), W a Z (h₁ a)) (f : Π (b : β), Z b) :
((h₁.Pi_congr h₂).symm) f = λ (a : α), ((h₂ a).symm) (f (h₁ a))
@[simp]
theorem equiv.Pi_congr_apply_apply {α : Sort u} {β : Sort v} {W : α Sort w} {Z : β Sort z} (h₁ : α β) (h₂ : Π (a : α), W a Z (h₁ a)) (f : Π (a : α), W a) (a : α) :
(h₁.Pi_congr h₂) f (h₁ a) = (h₂ a) (f a)
def equiv.Pi_congr' {α : Sort u} {β : Sort v} {W : α Sort w} {Z : β Sort z} (h₁ : α β) (h₂ : Π (b : β), W ((h₁.symm) b) Z b) :
(Π (a : α), W a) Π (b : β), Z b

Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibres.

Equations
@[simp]
theorem equiv.coe_Pi_congr' {α : Sort u} {β : Sort v} {W : α Sort w} {Z : β Sort z} (h₁ : α β) (h₂ : Π (b : β), W ((h₁.symm) b) Z b) :
(h₁.Pi_congr' h₂) = λ (f : Π (a : α), W a) (b : β), (h₂ b) (f ((h₁.symm) b))
theorem equiv.Pi_congr'_apply {α : Sort u} {β : Sort v} {W : α Sort w} {Z : β Sort z} (h₁ : α β) (h₂ : Π (b : β), W ((h₁.symm) b) Z b) (f : Π (a : α), W a) :
(h₁.Pi_congr' h₂) f = λ (b : β), (h₂ b) (f ((h₁.symm) b))
@[simp]
theorem equiv.Pi_congr'_symm_apply_symm_apply {α : Sort u} {β : Sort v} {W : α Sort w} {Z : β Sort z} (h₁ : α β) (h₂ : Π (b : β), W ((h₁.symm) b) Z b) (f : Π (b : β), Z b) (b : β) :
((h₁.Pi_congr' h₂).symm) f ((h₁.symm) b) = ((h₂ b).symm) (f b)
theorem equiv.semiconj_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁) :
theorem equiv.semiconj₂_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁ α₁) :
@[protected, instance]
def equiv.arrow_congr.is_associative {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁ α₁) [is_associative α₁ f] :
@[protected, instance]
def equiv.arrow_congr.is_idempotent {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁ α₁) [is_idempotent α₁ f] :
@[protected, instance]
def equiv.arrow_congr.is_left_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁ α₁) [is_left_cancel α₁ f] :
@[protected, instance]
def equiv.arrow_congr.is_right_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁ α₁) [is_right_cancel α₁ f] :
theorem function.injective.swap_apply {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] {f : α β} (hf : function.injective f) (x y z : α) :
(equiv.swap (f x) (f y)) (f z) = f ((equiv.swap x y) z)
theorem function.injective.swap_comp {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] {f : α β} (hf : function.injective f) (x y : α) :
(equiv.swap (f x) (f y)) f = f (equiv.swap x y)
def subsingleton_prod_self_equiv {α : Type u_1} [subsingleton α] :
α × α α

If α is a subsingleton, then it is equivalent to α × α.

Equations
def equiv_of_subsingleton_of_subsingleton {α : Sort u} {β : Sort v} [subsingleton α] [subsingleton β] (f : α β) (g : β α) :
α β

To give an equivalence between two subsingleton types, it is sufficient to give any two functions between them.

Equations
noncomputable def equiv.punit_of_nonempty_of_subsingleton {α : Sort u_1} [h : nonempty α] [subsingleton α] :

A nonempty subsingleton type is (noncomputably) equivalent to punit.

Equations
def unique_unique_equiv {α : Sort u} :

unique (unique α) is equivalent to unique α.

Equations
theorem function.update_comp_equiv {α : Sort u_1} {β : Sort u_2} {α' : Sort u_3} [decidable_eq α'] [decidable_eq α] (f : α β) (g : α' α) (a : α) (v : β) :
theorem function.update_apply_equiv_apply {α : Sort u_1} {β : Sort u_2} {α' : Sort u_3} [decidable_eq α'] [decidable_eq α] (f : α β) (g : α' α) (a : α) (v : β) (a' : α') :
function.update f a v (g a') = function.update (f g) ((g.symm) a) v a'
theorem function.Pi_congr_left'_update {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] (P : α Sort u_1) (e : α β) (f : Π (a : α), P a) (b : β) (x : P ((e.symm) b)) :
theorem function.Pi_congr_left'_symm_update {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] (P : α Sort u_1) (e : α β) (f : Π (b : β), P ((e.symm) b)) (b : β) (x : P ((e.symm) b)) :