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, b.casesOn α β;

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

Tags

equivalence, congruence, bijective map

def Equiv.pprodEquivProd {α : Type u_9} {β : Type u_10} : α ×' β ≃ α × β

PProd α β is equivalent to α × β

Equations

• Equiv.pprodEquivProd = { toFun := fun (x : α ×' β) => (x.fst, x.snd), invFun := fun (x : α × β) => ⟨x.1, x.2⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.pprodEquivProd_apply {α : Type u_9} {β : Type u_10} (x : α ×' β) : Equiv.pprodEquivProd x = (x.fst, x.snd)

@[simp]

theorem Equiv.pprodEquivProd_symm_apply {α : Type u_9} {β : Type u_10} (x : α × β) : Equiv.pprodEquivProd.symm x = ⟨x.1, x.2⟩

def Equiv.pprodCongr {α : Sort u_1} {β : Sort u_4} {γ : Sort u_7} {δ : Sort u_8} (e₁ : α ≃ β) (e₂ : γ ≃ δ) : α ×' γ ≃ β ×' δ

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

Equations

• e₁.pprodCongr e₂ = { toFun := fun (x : α ×' γ) => ⟨e₁ x.fst, e₂ x.snd⟩, invFun := fun (x : β ×' δ) => ⟨e₁.symm x.fst, e₂.symm x.snd⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.pprodCongr_apply {α : Sort u_1} {β : Sort u_4} {γ : Sort u_7} {δ : Sort u_8} (e₁ : α ≃ β) (e₂ : γ ≃ δ) (x : α ×' γ) : (e₁.pprodCongr e₂) x = ⟨e₁ x.fst, e₂ x.snd⟩

def Equiv.pprodProd {α₁ : Sort u_2} {β₁ : Sort u_5} {α₂ : Type u_9} {β₂ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ×' β₁ ≃ α₂ × β₂

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

Equations

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

@[simp]

theorem Equiv.pprodProd_apply {α₁ : Sort u_2} {β₁ : Sort u_5} {α₂ : Type u_9} {β₂ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : ∀ (a : α₁ ×' β₁), (ea.pprodProd eb) a = (ea a.fst, eb a.snd)

@[simp]

theorem Equiv.pprodProd_symm_apply {α₁ : Sort u_2} {β₁ : Sort u_5} {α₂ : Type u_9} {β₂ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : ∀ (a : α₂ × β₂), (ea.pprodProd eb).symm a = (ea.pprodCongr eb).symm ⟨a.1, a.2⟩

def Equiv.prodPProd {α₂ : Sort u_3} {β₂ : Sort u_6} {α₁ : Type u_9} {β₁ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ ×' β₂

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

Equations

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

@[simp]

theorem Equiv.prodPProd_symm_apply {α₂ : Sort u_3} {β₂ : Sort u_6} {α₁ : Type u_9} {β₁ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : ∀ (a : α₂ ×' β₂), (ea.prodPProd eb).symm a = (ea.symm a.fst, eb.symm a.snd)

@[simp]

theorem Equiv.prodPProd_apply {α₂ : Sort u_3} {β₂ : Sort u_6} {α₁ : Type u_9} {β₁ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : ∀ (a : α₁ × β₁), (ea.prodPProd eb) a = (ea.symm.pprodCongr eb.symm).symm ⟨a.1, a.2⟩

def Equiv.pprodEquivProdPLift {α : Sort u_1} {β : Sort u_4} : α ×' β ≃ PLift α × PLift β

PProd α β is equivalent to PLift α × PLift β

Equations

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

@[simp]

theorem Equiv.pprodEquivProdPLift_symm_apply {α : Sort u_1} {β : Sort u_4} : ∀ (a : PLift α × PLift β), Equiv.pprodEquivProdPLift.symm a = (Equiv.plift.symm.pprodCongr Equiv.plift.symm).symm ⟨a.1, a.2⟩

@[simp]

theorem Equiv.pprodEquivProdPLift_apply {α : Sort u_1} {β : Sort u_4} : ∀ (a : α ×' β), Equiv.pprodEquivProdPLift a = (Equiv.plift.symm a.fst, Equiv.plift.symm a.snd)

def Equiv.prodCongr {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂

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

Equations

• e₁.prodCongr e₂ = { toFun := Prod.map ⇑e₁ ⇑e₂, invFun := Prod.map ⇑e₁.symm ⇑e₂.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.prodCongr_apply {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : ⇑(e₁.prodCongr e₂) = Prod.map ⇑e₁ ⇑e₂

@[simp]

theorem Equiv.prodCongr_symm {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm

def Equiv.prodComm (α : Type u_9) (β : Type u_10) : α × β ≃ β × α

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 := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.coe_prodComm (α : Type u_9) (β : Type u_10) : ⇑(Equiv.prodComm α β) = Prod.swap

@[simp]

theorem Equiv.prodComm_apply {α : Type u_9} {β : Type u_10} (x : α × β) : (Equiv.prodComm α β) x = x.swap

@[simp]

theorem Equiv.prodComm_symm (α : Type u_9) (β : Type u_10) : (Equiv.prodComm α β).symm = Equiv.prodComm β α

def Equiv.prodAssoc (α : Type u_9) (β : Type u_10) (γ : Type u_11) : (α × β) × γ ≃ α × β × γ

Type product is associative up to an equivalence.

Equations

• Equiv.prodAssoc α β γ = { toFun := fun (p : (α × β) × γ) => (p.1.1, p.1.2, p.2), invFun := fun (p : α × β × γ) => ((p.1, p.2.1), p.2.2), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.prodAssoc_symm_apply (α : Type u_9) (β : Type u_10) (γ : Type u_11) (p : α × β × γ) : (Equiv.prodAssoc α β γ).symm p = ((p.1, p.2.1), p.2.2)

@[simp]

theorem Equiv.prodAssoc_apply (α : Type u_9) (β : Type u_10) (γ : Type u_11) (p : (α × β) × γ) : (Equiv.prodAssoc α β γ) p = (p.1.1, p.1.2, p.2)

def Equiv.prodProdProdComm (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) : (α × β) × γ × δ ≃ (α × γ) × β × δ

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

Equations

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

@[simp]

theorem Equiv.prodProdProdComm_apply (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) (abcd : (α × β) × γ × δ) : (Equiv.prodProdProdComm α β γ δ) abcd = ((abcd.1.1, abcd.2.1), abcd.1.2, abcd.2.2)

@[simp]

theorem Equiv.prodProdProdComm_symm (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) : (Equiv.prodProdProdComm α β γ δ).symm = Equiv.prodProdProdComm α γ β δ

def Equiv.curry (α : Type u_9) (β : Type u_10) (γ : Sort u_11) : (α × β → γ) ≃ (α → β → γ)

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

Equations

• Equiv.curry α β γ = { toFun := Function.curry, invFun := Function.uncurry, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.curry_apply (α : Type u_9) (β : Type u_10) (γ : Sort u_11) : ⇑(Equiv.curry α β γ) = Function.curry

@[simp]

theorem Equiv.curry_symm_apply (α : Type u_9) (β : Type u_10) (γ : Sort u_11) : ⇑(Equiv.curry α β γ).symm = Function.uncurry

def Equiv.prodPUnit (α : Type u_9) : α × PUnit.{u_10 + 1} ≃ α

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

Equations

• Equiv.prodPUnit α = { toFun := fun (p : α × PUnit.{?u.13 + 1} ) => p.1, invFun := fun (a : α) => (a, PUnit.unit), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.prodPUnit_apply (α : Type u_9) (p : α × PUnit.{u_10 + 1} ) : (Equiv.prodPUnit α) p = p.1

@[simp]

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

def Equiv.punitProd (α : Type u_9) : PUnit.{u_10 + 1} × α ≃ α

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

Equations

• Equiv.punitProd α = Trans.trans (Equiv.prodComm PUnit.{?u.11 + 1} α) (Equiv.prodPUnit α)

@[simp]

theorem Equiv.punitProd_apply (α : Type u_9) : ∀ (a : PUnit.{u_10 + 1} × α), (Equiv.punitProd α) a = a.2

@[simp]

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

def Equiv.sigmaPUnit (α : Type u_9) : (_ : α) × PUnit.{u_10 + 1} ≃ α

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

Equations

• Equiv.sigmaPUnit α = { toFun := fun (p : (_ : α) × PUnit.{?u.15 + 1} ) => p.fst, invFun := fun (a : α) => ⟨a, PUnit.unit⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.sigmaPUnit_apply (α : Type u_9) (p : (_ : α) × PUnit.{u_10 + 1} ) : (Equiv.sigmaPUnit α) p = p.fst

@[simp]

theorem Equiv.sigmaPUnit_symm_apply_snd (α : Type u_9) (a : α) : ((Equiv.sigmaPUnit α).symm a).snd = PUnit.unit

@[simp]

theorem Equiv.sigmaPUnit_symm_apply_fst (α : Type u_9) (a : α) : ((Equiv.sigmaPUnit α).symm a).fst = a

def Equiv.prodUnique (α : Type u_9) (β : Type u_10) [Unique β] : α × β ≃ α

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

Equations

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

@[simp]

theorem Equiv.coe_prodUnique {α : Type u_9} {β : Type u_10} [Unique β] : ⇑(Equiv.prodUnique α β) = Prod.fst

theorem Equiv.prodUnique_apply {α : Type u_9} {β : Type u_10} [Unique β] (x : α × β) : (Equiv.prodUnique α β) x = x.1

@[simp]

theorem Equiv.prodUnique_symm_apply {α : Type u_9} {β : Type u_10} [Unique β] (x : α) : (Equiv.prodUnique α β).symm x = (x, default)

def Equiv.uniqueProd (α : Type u_9) (β : Type u_10) [Unique β] : β × α ≃ α

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

Equations

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

@[simp]

theorem Equiv.coe_uniqueProd {α : Type u_9} {β : Type u_10} [Unique β] : ⇑(Equiv.uniqueProd α β) = Prod.snd

theorem Equiv.uniqueProd_apply {α : Type u_9} {β : Type u_10} [Unique β] (x : β × α) : (Equiv.uniqueProd α β) x = x.2

@[simp]

theorem Equiv.uniqueProd_symm_apply {α : Type u_9} {β : Type u_10} [Unique β] (x : α) : (Equiv.uniqueProd α β).symm x = (default, x)

def Equiv.sigmaUnique (α : Type u_10) (β : α → Type u_9) [(a : α) → Unique (β a)] : (a : α) × β a ≃ α

Any family of Unique types is a right identity for dependent type product up to equivalence.

Equations

• Equiv.sigmaUnique α β = (Equiv.sigmaCongrRight fun (a : α) => Equiv.equivPUnit (β a)).trans (Equiv.sigmaPUnit α)

@[simp]

theorem Equiv.coe_sigmaUnique {α : Type u_10} {β : α → Type u_9} [(a : α) → Unique (β a)] : ⇑(Equiv.sigmaUnique α β) = Sigma.fst

theorem Equiv.sigmaUnique_apply {α : Type u_10} {β : α → Type u_9} [(a : α) → Unique (β a)] (x : (a : α) × β a) : (Equiv.sigmaUnique α β) x = x.fst

@[simp]

theorem Equiv.sigmaUnique_symm_apply {α : Type u_10} {β : α → Type u_9} [(a : α) → Unique (β a)] (x : α) : (Equiv.sigmaUnique α β).symm x = ⟨x, default⟩

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

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

Equations

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

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

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

Equations

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

def Equiv.prodPEmpty (α : Type u_9) : α × PEmpty.{u_10 + 1} ≃ PEmpty.{u_11}

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

Equations

• Equiv.prodPEmpty α = Equiv.equivPEmpty (α × PEmpty.{?u.12 + 1} )

def Equiv.pemptyProd (α : Type u_9) : PEmpty.{u_10 + 1} × α ≃ PEmpty.{u_11}

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

Equations

• Equiv.pemptyProd α = Equiv.equivPEmpty (PEmpty.{?u.12 + 1} × α)

def Equiv.psumEquivSum (α : Type u_9) (β : Type u_10) : α ⊕' β ≃ α ⊕ β

PSum is equivalent to Sum.

Equations

• Equiv.psumEquivSum α β = { toFun := fun (s : α ⊕' β) => PSum.casesOn s Sum.inl Sum.inr, invFun := Sum.elim PSum.inl PSum.inr, left_inv := ⋯, right_inv := ⋯ }

def Equiv.sumCongr {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂

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

Equations

• ea.sumCongr eb = { toFun := Sum.map ⇑ea ⇑eb, invFun := Sum.map ⇑ea.symm ⇑eb.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.sumCongr_apply {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : ∀ (a : α₁ ⊕ β₁), (ea.sumCongr eb) a = Sum.map (⇑ea) (⇑eb) a

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

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

Equations

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

def Equiv.psumSum {α₁ : Sort u_2} {β₁ : Sort u_5} {α₂ : Type u_9} {β₂ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕' β₁ ≃ α₂ ⊕ β₂

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

Equations

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

def Equiv.sumPSum {α₂ : Sort u_3} {β₂ : Sort u_6} {α₁ : Type u_9} {β₁ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕ β₁ ≃ α₂ ⊕' β₂

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

Equations

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

@[simp]

theorem Equiv.sumCongr_trans {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} {γ₁ : Type u_13} {γ₂ : Type u_14} (e : α₁ ≃ β₁) (f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂) : (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)

@[simp]

theorem Equiv.sumCongr_symm {α : Type u_9} {β : Type u_10} {γ : Type u_11} {δ : Type u_12} (e : α ≃ β) (f : γ ≃ δ) : (e.sumCongr f).symm = e.symm.sumCongr f.symm

@[simp]

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

def Equiv.subtypeSum {α : Type u_9} {β : Type u_10} {p : α ⊕ β → Prop} : { c : α ⊕ β // p c } ≃ { a : α // p (Sum.inl a) } ⊕ { b : β // p (Sum.inr b) }

A subtype of a sum is equivalent to a sum of subtypes.

Equations

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

@[reducible, inline]

abbrev Equiv.Perm.sumCongr {α : Type u_9} {β : Type u_10} (ea : Equiv.Perm α) (eb : Equiv.Perm β) : Equiv.Perm (α ⊕ β)

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

Equations

• ea.sumCongr eb = Equiv.sumCongr ea eb

@[simp]

theorem Equiv.Perm.sumCongr_apply {α : Type u_9} {β : Type u_10} (ea : Equiv.Perm α) (eb : Equiv.Perm β) (x : α ⊕ β) : (ea.sumCongr eb) x = Sum.map (⇑ea) (⇑eb) x

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

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

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

def Equiv.boolEquivPUnitSumPUnit : Bool ≃ PUnit.{u + 1} ⊕ PUnit.{v + 1}

Bool is equivalent the sum of two PUnits.

Equations

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

def Equiv.sumComm (α : Type u_9) (β : Type u_10) : α ⊕ β ≃ β ⊕ α

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 := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.sumComm_apply (α : Type u_9) (β : Type u_10) : ⇑(Equiv.sumComm α β) = Sum.swap

@[simp]

theorem Equiv.sumComm_symm (α : Type u_9) (β : Type u_10) : (Equiv.sumComm α β).symm = Equiv.sumComm β α

def Equiv.sumAssoc (α : Type u_9) (β : Type u_10) (γ : Type u_11) : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ

Sum of types is associative up to an equivalence.

Equations

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

@[simp]

theorem Equiv.sumAssoc_apply_inl_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) : (Equiv.sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a

@[simp]

theorem Equiv.sumAssoc_apply_inl_inr {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β) : (Equiv.sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)

@[simp]

theorem Equiv.sumAssoc_apply_inr {α : Type u_9} {β : Type u_10} {γ : Type u_11} (c : γ) : (Equiv.sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)

@[simp]

theorem Equiv.sumAssoc_symm_apply_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) : (Equiv.sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)

@[simp]

theorem Equiv.sumAssoc_symm_apply_inr_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β) : (Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)

@[simp]

theorem Equiv.sumAssoc_symm_apply_inr_inr {α : Type u_9} {β : Type u_10} {γ : Type u_11} (c : γ) : (Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c

def Equiv.sumSumSumComm (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) : (α ⊕ β) ⊕ γ ⊕ δ ≃ (α ⊕ γ) ⊕ β ⊕ δ

Four-way commutativity of sum. The name matches add_add_add_comm.

Equations

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

@[simp]

theorem Equiv.sumSumSumComm_apply (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) : ∀ (a : (α ⊕ β) ⊕ γ ⊕ δ), (Equiv.sumSumSumComm α β γ δ) a = (⇑(Equiv.sumAssoc (α ⊕ γ) β δ) ∘ Sum.map (⇑(Equiv.sumAssoc α γ β).symm) id ∘ Sum.map (Sum.map id ⇑(Equiv.sumComm β γ)) id ∘ Sum.map (⇑(Equiv.sumAssoc α β γ)) id ∘ ⇑(Equiv.sumAssoc (α ⊕ β) γ δ).symm) a

@[simp]

theorem Equiv.sumSumSumComm_symm (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) : (Equiv.sumSumSumComm α β γ δ).symm = Equiv.sumSumSumComm α γ β δ

def Equiv.sumEmpty (α : Type u_9) (β : Type u_10) [IsEmpty β] : α ⊕ β ≃ α

Sum with IsEmpty is equivalent to the original type.

Equations

• Equiv.sumEmpty α β = { toFun := Sum.elim id fun (a : β) => isEmptyElim a, invFun := Sum.inl, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.sumEmpty_symm_apply (α : Type u_9) (β : Type u_10) [IsEmpty β] (val : α) : (Equiv.sumEmpty α β).symm val = Sum.inl val

@[simp]

theorem Equiv.sumEmpty_apply_inl {α : Type u_9} {β : Type u_10} [IsEmpty β] (a : α) : (Equiv.sumEmpty α β) (Sum.inl a) = a

def Equiv.emptySum (α : Type u_9) (β : Type u_10) [IsEmpty α] : α ⊕ β ≃ β

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

Equations

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

@[simp]

theorem Equiv.emptySum_symm_apply (α : Type u_9) (β : Type u_10) [IsEmpty α] : ∀ (a : β), (Equiv.emptySum α β).symm a = Sum.inr a

@[simp]

theorem Equiv.emptySum_apply_inr {α : Type u_9} {β : Type u_10} [IsEmpty α] (b : β) : (Equiv.emptySum α β) (Sum.inr b) = b

def Equiv.optionEquivSumPUnit (α : Type u_9) : Option α ≃ α ⊕ PUnit.{u_10 + 1}

Option α is equivalent to α ⊕ PUnit

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Equiv.optionEquivSumPUnit_symm_inr {α : Type u_9} (a : PUnit.{u_10 + 1} ) : (Equiv.optionEquivSumPUnit α).symm (Sum.inr a) = none

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

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

Equations

• Equiv.optionIsSomeEquiv α = { toFun := fun (o : { x : Option α // x.isSome = true }) => (↑o).get ⋯, invFun := fun (x : α) => ⟨some x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

def Equiv.piOptionEquivProd {α : Type u_10} {β : Option α → Type u_9} : ((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.

@[simp]

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

@[simp]

theorem Equiv.piOptionEquivProd_symm_apply {α : Type u_10} {β : Option α → Type u_9} (x : β none × ((a : α) → β (some a))) (a : Option α) : Equiv.piOptionEquivProd.symm x a = Option.casesOn a x.1 x.2

def Equiv.sumEquivSigmaBool (α : Type u_9) (β : Type u_9) : α ⊕ β ≃ (b : Bool) × Bool.casesOn 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 be 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.

def Equiv.sigmaFiberEquiv {α : Type u_9} {β : Type u_10} (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

• Equiv.sigmaFiberEquiv f = { toFun := fun (x : (y : β) × { x : α // f x = y }) => ↑x.snd, invFun := fun (x : α) => ⟨f x, ⟨x, ⋯⟩⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem Equiv.sigmaFiberEquiv_symm_apply_fst {α : Type u_9} {β : Type u_10} (f : α → β) (x : α) : ((Equiv.sigmaFiberEquiv f).symm x).fst = f x

def Equiv.sigmaEquivOptionOfInhabited (α : Type u) [Inhabited α] [DecidableEq α] : (β : Type u) × (α ≃ Option β)

Inhabited types are equivalent to Option β for some β by identifying default with none.

Equations

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

def Equiv.sumCompl {α : Type u_9} (p : α → Prop) [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} 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

• Equiv.sumCompl p = { toFun := Sum.elim Subtype.val Subtype.val, invFun := fun (a : α) => if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem Equiv.sumCompl_apply_symm_of_pos {α : Type u_9} (p : α → Prop) [DecidablePred p] (a : α) (h : p a) : (Equiv.sumCompl p).symm a = Sum.inl ⟨a, h⟩

@[simp]

theorem Equiv.sumCompl_apply_symm_of_neg {α : Type u_9} (p : α → Prop) [DecidablePred p] (a : α) (h : ¬p a) : (Equiv.sumCompl p).symm a = Sum.inr ⟨a, h⟩

def Equiv.subtypeCongr {α : Type u_9} {p : α → Prop} {q : α → Prop} [DecidablePred p] [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

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

def Equiv.Perm.subtypeCongr {ε : Type u_9} {p : ε → Prop} [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 constructs a permutation on ε.

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Equiv.Perm.subtypeCongr.trans {ε : Type u_9} {p : ε → Prop} [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 (ep.subtypeCongr en) (ep'.subtypeCongr en') = Equiv.Perm.subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')

def Equiv.subtypePreimage {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [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} → β.

Equations

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

@[simp]

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

@[simp]

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

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

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

def Equiv.piCongrRight {α : Sort u_1} {β₁ : α → Sort u_9} {β₂ : α → Sort u_10} (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

• Equiv.piCongrRight F = { toFun := Pi.map fun (a : α) => ⇑(F a), invFun := Pi.map fun (a : α) => ⇑(F a).symm, left_inv := ⋯, right_inv := ⋯ }

def Equiv.piComm {α : Sort u_1} {β : Sort u_4} (φ : α → β → Sort u_9) : ((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

• Equiv.piComm φ = { toFun := Function.swap, invFun := Function.swap, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

def Equiv.piCurry {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) : ((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

• Equiv.piCurry γ = { toFun := Sigma.curry, invFun := Sigma.uncurry, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.piCurry_apply {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) (f : (x : (i : α) × β i) → γ x.fst x.snd) : (Equiv.piCurry γ) f = Sigma.curry f

@[simp]

theorem Equiv.piCurry_symm_apply {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) (f : (a : α) → (b : β a) → γ a b) : (Equiv.piCurry γ).symm f = Sigma.uncurry f

def Equiv.prodCongrLeft {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) : β₁ × α₁ ≃ β₂ × α₁

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

Equations

• Equiv.prodCongrLeft e = { toFun := fun (ab : β₁ × α₁) => ((e ab.2) ab.1, ab.2), invFun := fun (ab : β₂ × α₁) => ((e ab.2).symm ab.1, ab.2), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.prodCongrLeft_apply {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (b : β₁) (a : α₁) : (Equiv.prodCongrLeft e) (b, a) = ((e a) b, a)

theorem Equiv.prodCongr_refl_right {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : β₁ ≃ β₂) : e.prodCongr (Equiv.refl α₁) = Equiv.prodCongrLeft fun (x : α₁) => e

def Equiv.prodCongrRight {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) : α₁ × β₁ ≃ α₁ × β₂

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

Equations

• Equiv.prodCongrRight e = { toFun := fun (ab : α₁ × β₁) => (ab.1, (e ab.1) ab.2), invFun := fun (ab : α₁ × β₂) => (ab.1, (e ab.1).symm ab.2), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.prodCongrRight_apply {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (a : α₁) (b : β₁) : (Equiv.prodCongrRight e) (a, b) = (a, (e a) b)

theorem Equiv.prodCongr_refl_left {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : β₁ ≃ β₂) : (Equiv.refl α₁).prodCongr e = Equiv.prodCongrRight fun (x : α₁) => e

@[simp]

theorem Equiv.prodCongrLeft_trans_prodComm {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) : (Equiv.prodCongrLeft e).trans (Equiv.prodComm β₂ α₁) = (Equiv.prodComm β₁ α₁).trans (Equiv.prodCongrRight e)

@[simp]

theorem Equiv.prodCongrRight_trans_prodComm {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) : (Equiv.prodCongrRight e).trans (Equiv.prodComm α₁ β₂) = (Equiv.prodComm α₁ β₁).trans (Equiv.prodCongrLeft e)

theorem Equiv.sigmaCongrRight_sigmaEquivProd {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) : (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂) = (Equiv.sigmaEquivProd α₁ β₁).trans (Equiv.prodCongrRight e)

theorem Equiv.sigmaEquivProd_sigmaCongrRight {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) : (Equiv.sigmaEquivProd α₁ β₁).symm.trans (Equiv.sigmaCongrRight e) = (Equiv.prodCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂).symm

def Equiv.ofFiberEquiv {α : Type u_13} {β : Type u_14} {γ : Type u_15} {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.sigmaFiberEquiv f).symm.trans ((Equiv.sigmaCongrRight e).trans (Equiv.sigmaFiberEquiv g))

@[simp]

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

@[simp]

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

theorem Equiv.ofFiberEquiv_map {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : α → γ} {g : β → γ} (e : (c : γ) → { a : α // f a = c } ≃ { b : β // g b = c }) (a : α) : g ((Equiv.ofFiberEquiv e) a) = f a

def Equiv.prodShear {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (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

• e₁.prodShear e₂ = { toFun := fun (x : α₁ × β₁) => (e₁ x.1, (e₂ x.1) x.2), invFun := fun (y : α₂ × β₂) => (e₁.symm y.1, (e₂ (e₁.symm y.1)).symm y.2), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.prodShear_symm_apply {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) : ⇑(e₁.prodShear e₂).symm = fun (y : α₂ × β₂) => (e₁.symm y.1, (e₂ (e₁.symm y.1)).symm y.2)

@[simp]

theorem Equiv.prodShear_apply {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) : ⇑(e₁.prodShear e₂) = fun (x : α₁ × β₁) => (e₁ x.1, (e₂ x.1) x.2)

def Equiv.Perm.prodExtendRight {α₁ : Type u_9} {β₁ : Type u_10} [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.

@[simp]

theorem Equiv.Perm.prodExtendRight_apply_eq {α₁ : Type u_9} {β₁ : Type u_10} [DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) (b : β₁) : (Equiv.Perm.prodExtendRight a e) (a, b) = (a, e b)

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

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

@[simp]

theorem Equiv.Perm.fst_prodExtendRight {α₁ : Type u_9} {β₁ : Type u_10} [DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) (ab : α₁ × β₁) : ((Equiv.Perm.prodExtendRight a e) ab).1 = ab.1

def Equiv.arrowProdEquivProdArrow (α : Type u_9) (β : Type u_10) (γ : Type u_11) : (γ → α × β) ≃ (γ → α) × (γ → β)

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.

def Equiv.sumPiEquivProdPi {ι : Type u_10} {ι' : Type u_11} (π : ι ⊕ ι' → Type u_9) : ((i : ι ⊕ ι') → π i) ≃ ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))

The type of dependent functions on a sum type ι ⊕ ι' is equivalent to the type of pairs of functions on ι and on ι'. This is a dependent version of Equiv.sumArrowEquivProdArrow.

Equations

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

@[simp]

theorem Equiv.sumPiEquivProdPi_apply {ι : Type u_10} {ι' : Type u_11} (π : ι ⊕ ι' → Type u_9) (f : (i : ι ⊕ ι') → π i) : (Equiv.sumPiEquivProdPi π) f = (fun (i : ι) => f (Sum.inl i), fun (i' : ι') => f (Sum.inr i'))

@[simp]

theorem Equiv.sumPiEquivProdPi_symm_apply {ι : Type u_10} {ι' : Type u_11} (π : ι ⊕ ι' → Type u_9) (g : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))) (t : ι ⊕ ι') : (Equiv.sumPiEquivProdPi π).symm g t = Sum.rec g.1 g.2 t

def Equiv.prodPiEquivSumPi {ι : Type u_9} {ι' : Type u_10} (π : ι → Type u) (π' : ι' → Type u) : ((i : ι) → π i) × ((i' : ι') → π' i') ≃ ((i : ι ⊕ ι') → Sum.elim π π' i)

The equivalence between a product of two dependent functions types and a single dependent function type. Basically a symmetric version of Equiv.sumPiEquivProdPi.

Equations

• Equiv.prodPiEquivSumPi π π' = (Equiv.sumPiEquivProdPi (Sum.elim π π')).symm

@[simp]

theorem Equiv.prodPiEquivSumPi_symm_apply {ι : Type u_9} {ι' : Type u_10} (π : ι → Type u) (π' : ι' → Type u) : ∀ (a : (i : ι ⊕ ι') → Sum.elim π π' i), (Equiv.prodPiEquivSumPi π π').symm a = (Equiv.sumPiEquivProdPi (Sum.elim π π')) a

@[simp]

theorem Equiv.prodPiEquivSumPi_apply {ι : Type u_9} {ι' : Type u_10} (π : ι → Type u) (π' : ι' → Type u) : ∀ (a : ((i : ι) → Sum.elim π π' (Sum.inl i)) × ((i' : ι') → Sum.elim π π' (Sum.inr i'))) (i : ι ⊕ ι'), (Equiv.prodPiEquivSumPi π π') a i = (Equiv.sumPiEquivProdPi (Sum.elim π π')).symm a i

def Equiv.sumArrowEquivProdArrow (α : Type u_9) (β : Type u_10) (γ : Type u_11) : (α ⊕ β → γ) ≃ (α → γ) × (β → γ)

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

Equations

• Equiv.sumArrowEquivProdArrow α β γ = { toFun := fun (f : α ⊕ β → γ) => (f ∘ Sum.inl, f ∘ Sum.inr), invFun := fun (p : (α → γ) × (β → γ)) => Sum.elim p.1 p.2, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.sumArrowEquivProdArrow_apply_fst {α : Type u_9} {β : Type u_10} {γ : Type u_11} (f : α ⊕ β → γ) (a : α) : ((Equiv.sumArrowEquivProdArrow α β γ) f).1 a = f (Sum.inl a)

@[simp]

theorem Equiv.sumArrowEquivProdArrow_apply_snd {α : Type u_9} {β : Type u_10} {γ : Type u_11} (f : α ⊕ β → γ) (b : β) : ((Equiv.sumArrowEquivProdArrow α β γ) f).2 b = f (Sum.inr b)

@[simp]

theorem Equiv.sumArrowEquivProdArrow_symm_apply_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (f : α → γ) (g : β → γ) (a : α) : (Equiv.sumArrowEquivProdArrow α β γ).symm (f, g) (Sum.inl a) = f a

@[simp]

theorem Equiv.sumArrowEquivProdArrow_symm_apply_inr {α : Type u_9} {β : Type u_10} {γ : Type u_11} (f : α → γ) (g : β → γ) (b : β) : (Equiv.sumArrowEquivProdArrow α β γ).symm (f, g) (Sum.inr b) = g b

def Equiv.sumProdDistrib (α : Type u_9) (β : Type u_10) (γ : Type u_11) : (α ⊕ β) × γ ≃ α × γ ⊕ β × γ

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.

@[simp]

theorem Equiv.sumProdDistrib_apply_left {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) (c : γ) : (Equiv.sumProdDistrib α β γ) (Sum.inl a, c) = Sum.inl (a, c)

@[simp]

theorem Equiv.sumProdDistrib_apply_right {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β) (c : γ) : (Equiv.sumProdDistrib α β γ) (Sum.inr b, c) = Sum.inr (b, c)

@[simp]

theorem Equiv.sumProdDistrib_symm_apply_left {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α × γ) : (Equiv.sumProdDistrib α β γ).symm (Sum.inl a) = (Sum.inl a.1, a.2)

@[simp]

theorem Equiv.sumProdDistrib_symm_apply_right {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β × γ) : (Equiv.sumProdDistrib α β γ).symm (Sum.inr b) = (Sum.inr b.1, b.2)

def Equiv.prodSumDistrib (α : Type u_9) (β : Type u_10) (γ : Type u_11) : α × (β ⊕ γ) ≃ α × β ⊕ α × γ

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.prodComm β α).sumCongr (Equiv.prodComm γ α))

@[simp]

theorem Equiv.prodSumDistrib_apply_left {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) (b : β) : (Equiv.prodSumDistrib α β γ) (a, Sum.inl b) = Sum.inl (a, b)

@[simp]

theorem Equiv.prodSumDistrib_apply_right {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) (c : γ) : (Equiv.prodSumDistrib α β γ) (a, Sum.inr c) = Sum.inr (a, c)

@[simp]

theorem Equiv.prodSumDistrib_symm_apply_left {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α × β) : (Equiv.prodSumDistrib α β γ).symm (Sum.inl a) = (a.1, Sum.inl a.2)

@[simp]

theorem Equiv.prodSumDistrib_symm_apply_right {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α × γ) : (Equiv.prodSumDistrib α β γ).symm (Sum.inr a) = (a.1, Sum.inr a.2)

def Equiv.sigmaSumDistrib {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) : (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.

@[simp]

theorem Equiv.sigmaSumDistrib_apply {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) (p : (i : ι) × (α i ⊕ β i)) : (Equiv.sigmaSumDistrib α β) p = Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd

@[simp]

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

def Equiv.sigmaProdDistrib {ι : Type u_10} (α : ι → Type u_9) (β : Type u_11) : ((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.

@[simp]

theorem Equiv.sigmaProdDistrib_apply {ι : Type u_10} (α : ι → Type u_9) (β : Type u_11) (p : ((i : ι) × α i) × β) : (Equiv.sigmaProdDistrib α β) p = ⟨p.1.fst, (p.1.snd, p.2)⟩

@[simp]

theorem Equiv.sigmaProdDistrib_symm_apply {ι : Type u_10} (α : ι → Type u_9) (β : Type u_11) (p : (i : ι) × α i × β) : (Equiv.sigmaProdDistrib α β).symm p = (⟨p.fst, p.snd.1⟩, p.snd.2)

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.

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

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

Equations

• Equiv.boolProdEquivSum α = { toFun := fun (p : Bool × α) => Bool.casesOn p.1 (Sum.inl p.2) (Sum.inr p.2), invFun := Sum.elim (Prod.mk false) (Prod.mk true), left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

theorem Equiv.boolProdEquivSum_apply (α : Type u_9) (p : Bool × α) : (Equiv.boolProdEquivSum α) p = Bool.casesOn p.1 (Sum.inl p.2) (Sum.inr p.2)

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

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

Equations

• Equiv.boolArrowEquivProd α = { toFun := fun (f : Bool → α) => (f false, f true), invFun := fun (p : α × α) (b : Bool) => Bool.casesOn b p.1 p.2, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

theorem Equiv.boolArrowEquivProd_symm_apply (α : Type u_9) (p : α × α) (b : Bool) : (Equiv.boolArrowEquivProd α).symm p b = Bool.casesOn b p.1 p.2

def Equiv.natEquivNatSumPUnit : ℕ ≃ ℕ ⊕ PUnit.{u_9 + 1}

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

Equations

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

def Equiv.natSumPUnitEquivNat : ℕ ⊕ PUnit.{u_9 + 1} ≃ ℕ

ℕ ⊕ PUnit is equivalent to ℕ.

Equations

• Equiv.natSumPUnitEquivNat = Equiv.natEquivNatSumPUnit.symm

def Equiv.intEquivNatSumNat : ℤ ≃ ℕ ⊕ ℕ

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

Equations

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

def Equiv.listEquivOfEquiv {α : Type u_9} {β : Type u_10} (e : α ≃ β) : List α ≃ List β

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

Equations

• e.listEquivOfEquiv = { toFun := List.map ⇑e, invFun := List.map ⇑e.symm, left_inv := ⋯, right_inv := ⋯ }

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

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

Equations

• e.uniqueCongr = { toFun := fun (h : Unique α) => e.symm.unique, invFun := fun (h : Unique β) => e.unique, left_inv := ⋯, right_inv := ⋯ }

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

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

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

def Equiv.subtypeEquiv {α : Sort u_1} {β : Sort u_4} {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.subtypePerm.

Equations

• e.subtypeEquiv h = { toFun := fun (a : { a : α // p a }) => ⟨e ↑a, ⋯⟩, invFun := fun (b : { b : β // q b }) => ⟨e.symm ↑b, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem Equiv.coe_subtypeEquiv_eq_map {X : Sort u_9} {Y : Sort u_10} {p : X → Prop} {q : Y → Prop} (e : X ≃ Y) (h : ∀ (x : X), p x ↔ q (e x)) : ⇑(e.subtypeEquiv h) = Subtype.map ⇑e ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Equiv.subtypeEquiv_apply {α : Sort u_1} {β : Sort u_4} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) (x : { x : α // p x }) : (e.subtypeEquiv h) x = ⟨e ↑x, ⋯⟩

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.refl α).subtypeEquiv e

@[simp]

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

@[simp]

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

theorem Equiv.subtypeEquivRight_apply {α : Sort u_1} {p : α → Prop} {q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (z : { x : α // p x }) : (Equiv.subtypeEquivRight e) z = ⟨↑z, ⋯⟩

theorem Equiv.subtypeEquivRight_symm_apply {α : Sort u_1} {p : α → Prop} {q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (z : { x : α // q x }) : (Equiv.subtypeEquivRight e).symm z = ⟨↑z, ⋯⟩

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

• e.subtypeEquivOfSubtype = e.subtypeEquiv ⋯

def Equiv.subtypeEquivOfSubtype' {α : Sort u_1} {β : Sort u_4} {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

• e.subtypeEquivOfSubtype' = e.symm.subtypeEquivOfSubtype.symm

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.refl α).subtypeEquiv ⋯

def Equiv.subtypeSubtypeEquivSubtypeExists {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) : Subtype q ≃ { a : α // ∃ (h : p a), q ⟨a, h⟩ }

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

Equations

• Equiv.subtypeSubtypeEquivSubtypeExists p q = { toFun := fun (a : Subtype q) => ⟨↑↑a, ⋯⟩, invFun := fun (a : { a : α // ∃ (h : p a), q ⟨a, h⟩ }) => ⟨⟨↑a, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

def Equiv.subtypeSubtypeEquivSubtypeInter {α : Type u} (p : α → Prop) (q : α → Prop) : { x : Subtype p // 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.subtypeSubtypeEquivSubtypeExists p fun (x : Subtype p) => q ↑x).trans (Equiv.subtypeEquivRight ⋯)

@[simp]

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

@[simp]

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

def Equiv.subtypeSubtypeEquivSubtype {α : Type u_9} {p : α → Prop} {q : α → Prop} (h : ∀ {x : α}, q x → p x) : { x : Subtype p // 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.subtypeSubtypeEquivSubtypeInter p q).trans (Equiv.subtypeEquivRight ⋯)

@[simp]

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

@[simp]

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

def Equiv.subtypeUnivEquiv {α : Type u_9} {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

• Equiv.subtypeUnivEquiv h = { toFun := fun (x : Subtype p) => ↑x, invFun := fun (x : α) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

theorem Equiv.subtypeUnivEquiv_symm_apply {α : Type u_9} {p : α → Prop} (h : ∀ (x : α), p x) (x : α) : (Equiv.subtypeUnivEquiv h).symm x = ⟨x, ⋯⟩

def Equiv.subtypeSigmaEquiv {α : Type u_9} (p : α → Type v) (q : α → Prop) : { y : Sigma p // 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.

def Equiv.sigmaSubtypeEquivOfSubset {α : Type u_9} (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.subtypeSigmaEquiv p q).symm.trans (Equiv.subtypeUnivEquiv ⋯)

def Equiv.sigmaSubtypeFiberEquiv {α : Type u_9} {β : Type u_10} (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

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

def Equiv.sigmaSubtypeFiberEquivSubtype {α : Type u_9} {β : Type u_10} (f : α → β) {p : α → Prop} {q : β → Prop} (h : ∀ (x : α), p x ↔ q (f x)) : (y : Subtype q) × { x : α // f x = ↑y } ≃ Subtype p

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

Equations

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

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

• Equiv.sigmaOptionEquivOfSome p h = (Equiv.sigmaSubtypeEquivOfSubset p (fun (x : Option α) => x.isSome = true) ⋯).symm.trans (Equiv.optionIsSomeEquiv α).sigmaCongrLeft'

def Equiv.piEquivSubtypeSigma (ι : Type u_10) (π : ι → Type u_9) : ((i : ι) → π i) ≃ { f : ι → (i : ι) × π i // ∀ (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

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

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

The type of functions f : ∀ 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}.

Equations

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

def Equiv.subtypeProdEquivProd {α : Type u_9} {β : Type u_10} {p : α → Prop} {q : β → Prop} : { c : α × β // p c.1 ∧ q c.2 } ≃ { 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.

def Equiv.prodSubtypeFstEquivSubtypeProd {α : Type u_9} {β : Type u_10} {p : α → Prop} : { s : α × β // p s.1 } ≃ { a : α // p a } × β

A subtype of a Prod that depends only on the first component is equivalent to the corresponding subtype of the first type times the second type.

Equations

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

def Equiv.subtypeProdEquivSigmaSubtype {α : Type u_9} {β : Type u_10} (p : α → β → Prop) : { x : α × β // p x.1 x.2 } ≃ (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.

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

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

Equations

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

@[simp]

theorem Equiv.piEquivPiSubtypeProd_apply {α : Type u_9} (p : α → Prop) (β : α → Type u_10) [DecidablePred p] (f : (i : α) → β i) : (Equiv.piEquivPiSubtypeProd p β) f = (fun (x : { x : α // p x }) => f ↑x, fun (x : { x : α // ¬p x }) => f ↑x)

@[simp]

theorem Equiv.piEquivPiSubtypeProd_symm_apply {α : Type u_9} (p : α → Prop) (β : α → Type u_10) [DecidablePred p] (f : ((i : { x : α // p x }) → β ↑i) × ((i : { x : α // ¬p x }) → β ↑i)) (x : α) : (Equiv.piEquivPiSubtypeProd p β).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩

def Equiv.piSplitAt {α : Type u_9} [DecidableEq α] (i : α) (β : α → Type u_10) : ((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.

@[simp]

theorem Equiv.piSplitAt_symm_apply {α : Type u_9} [DecidableEq α] (i : α) (β : α → Type u_10) (f : β i × ((j : { j : α // j ≠ i }) → β ↑j)) (j : α) : (Equiv.piSplitAt i β).symm f j = if h : j = i then ⋯ ▸ f.1 else f.2 ⟨j, h⟩

@[simp]

theorem Equiv.piSplitAt_apply {α : Type u_9} [DecidableEq α] (i : α) (β : α → Type u_10) (f : (j : α) → β j) : (Equiv.piSplitAt i β) f = (f i, fun (j : { j : α // j ≠ i }) => f ↑j)

def Equiv.funSplitAt {α : Type u_9} [DecidableEq α] (i : α) (β : Type u_10) : (α → β) ≃ β × ({ 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 : α) => β

@[simp]

theorem Equiv.funSplitAt_apply {α : Type u_9} [DecidableEq α] (i : α) (β : Type u_10) (f : (j : α) → (fun (a : α) => β) j) : (Equiv.funSplitAt i β) f = (f i, fun (j : { j : α // ¬j = i }) => f ↑j)

@[simp]

theorem Equiv.funSplitAt_symm_apply {α : Type u_9} [DecidableEq α] (i : α) (β : Type u_10) (f : (fun (a : α) => β) i × ((j : { j : α // j ≠ i }) → (fun (a : α) => β) ↑j)) (j : α) : (Equiv.funSplitAt i β).symm f j = if h : j = i then f.1 else f.2 ⟨j, ⋯⟩

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

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

Equations

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

@[simp]

theorem Equiv.coe_subtypeEquivCodomain {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) : ⇑(Equiv.subtypeEquivCodomain f) = fun (g : { g : X → Y // g ∘ Subtype.val = f }) => ↑g x

@[simp]

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

theorem Equiv.coe_subtypeEquivCodomain_symm {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) : ⇑(Equiv.subtypeEquivCodomain f).symm = fun (y : Y) => ⟨fun (x' : X) => if h : x' ≠ x then f ⟨x', h⟩ else y, ⋯⟩

@[simp]

theorem Equiv.subtypeEquivCodomain_symm_apply {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) (y : Y) (x' : X) : ↑((Equiv.subtypeEquivCodomain f).symm y) x' = if h : x' ≠ x then f ⟨x', h⟩ else y

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

theorem Equiv.subtypeEquivCodomain_symm_apply_ne {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) (y : Y) (x' : X) (h : x' ≠ x) : ↑((Equiv.subtypeEquivCodomain f).symm y) x' = f ⟨x', h⟩

instance Equiv.instCanLiftForallCoeBijective {α : Sort u_1} {β : Sort u_4} : CanLift (α → β) (α ≃ β) DFunLike.coe Function.Bijective

Equations

• ⋯ = ⋯

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

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_leftInverse' or Equiv.of_leftInverse when there is a known inverse, or Equiv.ofInjective in the general case.

Equations

• e.extendDomain f = (f.permCongr e).subtypeCongr (Equiv.refl { a : β' // ¬p a })

@[simp]

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

theorem Equiv.Perm.extendDomain_apply_subtype {α' : Type u_9} {β' : Type u_10} (e : Equiv.Perm α') {p : β' → Prop} [DecidablePred p] (f : α' ≃ Subtype p) {b : β'} (h : p b) : (e.extendDomain f) b = ↑(f (e (f.symm ⟨b, h⟩)))

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

@[simp]

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

@[simp]

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

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

def Equiv.subtypeQuotientEquivQuotientSubtype {α : Sort u_1} (p₁ : α → Prop) {s₁ : Setoid α} {s₂ : Setoid (Subtype p₁)} (p₂ : Quotient s₁ → Prop) (hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) (h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y) : { x : Quotient s₁ // 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

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

@[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₂ ⟦a⟧) (h : ∀ (x y : Subtype p₁), s₂ x y ↔ ↑x ≈ ↑y) (x : α) (hx : p₂ ⟦x⟧) : (Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h) ⟨⟦x⟧, hx⟩ = ⟦⟨x, ⋯⟩⟧

@[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₂ ⟦a⟧) (h : ∀ (x y : Subtype p₁), s₂ x y ↔ ↑x ≈ ↑y) (x : Subtype p₁) : (Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h).symm ⟦x⟧ = ⟨⟦↑x⟧, ⋯⟩

def Equiv.swapCore {α : Sort u_1} [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

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

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

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

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

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

Equations

• Equiv.swap a b = { toFun := Equiv.swapCore a b, invFun := Equiv.swapCore a b, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

theorem Equiv.eq_or_eq_of_swap_apply_ne_self {α : Sort u_1} [DecidableEq α] {a : α} {b : α} {x : α} (h : (Equiv.swap a b) x ≠ x) : x = a ∨ x = b

@[simp]

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

@[simp]

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

@[simp]

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

theorem Equiv.swap_comp_apply {α : Sort u_1} [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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Equiv.apply_swap_eq_self {α : Sort u_1} {β : Sort u_4} [DecidableEq α] {v : α → β} {i : α} {j : α} (hv : v i = v j) (k : α) : v ((Equiv.swap i j) k) = v k

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

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

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

@[simp]

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

@[simp]

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

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

Augment an equivalence with a prescribed mapping f a = b

Equations

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

@[simp]

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

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 := ⋯, right_inv := ⋯ }

@[simp]

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

@[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

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

theorem Function.Involutive.symm_eq_self_of_involutive {α : Sort u_1} (f : Equiv.Perm α) (h : Function.Involutive ⇑f) : Equiv.symm f = f

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

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

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

Transport dependent functions through an equivalence of the base space.

Equations

• Equiv.piCongrLeft' P e = { toFun := fun (f : (a : α) → P a) (x : β) => f (e.symm x), invFun := fun (f : (b : β) → P (e.symm b)) (x : α) => ⋯ ▸ f (e x), left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

theorem Equiv.piCongrLeft'_symm_apply {α : Sort u_1} {β : Sort u_4} (P : α → Sort u_9) (e : α ≃ β) (f : (b : β) → P (e.symm b)) (x : α) : (Equiv.piCongrLeft' P e).symm f x = ⋯ ▸ f (e x)

Note: the "obvious" statement (piCongrLeft' P e).symm g a = g (e a) doesn't typecheck: the LHS would have type P a while the RHS would have type P (e.symm (e a)). For that reason, we have to explicitly substitute along e.symm (e a) = a in the statement of this lemma.

@[simp]

theorem Equiv.piCongrLeft'_symm {α : Sort u_1} {β : Sort u_4} (P : Sort u_9) (e : α ≃ β) : (Equiv.piCongrLeft' (fun (x : α) => P) e).symm = Equiv.piCongrLeft' (fun (a : β) => P) e.symm

This lemma is impractical to state in the dependent case.

@[simp]

theorem Equiv.piCongrLeft'_symm_apply_apply {α : Sort u_1} {β : Sort u_4} (P : α → Sort u_9) (e : α ≃ β) (g : (b : β) → P (e.symm b)) (b : β) : (Equiv.piCongrLeft' P e).symm g (e.symm b) = g b

Note: the "obvious" statement (piCongrLeft' P e).symm g a = g (e a) doesn't typecheck: the LHS would have type P a while the RHS would have type P (e.symm (e a)). This lemma is a way around it in the case where a is of the form e.symm b, so we can use g b instead of g (e (e.symm b)).

def Equiv.piCongrLeft {α : Sort u_1} {β : Sort u_4} (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.piCongrLeft' P e.symm).symm

@[simp]

theorem Equiv.piCongrLeft_apply {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β) (f : (a : α) → P (e a)) (b : β) : (Equiv.piCongrLeft P e) f b = ⋯ ▸ f (e.symm b)

Note: the "obvious" statement (piCongrLeft P e) f b = f (e.symm b) doesn't typecheck: the LHS would have type P b while the RHS would have type P (e (e.symm b)). For that reason, we have to explicitly substitute along e (e.symm b) = b in the statement of this lemma.

@[simp]

theorem Equiv.piCongrLeft_symm_apply {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β) (g : (b : β) → P b) (a : α) : (Equiv.piCongrLeft P e).symm g a = g (e a)

theorem Equiv.piCongrLeft_apply_apply {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β) (f : (a : α) → P (e a)) (a : α) : (Equiv.piCongrLeft P e) f (e a) = f a

Note: the "obvious" statement (piCongrLeft P e) f b = f (e.symm b) doesn't typecheck: the LHS would have type P b while the RHS would have type P (e (e.symm b)). This lemma is a way around it in the case where b is of the form e a, so we can use f a instead of f (e.symm (e a)).

theorem Equiv.piCongrLeft_apply_eq_cast {α : Sort u_1} {β : Sort u_4} {P : β → Sort v} {e : α ≃ β} (f : (a : α) → P (e a)) (b : β) : (Equiv.piCongrLeft P e) f b = cast ⋯ (f (e.symm b))

theorem Equiv.piCongrLeft_sum_inl {ι : Type u_10} {ι' : Type u_11} {ι'' : Sort u_12} (π : ι'' → Type u_9) (e : ι ⊕ ι' ≃ ι'') (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (i : ι) : (Equiv.piCongrLeft π e) ((Equiv.sumPiEquivProdPi fun (x : ι ⊕ ι') => π (e x)).symm (f, g)) (e (Sum.inl i)) = f i

theorem Equiv.piCongrLeft_sum_inr {ι : Type u_10} {ι' : Type u_11} {ι'' : Sort u_12} (π : ι'' → Type u_9) (e : ι ⊕ ι' ≃ ι'') (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (j : ι') : (Equiv.piCongrLeft π e) ((Equiv.sumPiEquivProdPi fun (x : ι ⊕ ι') => π (e x)).symm (f, g)) (e (Sum.inr j)) = g j

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

theorem Equiv.semiconj_conj {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁) : Function.Semiconj (⇑e) f (e.conj f)

theorem Equiv.semiconj₂_conj {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) : Function.Semiconj₂ (⇑e) f ((e.arrowCongr e.conj) f)

instance Equiv.instAssociativeCoeForallForallArrowCongr {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [Std.Associative f] : Std.Associative ((e.arrowCongr (e.arrowCongr e)) f)

Equations

• ⋯ = ⋯

instance Equiv.instIdempotentOpCoeForallForallArrowCongr {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [Std.IdempotentOp f] : Std.IdempotentOp ((e.arrowCongr (e.arrowCongr e)) f)

Equations

• ⋯ = ⋯

@[simp]

theorem Equiv.ulift_symm_down {α : Type v} (x : α) : (Equiv.ulift.symm x).down = x

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

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

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

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

Equations

• subsingletonProdSelfEquiv = { toFun := fun (p : α × α) => p.1, invFun := fun (a : α) => (a, a), left_inv := ⋯, right_inv := ⋯ }

def equivOfSubsingletonOfSubsingleton {α : Sort u_1} {β : Sort u_4} [Subsingleton α] [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 := ⋯, right_inv := ⋯ }

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

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

Equations

• Equiv.punitOfNonemptyOfSubsingleton = equivOfSubsingletonOfSubsingleton (fun (x : α) => PUnit.unit) fun (x : PUnit.{?u.22}) => h.some

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

Unique (Unique α) is equivalent to Unique α.

Equations

• uniqueUniqueEquiv = equivOfSubsingletonOfSubsingleton (fun (h : Unique (Unique α)) => default) fun (h : Unique α) => { default := h, uniq := ⋯ }

def uniqueEquivEquivUnique (α : Sort u) (β : Sort v) [Unique β] : Unique α ≃ (α ≃ β)

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

Equations

• uniqueEquivEquivUnique α β = equivOfSubsingletonOfSubsingleton (fun (x : Unique α) => Equiv.equivOfUnique α β) Equiv.unique

theorem Function.update_comp_equiv {α : Sort u_1} {β : Sort u_4} {α' : Sort u_9} [DecidableEq α'] [DecidableEq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) : Function.update f a v ∘ ⇑g = Function.update (f ∘ ⇑g) (g.symm a) v

theorem Function.update_apply_equiv_apply {α : Sort u_1} {β : Sort u_4} {α' : Sort u_9} [DecidableEq α'] [DecidableEq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) (a' : α') : Function.update f a v (g a') = Function.update (f ∘ ⇑g) (g.symm a) v a'

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

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