Equivalence between types

In this file we continue the work on equivalences begun in Logic/Equiv/Defs.lean, defining

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

  • Equiv.sumEquivSigmaBool is the canonical equivalence between the sum of two types α ⊕ β⊕ β and the sigma-type Σ b : Bool, cond b α β;

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

• operations on equivalences: e.g.,

  • Equiv.prodCongr 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/TransferInstance.lean does it for many algebraic type classes like Group, Module, etc.

Tags

equivalence, congruence, bijective map

ink

@[simp]

theorem Equiv.pprodEquivProd_apply {α : Type u_1} {β : Type u_2} (x : PProd α β) : ↑Equiv.pprodEquivProd x = (x.fst, x.snd)

ink

@[simp]

theorem Equiv.pprodEquivProd_symm_apply {α : Type u_1} {β : Type u_2} (x : α × β) : ↑(Equiv.symm Equiv.pprodEquivProd) x = { fst := x.fst, snd := x.snd }

ink

def Equiv.pprodEquivProd {α : Type u_1} {β : Type u_2} : PProd α β ≃ α × β

PProd α β is equivalent to α × β× β

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.pprodCongr_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α ≃ β) (e₂ : γ ≃ δ) (x : PProd α γ) : ↑(Equiv.pprodCongr e₁ e₂) x = { fst := ↑e₁ x.fst, snd := ↑e₂ x.snd }

ink

def Equiv.pprodCongr {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α ≃ β) (e₂ : γ ≃ δ) : PProd α γ ≃ PProd β δ

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.pprodProd_apply {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : ∀ (a : PProd α₁ β₁), ↑(Equiv.pprodProd ea eb) a = (↑ea a.fst, ↑eb a.snd)

ink

@[simp]

theorem Equiv.pprodProd_symm_apply {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : ∀ (a : α₂ × β₂), ↑(Equiv.symm (Equiv.pprodProd ea eb)) a = ↑(Equiv.symm (Equiv.pprodCongr ea eb)) { fst := a.fst, snd := a.snd }

ink

def Equiv.pprodProd {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : PProd α₁ β₁ ≃ α₂ × β₂

Combine two equivalences using PProd in the domain and Prod in the codomain.

Equations

• Equiv.pprodProd ea eb = Equiv.trans (Equiv.pprodCongr ea eb) Equiv.pprodEquivProd

ink

@[simp]

theorem Equiv.prodPProd_symm_apply {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : ∀ (a : PProd α₂ β₂), ↑(Equiv.symm (Equiv.prodPProd ea eb)) a = (↑(Equiv.symm ea) a.fst, ↑(Equiv.symm eb) a.snd)

ink

@[simp]

theorem Equiv.prodPProd_apply {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : ∀ (a : α₁ × β₁), ↑(Equiv.prodPProd ea eb) a = ↑(Equiv.symm (Equiv.pprodCongr (Equiv.symm ea) (Equiv.symm eb))) { fst := a.fst, snd := a.snd }

ink

def Equiv.prodPProd {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ × β₁ ≃ PProd α₂ β₂

Combine two equivalences using PProd in the codomain and Prod in the domain.

Equations

• Equiv.prodPProd ea eb = Equiv.symm (Equiv.pprodProd (Equiv.symm ea) (Equiv.symm eb))

ink

@[simp]

theorem Equiv.pprodEquivProdPLift_apply {α : Sort u_1} {β : Sort u_2} : ∀ (a : PProd α β), ↑Equiv.pprodEquivProdPLift a = (↑(Equiv.symm Equiv.plift) a.fst, ↑(Equiv.symm Equiv.plift) a.snd)

ink

@[simp]

theorem Equiv.pprodEquivProdPLift_symm_apply {α : Sort u_1} {β : Sort u_2} : ∀ (a : PLift α × PLift β), ↑(Equiv.symm Equiv.pprodEquivProdPLift) a = ↑(Equiv.symm (Equiv.pprodCongr (Equiv.symm Equiv.plift) (Equiv.symm Equiv.plift))) { fst := a.fst, snd := a.snd }

ink

def Equiv.pprodEquivProdPLift {α : Sort u_1} {β : Sort u_2} : PProd α β ≃ PLift α × PLift β

PProd α β is equivalent to PLift α × PLift β× PLift β

Equations

• Equiv.pprodEquivProdPLift = Equiv.pprodProd (Equiv.symm Equiv.plift) (Equiv.symm Equiv.plift)

ink

@[simp]

theorem Equiv.prodCongr_apply {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : ↑(Equiv.prodCongr e₁ e₂) = Prod.map ↑e₁ ↑e₂

ink

def Equiv.prodCongr {α₁ : 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

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.prodCongr_symm {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : Equiv.symm (Equiv.prodCongr e₁ e₂) = Equiv.prodCongr (Equiv.symm e₁) (Equiv.symm e₂)

ink

def Equiv.prodComm (α : Type u_1) (β : Type u_2) : α × β ≃ β × α

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

Equations

• Equiv.prodComm α β = { toFun := Prod.swap, invFun := Prod.swap, left_inv := (_ : ∀ (x : α × β), Prod.swap (Prod.swap x) = x), right_inv := (_ : ∀ (x : β × α), Prod.swap (Prod.swap x) = x) }

ink

@[simp]

theorem Equiv.coe_prodComm (α : Type u_1) (β : Type u_2) : ↑(Equiv.prodComm α β) = Prod.swap

ink

@[simp]

theorem Equiv.prodComm_apply {α : Type u_1} {β : Type u_2} (x : α × β) : ↑(Equiv.prodComm α β) x = Prod.swap x

ink

@[simp]

theorem Equiv.prodComm_symm (α : Type u_1) (β : Type u_2) : Equiv.symm (Equiv.prodComm α β) = Equiv.prodComm β α

ink

@[simp]

theorem Equiv.prodAssoc_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ) : ↑(Equiv.symm (Equiv.prodAssoc α β γ)) p = ((p.fst, p.snd.fst), p.snd.snd)

ink

@[simp]

theorem Equiv.prodAssoc_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : (α × β) × γ) : ↑(Equiv.prodAssoc α β γ) p = (p.fst.fst, p.fst.snd, p.snd)

ink

def Equiv.prodAssoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) : (α × β) × γ ≃ α × β × γ

Type product is associative up to an equivalence.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.curry_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) : ↑(Equiv.curry α β γ) = Function.curry

ink

@[simp]

theorem Equiv.curry_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) : ↑(Equiv.symm (Equiv.curry α β γ)) = Function.uncurry

ink

def Equiv.curry (α : Type u_1) (β : Type u_2) (γ : Type u_3) : (α × β → γ) ≃ (α → β → γ)

γ-valued functions on α × β× β are equivalent to functions α → β → γ→ β → γ→ γ.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.prodPUnit_apply (α : Type u_1) (p : α × PUnit) : ↑(Equiv.prodPUnit α) p = p.fst

ink

@[simp]

theorem Equiv.prodPUnit_symm_apply (α : Type u_1) (a : α) : ↑(Equiv.symm (Equiv.prodPUnit α)) a = (a, PUnit.unit)

ink

def Equiv.prodPUnit (α : Type u_1) : α × PUnit ≃ α

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.punitProd_apply (α : Type u_1) : ∀ (a : PUnit × α), ↑(Equiv.punitProd α) a = a.snd

ink

@[simp]

theorem Equiv.punitProd_symm_apply (α : Type u_1) : ∀ (a : α), ↑(Equiv.symm (Equiv.punitProd α)) a = (PUnit.unit, a)

ink

def Equiv.punitProd (α : Type u_1) : PUnit × α ≃ α

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

Equations

• Equiv.punitProd α = Trans.trans (Equiv.prodComm PUnit α) (Equiv.prodPUnit α)

ink

def Equiv.prodUnique (α : Type u_1) (β : Type u_2) [inst : Unique β] : α × β ≃ α

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

Equations

• Equiv.prodUnique α β = Equiv.trans (Equiv.prodCongr (Equiv.refl α) (Equiv.equivPUnit β)) (Equiv.prodPUnit α)

ink

@[simp]

theorem Equiv.coe_prodUnique {β : Type u_1} {α : Type u_2} [inst : Unique β] : ↑(Equiv.prodUnique α β) = Prod.fst

ink

theorem Equiv.prodUnique_apply {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : α × β) : ↑(Equiv.prodUnique α β) x = x.fst

ink

@[simp]

theorem Equiv.prodUnique_symm_apply {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : α) : ↑(Equiv.symm (Equiv.prodUnique α β)) x = (x, default)

ink

def Equiv.uniqueProd (α : Type u_1) (β : Type u_2) [inst : Unique β] : β × α ≃ α

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

Equations

• Equiv.uniqueProd α β = Equiv.trans (Equiv.prodCongr (Equiv.equivPUnit β) (Equiv.refl α)) (Equiv.punitProd α)

ink

@[simp]

theorem Equiv.coe_uniqueProd {β : Type u_1} {α : Type u_2} [inst : Unique β] : ↑(Equiv.uniqueProd α β) = Prod.snd

ink

theorem Equiv.uniqueProd_apply {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : β × α) : ↑(Equiv.uniqueProd α β) x = x.snd

ink

@[simp]

theorem Equiv.uniqueProd_symm_apply {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : α) : ↑(Equiv.symm (Equiv.uniqueProd α β)) x = (default, x)

ink

def Equiv.prodEmpty (α : Type u_1) : α × Empty ≃ Empty

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

Equations

• Equiv.prodEmpty α = Equiv.equivEmpty (α × Empty)

ink

def Equiv.emptyProd (α : Type u_1) : Empty × α ≃ Empty

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

Equations

• Equiv.emptyProd α = Equiv.equivEmpty (Empty × α)

ink

def Equiv.prodPEmpty (α : Type u_1) : α × PEmpty ≃ PEmpty

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

Equations

• Equiv.prodPEmpty α = Equiv.equivPEmpty (α × PEmpty)

ink

def Equiv.pemptyProd (α : Type u_1) : PEmpty × α ≃ PEmpty

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

Equations

• Equiv.pemptyProd α = Equiv.equivPEmpty (PEmpty × α)

ink

def Equiv.psumEquivSum (α : Type u_1) (β : Type u_2) : α ⊕' β ≃ α ⊕ β

PSum is equivalent to Sum.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.sumCongr_apply {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : ∀ (a : α₁ ⊕ β₁), ↑(Equiv.sumCongr ea eb) a = Sum.map (↑ea) (↑eb) a

ink

def Equiv.sumCongr {α₁ : 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

• One or more equations did not get rendered due to their size.

ink

def Equiv.psumCongr {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α ≃ β) (e₂ : γ ≃ δ) : α ⊕' γ ≃ β ⊕' δ

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.psumSum {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕' β₁ ≃ α₂ ⊕ β₂

Combine two Equivs using PSum in the domain and Sum in the codomain.

Equations

• Equiv.psumSum ea eb = Equiv.trans (Equiv.psumCongr ea eb) (Equiv.psumEquivSum α₂ β₂)

ink

def Equiv.sumPSum {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕ β₁ ≃ α₂ ⊕' β₂

Combine two Equivs using Sum in the domain and PSum in the codomain.

Equations

• Equiv.sumPSum ea eb = Equiv.symm (Equiv.psumSum (Equiv.symm ea) (Equiv.symm eb))

ink

@[simp]

theorem Equiv.sumCongr_trans {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} (e : α₁ ≃ β₁) (f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂) : Equiv.trans (Equiv.sumCongr e f) (Equiv.sumCongr g h) = Equiv.sumCongr (Equiv.trans e g) (Equiv.trans f h)

ink

@[simp]

theorem Equiv.sumCongr_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α ≃ β) (f : γ ≃ δ) : Equiv.symm (Equiv.sumCongr e f) = Equiv.sumCongr (Equiv.symm e) (Equiv.symm f)

ink

@[simp]

theorem Equiv.sumCongr_refl {α : Type u_1} {β : Type u_2} : Equiv.sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)

ink

def Equiv.Perm.sumCongr {α : 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

• Equiv.Perm.sumCongr ea eb = Equiv.sumCongr ea eb

ink

@[simp]

theorem Equiv.Perm.sumCongr_apply {α : Type u_1} {β : Type u_2} (ea : Equiv.Perm α) (eb : Equiv.Perm β) (x : α ⊕ β) : ↑(Equiv.Perm.sumCongr ea eb) x = Sum.map (↑ea) (↑eb) x

ink

theorem Equiv.Perm.sumCongr_trans {α : Type u_1} {β : Type u_2} (e : Equiv.Perm α) (f : Equiv.Perm β) (g : Equiv.Perm α) (h : Equiv.Perm β) : Equiv.trans (Equiv.Perm.sumCongr e f) (Equiv.Perm.sumCongr g h) = Equiv.Perm.sumCongr (Equiv.trans e g) (Equiv.trans f h)

ink

theorem Equiv.Perm.sumCongr_symm {α : Type u_1} {β : Type u_2} (e : Equiv.Perm α) (f : Equiv.Perm β) : Equiv.symm (Equiv.Perm.sumCongr e f) = Equiv.Perm.sumCongr (Equiv.symm e) (Equiv.symm f)

ink

theorem Equiv.Perm.sumCongr_refl {α : Type u_1} {β : Type u_2} : Equiv.Perm.sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)

ink

def Equiv.boolEquivPUnitSumPUnit : Bool ≃ PUnit ⊕ PUnit

Bool is equivalent the sum of two PUnits.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.sumComm_apply (α : Type u_1) (β : Type u_2) : ↑(Equiv.sumComm α β) = Sum.swap

ink

def Equiv.sumComm (α : Type u_1) (β : Type u_2) : α ⊕ β ≃ β ⊕ α

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

Equations

• Equiv.sumComm α β = { toFun := Sum.swap, invFun := Sum.swap, left_inv := (_ : ∀ (x : α ⊕ β), Sum.swap (Sum.swap x) = x), right_inv := (_ : ∀ (x : β ⊕ α), Sum.swap (Sum.swap x) = x) }

ink

@[simp]

theorem Equiv.sumComm_symm (α : Type u_1) (β : Type u_2) : Equiv.symm (Equiv.sumComm α β) = Equiv.sumComm β α

ink

def Equiv.sumAssoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ

Sum of types is associative up to an equivalence.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.sumAssoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) : ↑(Equiv.sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a

ink

@[simp]

theorem Equiv.sumAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) : ↑(Equiv.sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)

ink

@[simp]

theorem Equiv.sumAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) : ↑(Equiv.sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)

ink

@[simp]

theorem Equiv.sumAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) : ↑(Equiv.symm (Equiv.sumAssoc α β γ)) (Sum.inl a) = Sum.inl (Sum.inl a)

ink

@[simp]

theorem Equiv.sumAssoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) : ↑(Equiv.symm (Equiv.sumAssoc α β γ)) (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)

ink

@[simp]

theorem Equiv.sumAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) : ↑(Equiv.symm (Equiv.sumAssoc α β γ)) (Sum.inr (Sum.inr c)) = Sum.inr c

ink

@[simp]

theorem Equiv.sumEmpty_symm_apply (α : Type u_1) (β : Type u_2) [inst : IsEmpty β] (val : α) : ↑(Equiv.symm (Equiv.sumEmpty α β)) val = Sum.inl val

ink

def Equiv.sumEmpty (α : Type u_1) (β : Type u_2) [inst : IsEmpty β] : α ⊕ β ≃ α

Sum with IsEmpty is equivalent to the original type.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.sumEmpty_apply_inl {β : Type u_1} {α : Type u_2} [inst : IsEmpty β] (a : α) : ↑(Equiv.sumEmpty α β) (Sum.inl a) = a

ink

@[simp]

theorem Equiv.emptySum_symm_apply (α : Type u_1) (β : Type u_2) [inst : IsEmpty α] : ∀ (a : β), ↑(Equiv.symm (Equiv.emptySum α β)) a = Sum.inr a

ink

def Equiv.emptySum (α : Type u_1) (β : Type u_2) [inst : IsEmpty α] : α ⊕ β ≃ β

The sum of IsEmpty with any type is equivalent to that type.

Equations

• Equiv.emptySum α β = Equiv.trans (Equiv.sumComm α β) (Equiv.sumEmpty β α)

ink

@[simp]

theorem Equiv.emptySum_apply_inr {α : Type u_1} {β : Type u_2} [inst : IsEmpty α] (b : β) : ↑(Equiv.emptySum α β) (Sum.inr b) = b

ink

def Equiv.optionEquivSumPUnit (α : Type u_1) : Option α ≃ α ⊕ PUnit

Option α is equivalent to α ⊕ punit⊕ punit

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.optionEquivSumPUnit_none {α : Type u_1} : ↑(Equiv.optionEquivSumPUnit α) none = Sum.inr PUnit.unit

ink

@[simp]

theorem Equiv.optionEquivSumPUnit_some {α : Type u_1} (a : α) : ↑(Equiv.optionEquivSumPUnit α) (some a) = Sum.inl a

ink

@[simp]

theorem Equiv.optionEquivSumPUnit_coe {α : Type u_1} (a : α) : ↑(Equiv.optionEquivSumPUnit α) (some a) = Sum.inl a

ink

@[simp]

theorem Equiv.optionEquivSumPUnit_symm_inl {α : Type u_1} (a : α) : ↑(Equiv.symm (Equiv.optionEquivSumPUnit α)) (Sum.inl a) = some a

ink

@[simp]

theorem Equiv.optionEquivSumPUnit_symm_inr {α : Type u_1} (a : PUnit) : ↑(Equiv.symm (Equiv.optionEquivSumPUnit α)) (Sum.inr a) = none

ink

@[simp]

theorem Equiv.optionIsSomeEquiv_apply (α : Type u_1) (o : { x // Option.isSome x = true }) : ↑(Equiv.optionIsSomeEquiv α) o = Option.get ↑o (_ : Option.isSome ↑o = true)

ink

@[simp]

theorem Equiv.optionIsSomeEquiv_symm_apply_coe (α : Type u_1) (x : α) : ↑(↑(Equiv.symm (Equiv.optionIsSomeEquiv α)) x) = some x

ink

def Equiv.optionIsSomeEquiv (α : Type u_1) : { x // Option.isSome x = true } ≃ α

The set of x : Option α such that isSome x is equivalent to α.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.piOptionEquivProd_apply {α : Type u_1} {β : Option α → Type u_2} (f : (a : Option α) → β a) : ↑Equiv.piOptionEquivProd f = (f none, fun a => f (some a))

ink

@[simp]

theorem Equiv.piOptionEquivProd_symm_apply {α : Type u_1} {β : Option α → Type u_2} (x : β none × ((a : α) → β (some a))) (a : Option α) : ↑(Equiv.symm Equiv.piOptionEquivProd) x a = Option.casesOn a x.fst x.snd

ink

def Equiv.piOptionEquivProd {α : Type u_1} {β : Option α → Type u_2} : ((a : Option α) → β a) ≃ β none × ((a : α) → β (some a))

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.sumEquivSigmaBool (α : Type u) (β : Type u) : α ⊕ β ≃ (b : Bool) × bif b then α else β

α ⊕ β⊕ β 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

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.sigmaFiberEquiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : (↑(Equiv.symm (Equiv.sigmaFiberEquiv f)) x).fst = f x

ink

@[simp]

theorem Equiv.sigmaFiberEquiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : ↑(↑(Equiv.symm (Equiv.sigmaFiberEquiv f)) x).snd = x

ink

@[simp]

theorem Equiv.sigmaFiberEquiv_apply {α : Type u_1} {β : Type u_2} (f : α → β) (x : (y : β) × { x // f x = y }) : ↑(Equiv.sigmaFiberEquiv f) x = ↑x.snd

ink

def Equiv.sigmaFiberEquiv {α : Type u_1} {β : Type u_2} (f : α → β) : (y : β) × { x // f x = y } ≃ α

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.sumCompl {α : Type u_1} (p : α → Prop) [inst : DecidablePred 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}¬ p a} is naturally equivalent to α.

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.sumCompl_apply_inl {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (x : { a // p a }) : ↑(Equiv.sumCompl p) (Sum.inl x) = ↑x

ink

@[simp]

theorem Equiv.sumCompl_apply_inr {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (x : { a // ¬p a }) : ↑(Equiv.sumCompl p) (Sum.inr x) = ↑x

ink

@[simp]

theorem Equiv.sumCompl_apply_symm_of_pos {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (a : α) (h : p a) : ↑(Equiv.symm (Equiv.sumCompl p)) a = Sum.inl { val := a, property := h }

ink

@[simp]

theorem Equiv.sumCompl_apply_symm_of_neg {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (a : α) (h : ¬p a) : ↑(Equiv.symm (Equiv.sumCompl p)) a = Sum.inr { val := a, property := h }

ink

def Equiv.subtypeCongr {α : Type u_1} {p : α → Prop} {q : α → Prop} [inst : DecidablePred p] [inst : DecidablePred q] (e : { x // p x } ≃ { x // q x }) (f : { x // ¬p x } ≃ { x // ¬q x }) : Equiv.Perm α

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

Equations

• Equiv.subtypeCongr e f = Equiv.trans (Equiv.symm (Equiv.sumCompl p)) (Equiv.trans (Equiv.sumCongr e f) (Equiv.sumCompl q))

ink

def Equiv.Perm.subtypeCongr {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }) : Equiv.Perm ε

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

Equations

• Equiv.Perm.subtypeCongr ep en = ↑(Equiv.permCongr (Equiv.sumCompl p)) (Equiv.Perm.sumCongr ep en)

ink

theorem Equiv.Perm.subtypeCongr.apply {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }) (a : ε) : ↑(Equiv.Perm.subtypeCongr ep en) a = if h : p a then ↑(↑ep { val := a, property := h }) else ↑(↑en { val := a, property := h })

ink

@[simp]

theorem Equiv.Perm.subtypeCongr.left_apply {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }) {a : ε} (h : p a) : ↑(Equiv.Perm.subtypeCongr ep en) a = ↑(↑ep { val := a, property := h })

ink

@[simp]

theorem Equiv.Perm.subtypeCongr.left_apply_subtype {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }) (a : { a // p a }) : ↑(Equiv.Perm.subtypeCongr ep en) ↑a = ↑(↑ep a)

ink

@[simp]

theorem Equiv.Perm.subtypeCongr.right_apply {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }) {a : ε} (h : ¬p a) : ↑(Equiv.Perm.subtypeCongr ep en) a = ↑(↑en { val := a, property := h })

ink

@[simp]

theorem Equiv.Perm.subtypeCongr.right_apply_subtype {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }) (a : { a // ¬p a }) : ↑(Equiv.Perm.subtypeCongr ep en) ↑a = ↑(↑en a)

ink

@[simp]

theorem Equiv.Perm.subtypeCongr.refl {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] : Equiv.Perm.subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε

ink

@[simp]

theorem Equiv.Perm.subtypeCongr.symm {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }) : Equiv.symm (Equiv.Perm.subtypeCongr ep en) = Equiv.Perm.subtypeCongr (Equiv.symm ep) (Equiv.symm en)

ink

@[simp]

theorem Equiv.Perm.subtypeCongr.trans {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (ep' : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }) (en' : Equiv.Perm { a // ¬p a }) : Equiv.trans (Equiv.Perm.subtypeCongr ep en) (Equiv.Perm.subtypeCongr ep' en') = Equiv.Perm.subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')

ink

@[simp]

theorem Equiv.subtypePreimage_apply {α : Sort u_1} {β : Sort u_2} (p : α → Prop) [inst : DecidablePred p] (x₀ : { a // p a } → β) (x : { x // x ∘ Subtype.val = x₀ }) (a : { a // ¬p a }) : ↑(Equiv.subtypePreimage p x₀) x a = ↑x ↑a

ink

@[simp]

theorem Equiv.subtypePreimage_symm_apply_coe {α : Sort u_1} {β : Sort u_2} (p : α → Prop) [inst : DecidablePred p] (x₀ : { a // p a } → β) (x : { a // ¬p a } → β) (a : α) : ↑(↑(Equiv.symm (Equiv.subtypePreimage p x₀)) x) a = if h : p a then x₀ { val := a, property := h } else x { val := a, property := h }

ink

def Equiv.subtypePreimage {α : Sort u_1} {β : Sort u_2} (p : α → Prop) [inst : DecidablePred p] (x₀ : { a // p a } → β) : { x // x ∘ Subtype.val = 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} → β¬ p a} → β→ β.

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Equiv.subtypePreimage_symm_apply_coe_pos {α : Sort u_1} {β : Sort u_2} (p : α → Prop) [inst : DecidablePred p] (x₀ : { a // p a } → β) (x : { a // ¬p a } → β) (a : α) (h : p a) : ↑(↑(Equiv.symm (Equiv.subtypePreimage p x₀)) x) a = x₀ { val := a, property := h }

ink

theorem Equiv.subtypePreimage_symm_apply_coe_neg {α : Sort u_1} {β : Sort u_2} (p : α → Prop) [inst : DecidablePred p] (x₀ : { a // p a } → β) (x : { a // ¬p a } → β) (a : α) (h : ¬p a) : ↑(↑(Equiv.symm (Equiv.subtypePreimage p x₀)) x) a = x { val := a, property := h }

ink

def Equiv.piCongrRight {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} (F : (a : α) → β₁ a ≃ β₂ a) : ((a : α) → β₁ a) ≃ ((a : α) → β₂ a)

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.piComm_apply {α : Sort u_1} {β : Sort u_2} (φ : α → β → Sort u_3) (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) : ↑(Equiv.piComm φ) f y x = Function.swap f y x

ink

def Equiv.piComm {α : Sort u_1} {β : Sort u_2} (φ : α → β → Sort u_3) : ((a : α) → (b : β) → φ a b) ≃ ((b : β) → (a : α) → φ a b)

Given φ : α → β → Sort*→ β → Sort*→ Sort*, we have an equivalence between ∀ a b, φ a b∀ a b, φ a b and ∀ b a, φ a b∀ b a, φ a b. This is Function.swap as an Equiv.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.piComm_symm {α : Sort u_1} {β : Sort u_2} {φ : α → β → Sort u_3} : Equiv.symm (Equiv.piComm φ) = Equiv.piComm (Function.swap φ)

ink

def Equiv.piCurry {α : 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

• One or more equations did not get rendered due to their size.

ink

def Equiv.prodCongrLeft {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) : β₁ × α₁ ≃ β₂ × α₁

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.prodCongrLeft_apply {α₁ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_1} (e : α₁ → β₁ ≃ β₂) (b : β₁) (a : α₁) : ↑(Equiv.prodCongrLeft e) (b, a) = (↑(e a) b, a)

ink

theorem Equiv.prodCongr_refl_right {α₁ : Type u_3} {β₁ : Type u_1} {β₂ : Type u_2} (e : β₁ ≃ β₂) : Equiv.prodCongr e (Equiv.refl α₁) = Equiv.prodCongrLeft fun x => e

ink

def Equiv.prodCongrRight {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) : α₁ × β₁ ≃ α₁ × β₂

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.prodCongrRight_apply {α₁ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_1} (e : α₁ → β₁ ≃ β₂) (a : α₁) (b : β₁) : ↑(Equiv.prodCongrRight e) (a, b) = (a, ↑(e a) b)

ink

theorem Equiv.prodCongr_refl_left {α₁ : Type u_3} {β₁ : Type u_1} {β₂ : Type u_2} (e : β₁ ≃ β₂) : Equiv.prodCongr (Equiv.refl α₁) e = Equiv.prodCongrRight fun x => e

ink

@[simp]

theorem Equiv.prodCongrLeft_trans_prodComm {α₁ : Type u_3} {β₁ : Type u_2} {β₂ : Type u_1} (e : α₁ → β₁ ≃ β₂) : Equiv.trans (Equiv.prodCongrLeft e) (Equiv.prodComm β₂ α₁) = Equiv.trans (Equiv.prodComm β₁ α₁) (Equiv.prodCongrRight e)

ink

@[simp]

theorem Equiv.prodCongrRight_trans_prodComm {α₁ : Type u_3} {β₁ : Type u_2} {β₂ : Type u_1} (e : α₁ → β₁ ≃ β₂) : Equiv.trans (Equiv.prodCongrRight e) (Equiv.prodComm α₁ β₂) = Equiv.trans (Equiv.prodComm α₁ β₁) (Equiv.prodCongrLeft e)

ink

theorem Equiv.sigmaCongrRight_sigmaEquivProd {α₁ : Type u_3} {β₁ : Type u_2} {β₂ : Type u_1} (e : α₁ → β₁ ≃ β₂) : Equiv.trans (Equiv.sigmaCongrRight e) (Equiv.sigmaEquivProd α₁ β₂) = Equiv.trans (Equiv.sigmaEquivProd α₁ β₁) (Equiv.prodCongrRight e)

ink

theorem Equiv.sigmaEquivProd_sigmaCongrRight {α₁ : Type u_2} {β₁ : Type u_1} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) : Equiv.trans (Equiv.symm (Equiv.sigmaEquivProd α₁ β₁)) (Equiv.sigmaCongrRight e) = Equiv.trans (Equiv.prodCongrRight e) (Equiv.symm (Equiv.sigmaEquivProd α₁ β₂))

ink

@[simp]

theorem Equiv.ofFiberEquiv_apply {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : α → γ} {g : β → γ} (e : (c : γ) → { a // f a = c } ≃ { b // g b = c }) : ∀ (a : α), ↑(Equiv.ofFiberEquiv e) a = ↑(↑(e (f a)) (↑(Equiv.symm (Equiv.sigmaFiberEquiv f)) a).snd)

ink

@[simp]

theorem Equiv.ofFiberEquiv_symm_apply {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : α → γ} {g : β → γ} (e : (c : γ) → { a // f a = c } ≃ { b // g b = c }) : ∀ (a : β), ↑(Equiv.symm (Equiv.ofFiberEquiv e)) a = ↑(↑(Equiv.symm (Equiv.sigmaCongrRight e)) (↑(Equiv.symm (Equiv.sigmaFiberEquiv g)) a)).snd

ink

def Equiv.ofFiberEquiv {α : 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

• Equiv.ofFiberEquiv e = Equiv.trans (Equiv.symm (Equiv.sigmaFiberEquiv f)) (Equiv.trans (Equiv.sigmaCongrRight e) (Equiv.sigmaFiberEquiv g))

ink

theorem Equiv.ofFiberEquiv_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} (e : (c : γ) → { a // f a = c } ≃ { b // g b = c }) (a : α) : g (↑(Equiv.ofFiberEquiv e) a) = f a

ink

@[simp]

theorem Equiv.prodShear_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} {α₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) : ↑(Equiv.prodShear e₁ e₂) = fun x => (↑e₁ x.fst, ↑(e₂ x.fst) x.snd)

ink

@[simp]

theorem Equiv.prodShear_symm_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} {α₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) : ↑(Equiv.symm (Equiv.prodShear e₁ e₂)) = fun y => (↑(Equiv.symm e₁) y.fst, ↑(Equiv.symm (e₂ (↑(Equiv.symm e₁) y.fst))) y.snd)

ink

def Equiv.prodShear {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} {α₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂

A variation on Equiv.prodCongr 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

• One or more equations did not get rendered due to their size.

ink

def Equiv.Perm.prodExtendRight {α₁ : Type u_1} {β₁ : Type u_2} [inst : DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) : Equiv.Perm (α₁ × β₁)

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.Perm.prodExtendRight_apply_eq {α₁ : Type u_2} {β₁ : Type u_1} [inst : DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) (b : β₁) : ↑(Equiv.Perm.prodExtendRight a e) (a, b) = (a, ↑e b)

ink

theorem Equiv.Perm.prodExtendRight_apply_ne {α₁ : Type u_1} {β₁ : Type u_2} [inst : DecidableEq α₁] (e : Equiv.Perm β₁) {a : α₁} {a' : α₁} (h : a' ≠ a) (b : β₁) : ↑(Equiv.Perm.prodExtendRight a e) (a', b) = (a', b)

ink

theorem Equiv.Perm.eq_of_prodExtendRight_ne {α₁ : Type u_2} {β₁ : Type u_1} [inst : DecidableEq α₁] {e : Equiv.Perm β₁} {a : α₁} {a' : α₁} {b : β₁} (h : ↑(Equiv.Perm.prodExtendRight a e) (a', b) ≠ (a', b)) : a' = a

ink

@[simp]

theorem Equiv.Perm.fst_prodExtendRight {α₁ : Type u_1} {β₁ : Type u_2} [inst : DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) (ab : α₁ × β₁) : (↑(Equiv.Perm.prodExtendRight a e) ab).fst = ab.fst

ink

def Equiv.arrowProdEquivProdArrow (α : 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

• One or more equations did not get rendered due to their size.

ink

def Equiv.sumArrowEquivProdArrow (α : 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

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.sumArrowEquivProdArrow_apply_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ⊕ β → γ) (a : α) : Prod.fst (α → γ) (β → γ) (↑(Equiv.sumArrowEquivProdArrow α β γ) f) a = f (Sum.inl a)

ink

@[simp]

theorem Equiv.sumArrowEquivProdArrow_apply_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ⊕ β → γ) (b : β) : Prod.snd (α → γ) (β → γ) (↑(Equiv.sumArrowEquivProdArrow α β γ) f) b = f (Sum.inr b)

ink

@[simp]

theorem Equiv.sumArrowEquivProdArrow_symm_apply_inl {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : α → γ) (g : β → γ) (a : α) : ↑(Equiv.symm (Equiv.sumArrowEquivProdArrow α β γ)) (f, g) (Sum.inl a) = f a

ink

@[simp]

theorem Equiv.sumArrowEquivProdArrow_symm_apply_inr {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : α → γ) (g : β → γ) (b : β) : ↑(Equiv.symm (Equiv.sumArrowEquivProdArrow α β γ)) (f, g) (Sum.inr b) = g b

ink

def Equiv.sumProdDistrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) : (α ⊕ β) × γ ≃ α × γ ⊕ β × γ

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.sumProdDistrib_apply_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} (a : α) (c : γ) : ↑(Equiv.sumProdDistrib α β γ) (Sum.inl a, c) = Sum.inl (a, c)

ink

@[simp]

theorem Equiv.sumProdDistrib_apply_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} (b : β) (c : γ) : ↑(Equiv.sumProdDistrib α β γ) (Sum.inr b, c) = Sum.inr (b, c)

ink

@[simp]

theorem Equiv.sumProdDistrib_symm_apply_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} (a : α × γ) : ↑(Equiv.symm (Equiv.sumProdDistrib α β γ)) (Sum.inl a) = (Sum.inl a.fst, a.snd)

ink

@[simp]

theorem Equiv.sumProdDistrib_symm_apply_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} (b : β × γ) : ↑(Equiv.symm (Equiv.sumProdDistrib α β γ)) (Sum.inr b) = (Sum.inr b.fst, b.snd)

ink

def Equiv.prodSumDistrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) : α × (β ⊕ γ) ≃ α × β ⊕ α × γ

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

Equations

• Equiv.prodSumDistrib α β γ = Trans.trans (Trans.trans (Equiv.prodComm α (β ⊕ γ)) (Equiv.sumProdDistrib β γ α)) (Equiv.sumCongr (Equiv.prodComm β α) (Equiv.prodComm γ α))

ink

@[simp]

theorem Equiv.prodSumDistrib_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (b : β) : ↑(Equiv.prodSumDistrib α β γ) (a, Sum.inl b) = Sum.inl (a, b)

ink

@[simp]

theorem Equiv.prodSumDistrib_apply_right {α : Type u_1} {γ : Type u_2} {β : Type u_3} (a : α) (c : γ) : ↑(Equiv.prodSumDistrib α β γ) (a, Sum.inr c) = Sum.inr (a, c)

ink

@[simp]

theorem Equiv.prodSumDistrib_symm_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α × β) : ↑(Equiv.symm (Equiv.prodSumDistrib α β γ)) (Sum.inl a) = (a.fst, Sum.inl a.snd)

ink

@[simp]

theorem Equiv.prodSumDistrib_symm_apply_right {α : Type u_1} {γ : Type u_2} {β : Type u_3} (a : α × γ) : ↑(Equiv.symm (Equiv.prodSumDistrib α β γ)) (Sum.inr a) = (a.fst, Sum.inr a.snd)

ink

@[simp]

theorem Equiv.sigmaSumDistrib_apply {ι : Type u_1} (α : ι → Type u_2) (β : ι → Type u_3) (p : (i : ι) × (α i ⊕ β i)) : ↑(Equiv.sigmaSumDistrib α β) p = Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd

ink

@[simp]

theorem Equiv.sigmaSumDistrib_symm_apply {ι : Type u_1} (α : ι → Type u_2) (β : ι → Type u_3) : ∀ (a : (i : ι) × α i ⊕ (i : ι) × β i), ↑(Equiv.symm (Equiv.sigmaSumDistrib α β)) a = Sum.elim (Sigma.map id fun x => Sum.inl) (Sigma.map id fun x => Sum.inr) a

ink

def Equiv.sigmaSumDistrib {ι : 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

• One or more equations did not get rendered due to their size.

ink

def Equiv.sigmaProdDistrib {ι : 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

• One or more equations did not get rendered due to their size.

ink

def Equiv.sigmaNatSucc (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

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.boolProdEquivSum_symm_apply (α : Type u_1) : ∀ (a : α ⊕ α), ↑(Equiv.symm (Equiv.boolProdEquivSum α)) a = Sum.elim (Prod.mk false) (Prod.mk true) a

ink

@[simp]

theorem Equiv.boolProdEquivSum_apply (α : Type u_1) (p : Bool × α) : ↑(Equiv.boolProdEquivSum α) p = bif p.fst then Sum.inr p.snd else Sum.inl p.snd

ink

def Equiv.boolProdEquivSum (α : Type u_1) : Bool × α ≃ α ⊕ α

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.boolArrowEquivProd_apply (α : Type u_1) (f : Bool → α) : ↑(Equiv.boolArrowEquivProd α) f = (f true, f false)

ink

@[simp]

theorem Equiv.boolArrowEquivProd_symm_apply (α : Type u_1) (p : α × α) (b : Bool) : ↑(Equiv.symm (Equiv.boolArrowEquivProd α)) p b = bif b then p.fst else p.snd

ink

def Equiv.boolArrowEquivProd (α : Type u_1) : (Bool → α) ≃ α × α

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.natEquivNatSumPUnit : ℕ ≃ ℕ ⊕ PUnit

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.natSumPUnitEquivNat : ℕ ⊕ PUnit ≃ ℕ

ℕ ⊕ Punit⊕ Punit is equivalent to ℕ.

Equations

• Equiv.natSumPUnitEquivNat = Equiv.symm Equiv.natEquivNatSumPUnit

ink

def Equiv.intEquivNatSumNat : ℤ ≃ ℕ ⊕ ℕ

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.listEquivOfEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) : List α ≃ List β

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.uniqueCongr {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) : Unique α ≃ Unique β

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

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Equiv.isEmpty_congr {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) : IsEmpty α ↔ IsEmpty β

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

ink

theorem Equiv.isEmpty {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) [inst : IsEmpty β] : IsEmpty α

ink

def Equiv.subtypeEquiv {α : Sort u_1} {β : Sort u_2} {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→ Prop and q : β → Prop→ 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.subtypePerm.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.subtypeEquiv_refl {α : Sort u_1} {p : α → Prop} (h : optParam (∀ (a : α), p a ↔ p (↑(Equiv.refl α) a)) (_ : ∀ (a : α), p a ↔ p a)) : Equiv.subtypeEquiv (Equiv.refl α) h = Equiv.refl { a // p a }

ink

@[simp]

theorem Equiv.subtypeEquiv_symm {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (↑e a)) : Equiv.symm (Equiv.subtypeEquiv e h) = Equiv.subtypeEquiv (Equiv.symm e) (_ : ∀ (a : β), q a ↔ p (↑(Equiv.symm e) a))

ink

@[simp]

theorem Equiv.subtypeEquiv_trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p : α → Prop} {q : β → Prop} {r : γ → Prop} (e : α ≃ β) (f : β ≃ γ) (h : ∀ (a : α), p a ↔ q (↑e a)) (h' : ∀ (b : β), q b ↔ r (↑f b)) : Equiv.trans (Equiv.subtypeEquiv e h) (Equiv.subtypeEquiv f h') = Equiv.subtypeEquiv (Equiv.trans e f) (_ : ∀ (a : α), p a ↔ r (↑(Equiv.trans e f) a))

ink

@[simp]

theorem Equiv.subtypeEquiv_apply {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (↑e a)) (x : { x // p x }) : ↑(Equiv.subtypeEquiv e h) x = { val := ↑e ↑x, property := Iff.mp (h ↑x) x.property }

ink

@[simp]

theorem Equiv.subtypeEquivRight_apply_coe {α : Sort u_1} {p : α → Prop} {q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (a : { a // (fun x => p x) a }) : ↑(↑(Equiv.subtypeEquivRight e) a) = ↑a

ink

@[simp]

theorem Equiv.subtypeEquivRight_symm_apply_coe {α : Sort u_1} {p : α → Prop} {q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (b : { b // (fun x => q x) b }) : ↑(↑(Equiv.symm (Equiv.subtypeEquivRight e)) b) = ↑b

ink

def Equiv.subtypeEquivRight {α : Sort u_1} {p : α → Prop} {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

• Equiv.subtypeEquivRight e = Equiv.subtypeEquiv (Equiv.refl α) e

ink

def Equiv.subtypeEquivOfSubtype {β : Sort u_1} {α : Sort u_2} {p : β → Prop} (e : α ≃ β) : { a // p (↑e a) } ≃ { b // p b }

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

Equations

• Equiv.subtypeEquivOfSubtype e = Equiv.subtypeEquiv e (_ : ∀ (a : α), p (↑e a) ↔ p (↑e a))

ink

def Equiv.subtypeEquivOfSubtype' {α : Sort u_1} {β : Sort u_2} {p : α → Prop} (e : α ≃ β) : { a // p a } ≃ { b // p (↑(Equiv.symm e) b) }

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

Equations

• Equiv.subtypeEquivOfSubtype' e = Equiv.symm (Equiv.subtypeEquivOfSubtype (Equiv.symm e))

ink

def Equiv.subtypeEquivProp {α : Sort u_1} {p : α → Prop} {q : α → Prop} (h : p = q) : Subtype p ≃ Subtype q

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

Equations

• Equiv.subtypeEquivProp h = Equiv.subtypeEquiv (Equiv.refl α) (_ : ∀ (x : α), p x ↔ q (↑(Equiv.refl α) x))

ink

@[simp]

theorem Equiv.subtypeSubtypeEquivSubtypeExists_apply_coe {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) (a : Subtype q) : ↑(↑(Equiv.subtypeSubtypeEquivSubtypeExists p q) a) = ↑↑a

ink

@[simp]

theorem Equiv.subtypeSubtypeEquivSubtypeExists_symm_apply_coe_coe {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) (a : { a // ∃ h, q { val := a, property := h } }) : ↑↑(↑(Equiv.symm (Equiv.subtypeSubtypeEquivSubtypeExists p q)) a) = ↑a

ink

def Equiv.subtypeSubtypeEquivSubtypeExists {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) : Subtype q ≃ { a // ∃ h, q { val := a, property := 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

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe {α : Type u} (p : α → Prop) (q : α → Prop) : ∀ (a : { x // q ↑x }), ↑(↑(Equiv.subtypeSubtypeEquivSubtypeInter p q) a) = ↑↑a

ink

@[simp]

theorem Equiv.subtypeSubtypeEquivSubtypeInter_symm_apply_coe_coe {α : Type u} (p : α → Prop) (q : α → Prop) : ∀ (a : { x // p x ∧ q x }), ↑↑(↑(Equiv.symm (Equiv.subtypeSubtypeEquivSubtypeInter p q)) a) = ↑a

ink

def Equiv.subtypeSubtypeEquivSubtypeInter {α : Type u} (p : α → Prop) (q : α → Prop) : { x // q ↑x } ≃ { x // p x ∧ q x }

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

Equations

• Equiv.subtypeSubtypeEquivSubtypeInter p q = Equiv.trans (Equiv.subtypeSubtypeEquivSubtypeExists p fun x => q ↑x) (Equiv.subtypeEquivRight (_ : ∀ (x : α), (∃ _h, q x) ↔ p x ∧ q x))

ink

@[simp]

theorem Equiv.subtypeSubtypeEquivSubtype_apply_coe {α : Type u_1} {p : α → Prop} {q : α → Prop} (h : {x : α} → q x → p x) : ∀ (a : { x // q ↑x }), ↑(↑(Equiv.subtypeSubtypeEquivSubtype h) a) = ↑↑a

ink

@[simp]

theorem Equiv.subtypeSubtypeEquivSubtype_symm_apply_coe_coe {α : Type u_1} {p : α → Prop} {q : α → Prop} (h : {x : α} → q x → p x) : ∀ (a : Subtype q), ↑↑(↑(Equiv.symm (Equiv.subtypeSubtypeEquivSubtype h)) a) = ↑a

ink

def Equiv.subtypeSubtypeEquivSubtype {α : Type u_1} {p : α → Prop} {q : α → Prop} (h : {x : α} → q x → p x) : { x // q ↑x } ≃ Subtype q

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

Equations

• Equiv.subtypeSubtypeEquivSubtype h = Equiv.trans (Equiv.subtypeSubtypeEquivSubtypeInter p q) (Equiv.subtypeEquivRight (_ : ∀ (x : α), p x ∧ q x ↔ q x))

ink

@[simp]

theorem Equiv.subtypeUnivEquiv_symm_apply {α : Type u_1} {p : α → Prop} (h : (x : α) → p x) (x : α) : ↑(Equiv.symm (Equiv.subtypeUnivEquiv h)) x = { val := x, property := h x }

ink

@[simp]

theorem Equiv.subtypeUnivEquiv_apply {α : Type u_1} {p : α → Prop} (h : (x : α) → p x) (x : Subtype p) : ↑(Equiv.subtypeUnivEquiv h) x = ↑x

ink

def Equiv.subtypeUnivEquiv {α : Type u_1} {p : α → Prop} (h : (x : α) → p x) : Subtype p ≃ α

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.subtypeSigmaEquiv {α : Type u_1} (p : α → Type v) (q : α → Prop) : { y // q y.fst } ≃ (x : Subtype q) × p ↑x

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.sigmaSubtypeEquivOfSubset {α : Type u_1} (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

• Equiv.sigmaSubtypeEquivOfSubset p q h = Equiv.trans (Equiv.symm (Equiv.subtypeSigmaEquiv p q)) (Equiv.subtypeUnivEquiv (Equiv.sigmaSubtypeEquivOfSubset.proof_1 p q h))

ink

def Equiv.sigmaSubtypeFiberEquiv {α : Type u_1} {β : Type u_2} (f : α → β) (p : β → Prop) (h : (x : α) → p (f x)) : (y : Subtype p) × { x // f x = ↑y } ≃ α

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

Equations

• Equiv.sigmaSubtypeFiberEquiv f p h = Trans.trans (Equiv.sigmaSubtypeEquivOfSubset (fun y => { x // f x = y }) p (Equiv.sigmaSubtypeFiberEquiv.proof_1 f p h)) (Equiv.sigmaFiberEquiv f)

ink

def Equiv.sigmaSubtypeFiberEquivSubtype {α : Type u_1} {β : Type u_2} (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)↔ q (f x), then Σ y : {y // q y}, f ⁻¹' {y}⁻¹' {y} is equivalent to {x // p x}.

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.sigmaOptionEquivOfSome {α : Type u_1} (p : Option α → Type v) (h : p none → False) : (x : Option α) × p x ≃ (x : α) × p (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

• One or more equations did not get rendered due to their size.

ink

def Equiv.piEquivSubtypeSigma (ι : Type u_1) (π : ι → Type u_2) : ((i : ι) → π i) ≃ { f // ∀ (i : ι), (f i).fst = i }

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.subtypePiEquivPi {α : Sort u_1} {β : α → Sort v} {p : (a : α) → β a → Prop} : { f // (a : α) → p a (f a) } ≃ ((a : α) → { b // p a b })

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

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.subtypeProdEquivProd {α : Type u_1} {β : Type u_2} {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

• One or more equations did not get rendered due to their size.

ink

def Equiv.subtypeProdEquivSigmaSubtype {α : 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

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.piEquivPiSubtypeProd_symm_apply {α : Type u_1} (p : α → Prop) (β : α → Type u_2) [inst : DecidablePred p] (f : ((i : { x // p x }) → β ↑i) × ((i : { x // ¬p x }) → β ↑i)) (x : α) : ↑(Equiv.symm (Equiv.piEquivPiSubtypeProd p β)) f x = if h : p x then Prod.fst ((i : { x // p x }) → β ↑i) ((i : { x // ¬p x }) → β ↑i) f { val := x, property := h } else Prod.snd ((i : { x // p x }) → β ↑i) ((i : { x // ¬p x }) → β ↑i) f { val := x, property := h }

ink

@[simp]

theorem Equiv.piEquivPiSubtypeProd_apply {α : Type u_1} (p : α → Prop) (β : α → Type u_2) [inst : DecidablePred p] (f : (i : α) → β i) : ↑(Equiv.piEquivPiSubtypeProd p β) f = (fun x => f ↑x, fun x => f ↑x)

ink

def Equiv.piEquivPiSubtypeProd {α : Type u_1} (p : α → Prop) (β : α → Type u_2) [inst : DecidablePred p] : ((i : α) → β i) ≃ ((i : { x // p x }) → β ↑i) × ((i : { x // ¬p x }) → β ↑i)

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.piSplitAt_symm_apply {α : Type u_1} [inst : DecidableEq α] (i : α) (β : α → Type u_2) (f : β i × ((j : { j // j ≠ i }) → β ↑j)) (j : α) : ↑(Equiv.symm (Equiv.piSplitAt i β)) f j = if h : j = i then (_ : i = j) ▸ f.fst else Prod.snd (β i) ((j : { j // j ≠ i }) → β ↑j) f { val := j, property := h }

ink

@[simp]

theorem Equiv.piSplitAt_apply {α : Type u_1} [inst : DecidableEq α] (i : α) (β : α → Type u_2) (f : (j : α) → β j) : ↑(Equiv.piSplitAt i β) f = (f i, fun j => f ↑j)

ink

def Equiv.piSplitAt {α : Type u_1} [inst : DecidableEq α] (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

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.funSplitAt_apply {α : Type u_1} [inst : DecidableEq α] (i : α) (β : Type u_2) (f : (j : α) → (fun a => β) j) : ↑(Equiv.funSplitAt i β) f = (f i, fun j => f ↑j)

ink

@[simp]

theorem Equiv.funSplitAt_symm_apply {α : Type u_1} [inst : DecidableEq α] (i : α) (β : Type u_2) (f : (fun a => β) i × ((j : { j // j ≠ i }) → (fun a => β) ↑j)) (j : α) : ↑(Equiv.symm (Equiv.funSplitAt i β)) f j = if h : j = i then f.fst else Prod.snd β ({ j // ¬j = i } → β) f { val := j, property := (_ : ¬j = i) }

ink

def Equiv.funSplitAt {α : Type u_1} [inst : DecidableEq α] (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

• Equiv.funSplitAt i β = Equiv.piSplitAt i fun a => β

ink

def Equiv.subtypeEquivCodomain {X : Sort u_1} [inst : DecidableEq X] {x : X} {Y : Sort u_2} (f : { x' // x' ≠ x } → Y) : { g // g ∘ Subtype.val = f } ≃ Y

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

Equations

• Equiv.subtypeEquivCodomain f = Equiv.trans (Equiv.subtypePreimage (fun a => a ≠ x) f) (Equiv.funUnique { x' // ¬x' ≠ x } Y)

ink

@[simp]

theorem Equiv.coe_subtypeEquivCodomain {X : Sort u_2} [inst : DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' // x' ≠ x } → Y) : ↑(Equiv.subtypeEquivCodomain f) = fun g => ↑g x

ink

@[simp]

theorem Equiv.subtypeEquivCodomain_apply {X : Sort u_2} [inst : DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' // x' ≠ x } → Y) (g : { g // g ∘ Subtype.val = f }) : ↑(Equiv.subtypeEquivCodomain f) g = ↑g x

ink

theorem Equiv.coe_subtypeEquivCodomain_symm {X : Sort u_2} [inst : DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' // x' ≠ x } → Y) : ↑(Equiv.symm (Equiv.subtypeEquivCodomain f)) = fun y => { val := fun x' => if h : x' ≠ x then f { val := x', property := h } else y, property := (_ : (fun x' => if h : x' ≠ x then f { val := x', property := h } else y) ∘ Subtype.val = f) }

ink

@[simp]

theorem Equiv.subtypeEquivCodomain_symm_apply {X : Sort u_2} [inst : DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' // x' ≠ x } → Y) (y : Y) (x' : X) : ↑(↑(Equiv.symm (Equiv.subtypeEquivCodomain f)) y) x' = if h : x' ≠ x then f { val := x', property := h } else y

ink

theorem Equiv.subtypeEquivCodomain_symm_apply_eq {X : Sort u_2} [inst : DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' // x' ≠ x } → Y) (y : Y) : ↑(↑(Equiv.symm (Equiv.subtypeEquivCodomain f)) y) x = y

ink

theorem Equiv.subtypeEquivCodomain_symm_apply_ne {X : Sort u_2} [inst : DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' // x' ≠ x } → Y) (y : Y) (x' : X) (h : x' ≠ x) : ↑(↑(Equiv.symm (Equiv.subtypeEquivCodomain f)) y) x' = f { val := x', property := h }

ink

@[simp]

theorem Equiv.ofBijective_apply {α : Sort u_1} {β : Sort u_2} (f : α → β) (hf : Function.Bijective f) : ∀ (a : α), ↑(Equiv.ofBijective f hf) a = f a

ink

noncomputable def Equiv.ofBijective {α : Sort u_1} {β : Sort u_2} (f : α → β) (hf : Function.Bijective f) : α ≃ β

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

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Equiv.ofBijective_apply_symm_apply {α : Sort u_1} {β : Sort u_2} (f : α → β) (hf : Function.Bijective f) (x : β) : f (↑(Equiv.symm (Equiv.ofBijective f hf)) x) = x

ink

@[simp]

theorem Equiv.ofBijective_symm_apply_apply {α : Sort u_1} {β : Sort u_2} (f : α → β) (hf : Function.Bijective f) (x : α) : ↑(Equiv.symm (Equiv.ofBijective f hf)) (f x) = x

ink

instance Equiv.instCanLiftForAllEquivCoeInstFunLikeEquivBijective {α : Sort u_1} {β : Sort u_2} : CanLift (α → β) (α ≃ β) FunLike.coe Function.Bijective

Equations

• Equiv.instCanLiftForAllEquivCoeInstFunLikeEquivBijective = { prf := (_ : ∀ (f : α → β), Function.Bijective f → ∃ y, ↑y = f) }

ink

def Equiv.Perm.extendDomain {α' : Type u_1} {β' : Type u_2} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p) : Equiv.Perm β'

Extend the domain of e : Equiv.Perm α to one that is over β via f : α → Subtype p→ Subtype p, where p : β → Prop→ 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_leftInverse' or Equiv.of_leftInverse when there is a known inverse, or Equiv.ofInjective in the general case.`.

Equations

• Equiv.Perm.extendDomain e f = Equiv.Perm.subtypeCongr (↑(Equiv.permCongr f) e) (Equiv.refl { a // ¬p a })

ink

@[simp]

theorem Equiv.Perm.extendDomain_apply_image {α' : Type u_2} {β' : Type u_1} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p) (a : α') : ↑(Equiv.Perm.extendDomain e f) ↑(↑f a) = ↑(↑f (↑e a))

ink

theorem Equiv.Perm.extendDomain_apply_subtype {α' : Type u_2} {β' : Type u_1} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p) {b : β'} (h : p b) : ↑(Equiv.Perm.extendDomain e f) b = ↑(↑f (↑e (↑(Equiv.symm f) { val := b, property := h })))

ink

theorem Equiv.Perm.extendDomain_apply_not_subtype {α' : Type u_2} {β' : Type u_1} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p) {b : β'} (h : ¬p b) : ↑(Equiv.Perm.extendDomain e f) b = b

ink

@[simp]

theorem Equiv.Perm.extendDomain_refl {α' : Type u_2} {β' : Type u_1} {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p) : Equiv.Perm.extendDomain (Equiv.refl α') f = Equiv.refl β'

ink

@[simp]

theorem Equiv.Perm.extendDomain_symm {α' : Type u_2} {β' : Type u_1} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p) : Equiv.symm (Equiv.Perm.extendDomain e f) = Equiv.Perm.extendDomain (Equiv.symm e) f

ink

theorem Equiv.Perm.extendDomain_trans {α' : Type u_1} {β' : Type u_2} {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p) (e : Equiv.Perm α') (e' : Equiv.Perm α') : Equiv.trans (Equiv.Perm.extendDomain e f) (Equiv.Perm.extendDomain e' f) = Equiv.Perm.extendDomain (Equiv.trans e e') f

ink

def Equiv.subtypeQuotientEquivQuotientSubtype {α : Sort u_1} (p₁ : α → Prop) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)] (p₂ : Quotient s₁ → Prop) (hp₂ : ∀ (a : α), p₁ a ↔ p₂ (Quotient.mk s₁ 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⟧↔ 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

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.subtypeQuotientEquivQuotientSubtype_mk {α : Sort u_1} (p₁ : α → Prop) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)] (p₂ : Quotient s₁ → Prop) (hp₂ : ∀ (a : α), p₁ a ↔ p₂ (Quotient.mk s₁ a)) (h : ∀ (x y : Subtype p₁), Setoid.r x y ↔ ↑x ≈ ↑y) (x : α) (hx : p₂ (Quotient.mk s₁ x)) : ↑(Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h) { val := Quotient.mk s₁ x, property := hx } = Quotient.mk s₂ { val := x, property := Iff.mpr (hp₂ x) hx }

ink

@[simp]

theorem Equiv.subtypeQuotientEquivQuotientSubtype_symm_mk {α : Sort u_1} (p₁ : α → Prop) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)] (p₂ : Quotient s₁ → Prop) (hp₂ : ∀ (a : α), p₁ a ↔ p₂ (Quotient.mk s₁ a)) (h : ∀ (x y : Subtype p₁), Setoid.r x y ↔ ↑x ≈ ↑y) (x : Subtype p₁) : ↑(Equiv.symm (Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h)) (Quotient.mk s₂ x) = { val := Quotient.mk s₁ ↑x, property := Iff.mp (hp₂ ↑x) x.property }

ink

def Equiv.swapCore {α : Sort u_1} [inst : DecidableEq α] (a : α) (b : α) (r : α) : α

A helper function for Equiv.swap.

Equations

• Equiv.swapCore a b r = if r = a then b else if r = b then a else r

ink

theorem Equiv.swapCore_self {α : Sort u_1} [inst : DecidableEq α] (r : α) (a : α) : Equiv.swapCore a a r = r

ink

theorem Equiv.swapCore_swapCore {α : Sort u_1} [inst : DecidableEq α] (r : α) (a : α) (b : α) : Equiv.swapCore a b (Equiv.swapCore a b r) = r

ink

theorem Equiv.swapCore_comm {α : Sort u_1} [inst : DecidableEq α] (r : α) (a : α) (b : α) : Equiv.swapCore a b r = Equiv.swapCore b a r

ink

def Equiv.swap {α : Sort u_1} [inst : DecidableEq α] (a : α) (b : α) : Equiv.Perm α

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Equiv.swap_self {α : Sort u_1} [inst : DecidableEq α] (a : α) : Equiv.swap a a = Equiv.refl α

ink

theorem Equiv.swap_comm {α : Sort u_1} [inst : DecidableEq α] (a : α) (b : α) : Equiv.swap a b = Equiv.swap b a

ink

theorem Equiv.swap_apply_def {α : Sort u_1} [inst : DecidableEq α] (a : α) (b : α) (x : α) : ↑(Equiv.swap a b) x = if x = a then b else if x = b then a else x

ink

@[simp]

theorem Equiv.swap_apply_left {α : Sort u_1} [inst : DecidableEq α] (a : α) (b : α) : ↑(Equiv.swap a b) a = b

ink

@[simp]

theorem Equiv.swap_apply_right {α : Sort u_1} [inst : DecidableEq α] (a : α) (b : α) : ↑(Equiv.swap a b) b = a

ink

theorem Equiv.swap_apply_of_ne_of_ne {α : Sort u_1} [inst : DecidableEq α] {a : α} {b : α} {x : α} : x ≠ a → x ≠ b → ↑(Equiv.swap a b) x = x

ink

@[simp]

theorem Equiv.swap_swap {α : Sort u_1} [inst : DecidableEq α] (a : α) (b : α) : Equiv.trans (Equiv.swap a b) (Equiv.swap a b) = Equiv.refl α

ink

@[simp]

theorem Equiv.symm_swap {α : Sort u_1} [inst : DecidableEq α] (a : α) (b : α) : Equiv.symm (Equiv.swap a b) = Equiv.swap a b

ink

@[simp]

theorem Equiv.swap_eq_refl_iff {α : Sort u_1} [inst : DecidableEq α] {x : α} {y : α} : Equiv.swap x y = Equiv.refl α ↔ x = y

ink

theorem Equiv.swap_comp_apply {α : Sort u_1} [inst : DecidableEq α] {a : α} {b : α} {x : α} (π : Equiv.Perm α) : ↑(Equiv.trans π (Equiv.swap a b)) x = if ↑π x = a then b else if ↑π x = b then a else ↑π x

ink

theorem Equiv.swap_eq_update {α : Sort u_1} [inst : DecidableEq α] (i : α) (j : α) : ↑(Equiv.swap i j) = Function.update (Function.update id j i) i j

ink

theorem Equiv.comp_swap_eq_update {α : Sort u_2} [inst : DecidableEq α] {β : Sort u_1} (i : α) (j : α) (f : α → β) : f ∘ ↑(Equiv.swap i j) = Function.update (Function.update f j (f i)) i (f j)

ink

@[simp]

theorem Equiv.symm_trans_swap_trans {α : Sort u_2} [inst : DecidableEq α] {β : Sort u_1} [inst : DecidableEq β] (a : α) (b : α) (e : α ≃ β) : Equiv.trans (Equiv.trans (Equiv.symm e) (Equiv.swap a b)) e = Equiv.swap (↑e a) (↑e b)

ink

@[simp]

theorem Equiv.trans_swap_trans_symm {α : Sort u_2} [inst : DecidableEq α] {β : Sort u_1} [inst : DecidableEq β] (a : β) (b : β) (e : α ≃ β) : Equiv.trans (Equiv.trans e (Equiv.swap a b)) (Equiv.symm e) = Equiv.swap (↑(Equiv.symm e) a) (↑(Equiv.symm e) b)

ink

@[simp]

theorem Equiv.swap_apply_self {α : Sort u_1} [inst : DecidableEq α] (i : α) (j : α) (a : α) : ↑(Equiv.swap i j) (↑(Equiv.swap i j) a) = a

ink

theorem Equiv.apply_swap_eq_self {α : Sort u_2} [inst : DecidableEq α] {β : Sort u_1} {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

ink

theorem Equiv.swap_apply_eq_iff {α : Sort u_1} [inst : DecidableEq α] {x : α} {y : α} {z : α} {w : α} : ↑(Equiv.swap x y) z = w ↔ z = ↑(Equiv.swap x y) w

ink

theorem Equiv.swap_apply_ne_self_iff {α : Sort u_1} [inst : DecidableEq α] {a : α} {b : α} {x : α} : ↑(Equiv.swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

ink

@[simp]

theorem Equiv.Perm.sumCongr_swap_refl {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] (i : α) (j : α) : Equiv.Perm.sumCongr (Equiv.swap i j) (Equiv.refl β) = Equiv.swap (Sum.inl i) (Sum.inl j)

ink

@[simp]

theorem Equiv.Perm.sumCongr_refl_swap {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] (i : β) (j : β) : Equiv.Perm.sumCongr (Equiv.refl α) (Equiv.swap i j) = Equiv.swap (Sum.inr i) (Sum.inr j)

ink

def Equiv.setValue {α : Sort u_1} [inst : DecidableEq α] {β : Sort u_2} (f : α ≃ β) (a : α) (b : β) : α ≃ β

Augment an equivalence with a prescribed mapping f a = b

Equations

• Equiv.setValue f a b = Equiv.trans (Equiv.swap a (↑(Equiv.symm f) b)) f

ink

@[simp]

theorem Equiv.setValue_eq {α : Sort u_2} [inst : DecidableEq α] {β : Sort u_1} (f : α ≃ β) (a : α) (b : β) : ↑(Equiv.setValue f a b) a = b

ink

def Function.Involutive.toPerm {α : Sort u_1} (f : α → α) (h : Function.Involutive f) : Equiv.Perm α

Convert an involutive function f to a permutation with toFun = invFun = f.

Equations

• Function.Involutive.toPerm f h = { toFun := f, invFun := f, left_inv := (_ : Function.LeftInverse f f), right_inv := (_ : Function.RightInverse f f) }

ink

@[simp]

theorem Function.Involutive.coe_toPerm {α : Sort u_1} {f : α → α} (h : Function.Involutive f) : ↑(Function.Involutive.toPerm f h) = f

ink

@[simp]

theorem Function.Involutive.toPerm_symm {α : Sort u_1} {f : α → α} (h : Function.Involutive f) : Equiv.symm (Function.Involutive.toPerm f h) = Function.Involutive.toPerm f h

ink

theorem Function.Involutive.toPerm_involutive {α : Sort u_1} {f : α → α} (h : Function.Involutive f) : Function.Involutive ↑(Function.Involutive.toPerm f h)

ink

theorem PLift.eq_up_iff_down_eq {α : Sort u_1} {x : PLift α} {y : α} : x = { down := y } ↔ x.down = y

ink

theorem Function.Injective.map_swap {α : Sort u_1} {β : Sort u_2} [inst : DecidableEq α] [inst : DecidableEq β] {f : α → β} (hf : Function.Injective f) (x : α) (y : α) (z : α) : f (↑(Equiv.swap x y) z) = ↑(Equiv.swap (f x) (f y)) (f z)

ink

@[simp]

theorem Equiv.piCongrLeft'_apply {α : Sort u_1} {β : Sort u_2} (P : α → Sort u_3) (e : α ≃ β) (f : (a : α) → P a) (x : β) : ↑(Equiv.piCongrLeft' P e) f x = f (↑(Equiv.symm e) x)

ink

@[simp]

theorem Equiv.piCongrLeft'_symm_apply {α : Sort u_1} {β : Sort u_2} (P : α → Sort u_3) (e : α ≃ β) (f : (b : β) → P (↑(Equiv.symm e) b)) (x : α) : ↑(Equiv.symm (Equiv.piCongrLeft' P e)) f x = (_ : ↑(Equiv.symm e) (↑e x) = x) ▸ f (↑e x)

ink

def Equiv.piCongrLeft' {α : Sort u_1} {β : Sort u_2} (P : α → Sort u_3) (e : α ≃ β) : ((a : α) → P a) ≃ ((b : β) → P (↑(Equiv.symm e) b))

Transport dependent functions through an equivalence of the base space.

Equations

• One or more equations did not get rendered due to their size.

ink

def Equiv.piCongrLeft {β : Sort u_1} {α : Sort u_2} (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

• Equiv.piCongrLeft P e = Equiv.symm (Equiv.piCongrLeft' P (Equiv.symm e))

ink

def Equiv.piCongr {α : Sort u_1} {β : Sort u_2} {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

• Equiv.piCongr h₁ h₂ = Equiv.trans (Equiv.piCongrRight h₂) (Equiv.piCongrLeft Z h₁)

ink

@[simp]

theorem Equiv.coe_piCongr_symm {α : Sort u_2} {β : Sort u_1} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (↑h₁ a)) : ↑(Equiv.symm (Equiv.piCongr h₁ h₂)) = fun f a => ↑(Equiv.symm (h₂ a)) (f (↑h₁ a))

ink

theorem Equiv.piCongr_symm_apply {α : Sort u_1} {β : Sort u_2} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (↑h₁ a)) (f : (b : β) → Z b) : ↑(Equiv.symm (Equiv.piCongr h₁ h₂)) f = fun a => ↑(Equiv.symm (h₂ a)) (f (↑h₁ a))

ink

@[simp]

theorem Equiv.piCongr_apply_apply {α : Sort u_1} {β : Sort u_2} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (↑h₁ a)) (f : (a : α) → W a) (a : α) : ↑(Equiv.piCongr h₁ h₂) f (↑h₁ a) = ↑(h₂ a) (f a)

ink

def Equiv.piCongr' {α : Sort u_1} {β : Sort u_2} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (↑(Equiv.symm h₁) 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

• Equiv.piCongr' h₁ h₂ = Equiv.symm (Equiv.piCongr (Equiv.symm h₁) fun b => Equiv.symm (h₂ b))

ink

@[simp]

theorem Equiv.coe_piCongr' {α : Sort u_1} {β : Sort u_2} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (↑(Equiv.symm h₁) b) ≃ Z b) : ↑(Equiv.piCongr' h₁ h₂) = fun f b => ↑(h₂ b) (f (↑(Equiv.symm h₁) b))

ink

theorem Equiv.piCongr'_apply {α : Sort u_2} {β : Sort u_1} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (↑(Equiv.symm h₁) b) ≃ Z b) (f : (a : α) → W a) : ↑(Equiv.piCongr' h₁ h₂) f = fun b => ↑(h₂ b) (f (↑(Equiv.symm h₁) b))

ink

@[simp]

theorem Equiv.piCongr'_symm_apply_symm_apply {α : Sort u_1} {β : Sort u_2} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (↑(Equiv.symm h₁) b) ≃ Z b) (f : (b : β) → Z b) (b : β) : ↑(Equiv.symm (Equiv.piCongr' h₁ h₂)) f (↑(Equiv.symm h₁) b) = ↑(Equiv.symm (h₂ b)) (f b)

ink

theorem Equiv.semiconj_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁) : Function.Semiconj (↑e) f (↑(Equiv.conj e) f)

ink

theorem Equiv.semiconj₂_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) : Function.Semiconj₂ (↑e) f (↑(Equiv.arrowCongr e (Equiv.conj e)) f)

ink

instance Equiv.instIsAssociativeCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [inst : IsAssociative α₁ f] : IsAssociative β₁ (↑(Equiv.arrowCongr e (Equiv.arrowCongr e e)) f)

Equations

• @Equiv.instIsAssociativeCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll = @Equiv.instIsAssociativeCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll.proof_1

ink

instance Equiv.instIsIdempotentCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [inst : IsIdempotent α₁ f] : IsIdempotent β₁ (↑(Equiv.arrowCongr e (Equiv.arrowCongr e e)) f)

Equations

• @Equiv.instIsIdempotentCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll = @Equiv.instIsIdempotentCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll.proof_1

ink

instance Equiv.instIsLeftCancelCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [inst : IsLeftCancel α₁ f] : IsLeftCancel β₁ (↑(Equiv.arrowCongr e (Equiv.arrowCongr e e)) f)

Equations

• @Equiv.instIsLeftCancelCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll = @Equiv.instIsLeftCancelCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll.proof_1

ink

instance Equiv.instIsRightCancelCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [inst : IsRightCancel α₁ f] : IsRightCancel β₁ (↑(Equiv.arrowCongr e (Equiv.arrowCongr e e)) f)

Equations

• @Equiv.instIsRightCancelCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll = @Equiv.instIsRightCancelCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll.proof_1

ink

theorem Function.Injective.swap_apply {α : Sort u_1} {β : Sort u_2} [inst : DecidableEq α] [inst : DecidableEq β] {f : α → β} (hf : Function.Injective f) (x : α) (y : α) (z : α) : ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)

ink

theorem Function.Injective.swap_comp {α : Sort u_1} {β : Sort u_2} [inst : DecidableEq α] [inst : DecidableEq β] {f : α → β} (hf : Function.Injective f) (x : α) (y : α) : ↑(Equiv.swap (f x) (f y)) ∘ f = f ∘ ↑(Equiv.swap x y)

ink

def subsingletonProdSelfEquiv {α : Type u_1} [inst : Subsingleton α] : α × α ≃ α

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

Equations

• One or more equations did not get rendered due to their size.

ink

def equivOfSubsingletonOfSubsingleton {α : Sort u_1} {β : Sort u_2} [inst : Subsingleton α] [inst : Subsingleton β] (f : α → β) (g : β → α) : α ≃ β

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

Equations

• equivOfSubsingletonOfSubsingleton f g = { toFun := f, invFun := g, left_inv := (_ : ∀ (x : α), g (f x) = x), right_inv := (_ : ∀ (x : β), f (g x) = x) }

ink

noncomputable def Equiv.punitOfNonemptyOfSubsingleton {α : Sort u_1} [h : Nonempty α] [inst : Subsingleton α] : α ≃ PUnit

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

Equations

• Equiv.punitOfNonemptyOfSubsingleton = equivOfSubsingletonOfSubsingleton (fun x => PUnit.unit) fun x => Nonempty.some h

ink

def uniqueUniqueEquiv {α : Sort u_1} : Unique (Unique α) ≃ Unique α

Unique (Unique α) is equivalent to Unique α.

Equations

• uniqueUniqueEquiv = equivOfSubsingletonOfSubsingleton (fun h => default) fun h => { toInhabited := { default := h }, uniq := (_ : ∀ (x : Unique α), x = default) }

ink

theorem Function.update_comp_equiv {α' : Sort u_1} {α : Sort u_2} {β : Sort u_3} [inst : DecidableEq α'] [inst : DecidableEq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) : Function.update f a v ∘ ↑g = Function.update (f ∘ ↑g) (↑(Equiv.symm g) a) v

ink

theorem Function.update_apply_equiv_apply {α' : Sort u_1} {α : Sort u_2} {β : Sort u_3} [inst : DecidableEq α'] [inst : DecidableEq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) (a' : α') : Function.update f a v (↑g a') = Function.update (f ∘ ↑g) (↑(Equiv.symm g) a) v a'

ink

theorem Function.piCongrLeft'_update {α : Sort u_1} {β : Sort u_2} [inst : DecidableEq α] [inst : DecidableEq β] (P : α → Sort u_3) (e : α ≃ β) (f : (a : α) → P a) (b : β) (x : P (↑(Equiv.symm e) b)) : ↑(Equiv.piCongrLeft' P e) (Function.update f (↑(Equiv.symm e) b) x) = Function.update (↑(Equiv.piCongrLeft' P e) f) b x

ink

theorem Function.piCongrLeft'_symm_update {α : Sort u_1} {β : Sort u_2} [inst : DecidableEq α] [inst : DecidableEq β] (P : α → Sort u_3) (e : α ≃ β) (f : (b : β) → P (↑(Equiv.symm e) b)) (b : β) (x : P (↑(Equiv.symm e) b)) : ↑(Equiv.symm (Equiv.piCongrLeft' P e)) (Function.update f b x) = Function.update (↑(Equiv.symm (Equiv.piCongrLeft' P e)) f) (↑(Equiv.symm e) b) x