# mathlib3documentation

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

• canonical isomorphisms between various types: e.g.,

• `equiv.sum_equiv_sigma_bool` is the canonical equivalence between the sum of two types `α ⊕ β` and the sigma-type `Σ b : bool, cond b α β`;

• `equiv.prod_sum_distrib : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ)` shows that type product and type sum satisfy the distributive law up to a canonical equivalence;

• operations on equivalences: e.g.,

• `equiv.prod_congr ea eb : α₁ × β₁ ≃ α₂ × β₂`: combine two equivalences `ea : α₁ ≃ α₂` and `eb : β₁ ≃ β₂` using `prod.map`.

More definitions of this kind can be found in other files. E.g., `data/equiv/transfer_instance` does it for many algebraic type classes like `group`, `module`, etc.

## Tags #

equivalence, congruence, bijective map

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

`pprod α β` is equivalent to `α × β`

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

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 : γ) :
(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
@[simp]
theorem equiv.pprod_equiv_prod_plift_symm_apply {α : Sort u_1} {β : Sort u_2} (ᾰ : × ) :
= ᾰ.fst, ᾰ.snd
def equiv.pprod_equiv_prod_plift {α : Sort u_1} {β : Sort u_2} :
β ×

`pprod α β` is equivalent to `plift α × plift β`

Equations
@[simp]
theorem equiv.pprod_equiv_prod_plift_apply {α : Sort u_1} {β : Sort u_2} (ᾰ : β) :
= ({down := ᾰ.fst}, {down := ᾰ.snd})
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₂) = 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 : α × β) :
β) x = x.swap
@[simp]
theorem equiv.prod_comm_symm (α : Type u_1) (β : Type u_2) :
β).symm =
@[simp]
theorem equiv.prod_assoc_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ) :
β γ).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 : × β) × γ) :
β γ) 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 : × β) × γ × δ) :
δ) 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) :
δ).symm = δ
@[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` is a right identity for type product up to an equivalence.

Equations
@[simp]
theorem equiv.prod_punit_apply (α : Type u_1) (p : α × punit) :
p = p.fst
@[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` 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 × α) :
= ᾰ.snd
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 : α × β) :
β) x = x.fst
@[simp]
theorem equiv.prod_unique_symm_apply {α : Type u_1} {β : Type u_2} [unique β] (x : α) :
β).symm) 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 : β × α) :
β) x = x.snd
@[simp]
theorem equiv.unique_prod_symm_apply {α : Type u_1} {β : Type u_2} [unique β] (x : α) :
β).symm) 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 `equiv`s 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 `equiv`s 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} :
= equiv.refl β)

`bool` is equivalent the sum of two `punit`s.

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) :
β).symm =
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 : α) :
β γ) (sum.inl (sum.inl a)) =
@[simp]
theorem equiv.sum_assoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :
β γ) (sum.inl (sum.inr b)) = sum.inr (sum.inl b)
@[simp]
theorem equiv.sum_assoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :
β γ) (sum.inr c) = sum.inr (sum.inr c)
@[simp]
theorem equiv.sum_assoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) :
β γ).symm) (sum.inl a) = sum.inl (sum.inl a)
@[simp]
theorem equiv.sum_assoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :
β γ).symm) (sum.inr (sum.inl b)) = sum.inl (sum.inr b)
@[simp]
theorem equiv.sum_assoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :
β γ).symm) (sum.inr (sum.inr 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 : α) :
β).symm) val = sum.inl val
@[simp]
theorem equiv.sum_empty_apply_inl {α : Type u_1} {β : Type u_2} [is_empty β] (a : α) :
β) (sum.inl a) = 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 α] (ᾰ : β) :
β).symm) =
@[simp]
theorem equiv.empty_sum_apply_inr {α : Type u_1} {β : Type u_2} [is_empty α] (b : β) :
β) (sum.inr b) = b

`option α` is equivalent to `α ⊕ punit`

Equations
@[simp]
theorem equiv.option_equiv_sum_punit_none {α : Type u_1} :
= sum.inr punit.star
@[simp]
theorem equiv.option_equiv_sum_punit_some {α : Type u_1} (a : α) :
@[simp]
theorem equiv.option_equiv_sum_punit_coe {α : Type u_1} (a : α) :
@[simp]
theorem equiv.option_equiv_sum_punit_symm_inl {α : Type u_1} (a : α) :
(sum.inl a) = a
@[simp]
theorem equiv.option_equiv_sum_punit_symm_inr {α : Type u_1} (a : punit) :
@[simp]
theorem equiv.option_is_some_equiv_symm_apply_coe (α : Type u_1) (x : α) :
( x) =
@[simp]
theorem equiv.option_is_some_equiv_apply (α : Type u_1) (o : {x // (x.is_some)}) :
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} {β : Type u_2} (f : Π (a : option α), β a) :
= , λ (a : α), f (option.some a))
@[simp]
theorem equiv.pi_option_equiv_prod_symm_apply {α : Type u_1} {β : Type u_2} (x : × Π (a : α), β (option.some a)) (a : option α) :
= a.cases_on x.fst x.snd
def equiv.pi_option_equiv_prod {α : Type u_1} {β : Type u_2} :
(Π (a : option α), β a) × Π (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}) :
= (x.snd)
@[simp]
theorem equiv.sigma_fiber_equiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
((.symm) x).snd) = x
@[simp]
theorem equiv.sigma_fiber_equiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
(.symm) x).fst = 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)  :
{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) (x : {a // p a}) :
@[simp]
theorem equiv.sum_compl_apply_inr {α : Type u_1} (p : α Prop) (x : {a // ¬p a}) :
@[simp]
theorem equiv.sum_compl_apply_symm_of_pos {α : Type u_1} (p : α Prop) (a : α) (h : p a) :
@[simp]
theorem equiv.sum_compl_apply_symm_of_neg {α : Type u_1} (p : α Prop) (a : α) (h : ¬p a) :
def equiv.subtype_congr {α : Type u_1} {p q : α Prop} (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} (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} (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} (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} (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} (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} (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}  :
@[simp]
theorem equiv.perm.subtype_congr.symm {ε : Type u_1} {p : ε Prop} (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) :
@[simp]
theorem equiv.perm.subtype_congr.trans {ε : Type u_1} {p : ε Prop} (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) (x₀ : {a // p a} β) (x : {a // ¬p a} β) (a : α) :
( 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) (x₀ : {a // p a} β) (x : {x // x coe = x₀}) (a : {a // ¬p a}) :
x₀) x a = x a
def equiv.subtype_preimage {α : Sort u} {β : Sort v} (p : α Prop) (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) (x₀ : {a // p a} β) (x : {a // ¬p a} β) (a : α) (h : p a) :
( x₀).symm) x) a = x₀ a, h⟩
theorem equiv.subtype_preimage_symm_apply_coe_neg {α : Sort u} {β : Sort v} (p : α Prop) (x₀ : {a // p a} β) (x : {a // ¬p a} β) (a : α) (h : ¬p a) :
( 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 : α) :
f y x = 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 : α₁) :
(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 : β₁) :
(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 : α₁ β₁ β₂) :
α₁) = α₁).trans
@[simp]
theorem equiv.prod_congr_right_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) :
β₂) = β₁).trans
theorem equiv.sigma_congr_right_sigma_equiv_prod {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) :
β₂) = β₁).trans
theorem equiv.sigma_equiv_prod_sigma_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ β₁ β₂) :
β₁).symm.trans = β₂).symm
@[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}) (ᾰ : β) :
.symm) = ((.symm) (.symm) ᾰ)).snd)
@[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}) (ᾰ : α) :
= ((e (f ᾰ)) (.symm) ᾰ).snd)
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 : α) :
g a) = f 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 : β₁) :
(a, b) = (a, e 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 : β₁) :
(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 : (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 : α₁ × β₁) :
ab).fst = ab.fst
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 : α) :
( f).fst a = f (sum.inl a)
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_apply_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) (b : β) :
( f).snd b = f (sum.inr b)
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α γ) (g : β γ) (a : α) :
γ).symm) (f, g) (sum.inl a) = f a
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_symm_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α γ) (g : β γ) (b : β) :
γ).symm) (f, g) (sum.inr b) = 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 : γ) :
γ) (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 : γ) :
γ) (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 : α × γ) :
γ).symm) (sum.inl a) = (sum.inl a.fst, a.snd)
@[simp]
theorem equiv.sum_prod_distrib_symm_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β × γ) :
γ).symm) (sum.inr b) = (sum.inr b.fst, b.snd)
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 : β) :
γ) (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 : γ) :
γ) (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 : α × β) :
γ).symm) (sum.inl a) = (a.fst, sum.inl a.snd)
@[simp]
theorem equiv.prod_sum_distrib_symm_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α × γ) :
γ).symm) (sum.inr a) = (a.fst, sum.inr a.snd)
@[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) :
β).symm) = sum.elim (λ (_x : ι), sum.inl)) (λ (_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
@[simp]
theorem equiv.bool_prod_equiv_sum_symm_apply (α : Type u) (ᾰ : α α) :
=
def equiv.bool_prod_equiv_sum (α : Type u) :
α α

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

Equations
@[simp]
theorem equiv.bool_prod_equiv_sum_apply (α : Type u) (p : bool × α) :
def equiv.bool_arrow_equiv_prod (α : Type u) :
(bool α) α × α

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

Equations
@[simp]
theorem equiv.bool_arrow_equiv_prod_apply (α : Type u) (f : bool α) :
= (f bool.tt, f bool.ff)
@[simp]
theorem equiv.bool_arrow_equiv_prod_symm_apply (α : Type u) (p : α × α) (b : bool) :
p b = cond b p.fst p.snd

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

Equations

`ℕ ⊕ punit` is equivalent to `ℕ`.

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)) := _) :
h = equiv.refl {a // p 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}) :
( b) = 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}) :
a) = 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 : Prop) :
{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 : Prop) (a : {a // (h : p a), q a, h⟩}) :
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_exists_apply_coe {α : Sort u} (p : α Prop) (q : Prop) (a : subtype q) :
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]
theorem equiv.subtype_subtype_equiv_subtype_inter_symm_apply_coe_coe {α : Sort u} (p q : α Prop) (ᾰ : {x // p x q x}) :
ᾰ) =
@[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}

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 : α) :
x = x, _⟩
@[simp]
theorem equiv.subtype_univ_equiv_apply {α : Type u} {p : α Prop} (h : (x : α), p x) (x : subtype p) :
= x
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})

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 : Type v) (h : 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)  :
(Π (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) (f : (Π (i : {x // p x}), β i) × Π (i : {x // ¬p x}), β i) (x : α) :
.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) (f : Π (i : α), β i) :
= (λ (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 : α) :
β).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) :
β) 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 : α) :
β).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) :
β) 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) :
= λ (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}) :
= g x
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) :
= λ (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) :
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) :
y) x = 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) :
y) x' = f x', h⟩
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) (ᾰ : α) :
hf) = f ᾰ
theorem equiv.of_bijective_apply_symm_apply {α : Sort u} {β : Sort v} (f : α β) (hf : function.bijective f) (x : β) :
f ( hf).symm) x) = x
@[simp]
theorem equiv.of_bijective_symm_apply_apply {α : Sort u} {β : Sort v} (f : α β) (hf : function.bijective f) (x : α) :
hf).symm) (f x) = x
@[protected, instance]
Equations
def equiv.perm.extend_domain {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' Prop} (f : α' ) :

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} (f : α' ) (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} (f : α' ) {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} (f : α' ) {b : β'} (h : ¬p b) :
@[simp]
theorem equiv.perm.extend_domain_refl {α' : Type u_1} {β' : Type u_2} {p : β' Prop} (f : α' ) :
@[simp]
theorem equiv.perm.extend_domain_symm {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' Prop} (f : α' ) :
theorem equiv.perm.extend_domain_trans {α' : Type u_1} {β' : Type u_2} {p : β' Prop} (f : α' ) (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₁), 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₁), y x y) (x : α) (hx : p₂ x) :
h) x, hx⟩ = 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₁), 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 : α) :
r = r
theorem equiv.swap_core_swap_core {α : Sort u} [decidable_eq α] (r a b : α) :
b r) = r
theorem equiv.swap_core_comm {α : Sort u} [decidable_eq α] (r a b : α) :
r = r
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 : α) :
a =
theorem equiv.swap_comm {α : Sort u} [decidable_eq α] (a b : α) :
b = a
theorem equiv.swap_apply_def {α : Sort u} [decidable_eq α] (a b x : α) :
b) x = ite (x = a) b (ite (x = b) a x)
@[simp]
theorem equiv.swap_apply_left {α : Sort u} [decidable_eq α] (a b : α) :
b) a = b
@[simp]
theorem equiv.swap_apply_right {α : Sort u} [decidable_eq α] (a b : α) :
b) b = a
theorem equiv.swap_apply_of_ne_of_ne {α : Sort u} [decidable_eq α] {a b x : α} :
x a x b b) x = x
@[simp]
theorem equiv.swap_swap {α : Sort u} [decidable_eq α] (a b : α) :
equiv.trans b) 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 : α} :
y = x = y
theorem equiv.swap_comp_apply {α : Sort u} [decidable_eq α] {a b x : α} (π : equiv.perm α) :
b)) x = ite (π x = a) b (ite (π x = b) a (π x))
theorem equiv.swap_eq_update {α : Sort u} [decidable_eq α] (i j : α) :
j) = i j
theorem equiv.comp_swap_eq_update {α : Sort u} {β : Sort v} [decidable_eq α] (i j : α) (f : α β) :
f j) = function.update 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 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 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 : α) :
j) ( 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 ( 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 : α} :
y) z = w z = y) w
theorem equiv.swap_apply_ne_self_iff {α : Sort u} [decidable_eq α] {a b x : α} :
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 : β) :
j) = (sum.inr 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 function.involutive.coe_to_perm {α : Sort u} {f : α α} (h : function.involutive f) :
@[simp]
theorem function.involutive.to_perm_symm {α : Sort u} {f : α α} (h : function.involutive f) :
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 ( 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 : β) :
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 : α) :
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 : α₁ α₁) :
((e.conj) f)
theorem equiv.semiconj₂_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁ α₁) :
((e.arrow_congr e.conj) f)
@[protected, instance]
def equiv.arrow_congr.is_associative {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁ α₁) [ f] :
@[protected, instance]
def equiv.arrow_congr.is_idempotent {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁ α₁) [ f] :
@[protected, instance]
def equiv.arrow_congr.is_left_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁ α₁) [ f] :
@[protected, instance]
def equiv.arrow_congr.is_right_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ α₁ α₁) [ 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 ( 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 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 : β) :
v g = function.update (f g) ((g.symm) 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' : α') :
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)) :
e) ((e.symm) b) x) = function.update ( e) f) b x
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)) :
e).symm) b x) = function.update ( e).symm) f) ((e.symm) b) x