Equivalence between product types

In this file we continue the work on equivalences begun in Mathlib/Logic/Equiv/Defs.lean, focussing on product types.

Main definitions

• Equiv.prodCongr ea eb : α₁ × β₁ ≃ α₂ × β₂: combine two equivalences ea : α₁ ≃ α₂ and eb : β₁ ≃ β₂ using Prod.map.

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.fst, x.snd⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

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✝.fst, a✝.snd⟩

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_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✝.fst, a✝.snd⟩

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

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 β) : pprodEquivProdPLift.symm a✝ = (Equiv.plift.symm.pprodCongr Equiv.plift.symm).symm ⟨a✝.fst, a✝.snd⟩

@[simp]

theorem Equiv.pprodEquivProdPLift_apply {α : Sort u_1} {β : Sort u_4} (a✝ : α ×' β) : 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) : ⇑(prodComm α β) = Prod.swap

@[simp]

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

@[simp]

theorem Equiv.prodComm_symm (α : Type u_9) (β : Type u_10) : (prodComm α β).symm = 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.fst.fst, p.fst.snd, p.snd), invFun := fun (p : α × β × γ) => ((p.fst, p.snd.fst), p.snd.snd), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.prodAssoc_apply (α : Type u_9) (β : Type u_10) (γ : Type u_11) (p : (α × β) × γ) : (prodAssoc α β γ) p = (p.fst.fst, p.fst.snd, p.snd)

@[simp]

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

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 : (α × β) × γ × δ) : (prodProdProdComm α β γ δ) abcd = ((abcd.fst.fst, abcd.snd.fst), abcd.fst.snd, abcd.snd.snd)

@[simp]

theorem Equiv.prodProdProdComm_symm (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) : (prodProdProdComm α β γ δ).symm = 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) : ⇑(curry α β γ) = Function.curry

@[simp]

theorem Equiv.curry_symm_apply (α : Type u_9) (β : Type u_10) (γ : Sort u_11) : ⇑(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.9 + 1}) => p.fst, invFun := fun (a : α) => (a, PUnit.unit), left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

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.7 + 1} α) (Equiv.prodPUnit α)

@[simp]

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

@[simp]

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

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.11 + 1}) => p.fst, invFun := fun (a : α) => ⟨a, PUnit.unit⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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 β] : ⇑(prodUnique α β) = Prod.fst

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

@[simp]

theorem Equiv.prodUnique_symm_apply {α : Type u_9} {β : Type u_10} [Unique β] (x : α) : (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 β] : ⇑(uniqueProd α β) = Prod.snd

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

@[simp]

theorem Equiv.uniqueProd_symm_apply {α : Type u_9} {β : Type u_10} [Unique β] (x : α) : (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)] : ⇑(sigmaUnique α β) = Sigma.fst

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

@[simp]

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

def Equiv.uniqueSigma {α : Type u_10} (β : α → Type u_9) [Unique α] : (i : α) × β i ≃ β default

Any Unique type is a left identity for type sigma up to equivalence. Compare with uniqueProd which is non-dependent.

Equations

• Equiv.uniqueSigma β = { toFun := fun (p : (i : α) × β i) => ⋯ ▸ p.snd, invFun := fun (b : β default) => ⟨default, b⟩, left_inv := ⋯, right_inv := ⋯ }

theorem Equiv.uniqueSigma_apply {α : Type u_10} {β : α → Type u_9} [Unique α] (x : (a : α) × β a) : (uniqueSigma β) x = ⋯ ▸ x.snd

@[simp]

theorem Equiv.uniqueSigma_symm_apply {α : Type u_10} {β : α → Type u_9} [Unique α] (y : β default) : (uniqueSigma β).symm y = ⟨default, y⟩

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.8 + 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.8 + 1} × α)

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.snd) ab.fst, ab.snd), invFun := fun (ab : β₂ × α₁) => ((e ab.snd).symm ab.fst, ab.snd), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.prodCongrLeft_apply {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (b : β₁) (a : α₁) : (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 α₁) = 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.fst, (e ab.fst) ab.snd), invFun := fun (ab : α₁ × β₂) => (ab.fst, (e ab.fst).symm ab.snd), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.prodCongrRight_apply {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (a : α₁) (b : β₁) : (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 = prodCongrRight fun (x : α₁) => e

@[simp]

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

@[simp]

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

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

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

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.fst, (e₂ x.fst) x.snd), invFun := fun (y : α₂ × β₂) => (e₁.symm y.fst, (e₂ (e₁.symm y.fst)).symm y.snd), 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.fst, (e₂ (e₁.symm y.fst)).symm y.snd)

@[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.fst, (e₂ x.fst) x.snd)

def Equiv.Perm.prodExtendRight {α₁ : Type u_9} {β₁ : Type u_10} [DecidableEq α₁] (a : α₁) (e : Perm β₁) : 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 : Perm β₁) (b : β₁) : (prodExtendRight a e) (a, b) = (a, e b)

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

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

@[simp]

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

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

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.

@[simp]

theorem Equiv.arrowProdEquivProdArrow_symm_apply (α : Type u_9) (β : α → Type u_10) (γ : α → Type u_11) (p : ((i : α) → β i) × ((i : α) → γ i)) (c : α) : (arrowProdEquivProdArrow α β γ).symm p c = (p.fst c, p.snd c)

@[simp]

theorem Equiv.arrowProdEquivProdArrow_apply (α : Type u_9) (β : α → Type u_10) (γ : α → Type u_11) (f : (i : α) → β i × γ i) : (arrowProdEquivProdArrow α β γ) f = (fun (c : α) => (f c).fst, fun (c : α) => (f c).snd)

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) : (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 : ι ⊕ ι') : (sumPiEquivProdPi π).symm g t = Sum.rec g.fst g.snd 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) : (prodPiEquivSumPi π π').symm a✝ = (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 : ι ⊕ ι') : (prodPiEquivSumPi π π') a✝ i = (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.fst p.snd, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem Equiv.sumArrowEquivProdArrow_symm_apply_inl {α : Type u_9} {β : Type u_10} {γ : Type u_11} (f : α → γ) (g : β → γ) (a : α) : (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 : β) : (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 : γ) : (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 : γ) : (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 : α × γ) : (sumProdDistrib α β γ).symm (Sum.inl a) = (Sum.inl a.fst, a.snd)

@[simp]

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

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) × β) : (sigmaProdDistrib α β) p = ⟨p.fst.fst, (p.fst.snd, p.snd)⟩

@[simp]

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

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

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

Equations

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

@[simp]

theorem Equiv.boolProdEquivSum_apply (α : Type u_9) (p : Bool × α) : (boolProdEquivSum α) p = if p.fst = true then Sum.inr p.snd else Sum.inl p.snd

@[simp]

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

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) => if b = true then p.snd else p.fst, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

theorem Equiv.boolArrowEquivProd_symm_apply (α : Type u_9) (p : α × α) (b : Bool) : (boolArrowEquivProd α).symm p b = if b = true then p.snd else p.fst

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

def Equiv.prodSubtypeFstEquivSubtypeProd {α : Type u_9} {β : Type u_10} {p : α → Prop} : { s : α × β // p s.fst } ≃ { 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.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.

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_symm_apply {α : Type u_9} (p : α → Prop) (β : α → Type u_10) [DecidablePred p] (f : ((i : { x : α // p x }) → β ↑i) × ((i : { x : α // ¬p x }) → β ↑i)) (x : α) : (piEquivPiSubtypeProd p β).symm f x = if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩

@[simp]

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

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_apply {α : Type u_9} [DecidableEq α] (i : α) (β : α → Type u_10) (f : (j : α) → β j) : (piSplitAt i β) f = (f i, fun (j : { j : α // j ≠ i }) => f ↑j)

@[simp]

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

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) : (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 : α) : (funSplitAt i β).symm f j = if h : j = i then f.fst else f.snd ⟨j, ⋯⟩

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

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

Equations

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