Documentation

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

α ×' β ≃ α × β

PProd α β is equivalent to α × β

Instances For

@[simp]

theorem Equiv.pprodEquivProd_apply {α : Type u_9} {β : Type u_10} (x : α ×' β) :

pprodEquivProd x = (x.fst, x.snd)

@[simp]

theorem Equiv.pprodEquivProd_symm_apply {α : Type u_9} {β : Type u_10} (x : α × β) :

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 β δ.

Instances For

@[simp]

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

(e₁.pprodCongr e₂).symm x = ⟨e₁.symm x.fst, e₂.symm x.snd⟩

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

Instances For

@[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.symm a✝.1, eb.symm a✝.2⟩

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

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.

Instances For

@[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 a✝.1, eb a✝.2⟩

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

Instances For

@[simp]

theorem Equiv.pprodEquivProdPLift_apply {α : Sort u_1} {β : Sort u_4} (a✝ : α ×' β) :

pprodEquivProdPLift a✝ = ({ down := a✝.fst }, { down := a✝.snd })

@[simp]

theorem Equiv.pprodEquivProdPLift_symm_apply {α : Sort u_1} {β : Sort u_4} (a✝ : PLift α × PLift β) :

pprodEquivProdPLift.symm a✝ = ⟨a✝.1.down, a✝.2.down⟩

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.

Instances For

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

Instances For

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

Instances For

@[simp]

theorem Equiv.prodAssoc_apply (α : Type u_9) (β : Type u_10) (γ : Type u_11) (p : (α × β) × γ) :

(prodAssoc α β γ) p = (p.1.1, p.1.2, p.2)

@[simp]

theorem Equiv.prodAssoc_symm_apply (α : Type u_9) (β : Type u_10) (γ : Type u_11) (p : α × β × γ) :

(prodAssoc α β γ).symm p = ((p.1, p.2.1), p.2.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.

Instances For

@[simp]

theorem Equiv.prodProdProdComm_apply (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) (abcd : (α × β) × γ × δ) :

(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) :

(prodProdProdComm α β γ δ).symm = prodProdProdComm α γ β δ

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

(α × β → γ) ≃ (α → β → γ)

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

Instances For

@[simp]

theorem Equiv.curry_symm_apply (α : Type u_9) (β : Type u_10) (γ : Sort u_11) :

⇑(curry α β γ).symm = Function.uncurry

@[simp]

theorem Equiv.curry_apply (α : Type u_9) (β : Type u_10) (γ : Sort u_11) :

⇑(curry α β γ) = Function.curry

def Equiv.prodPUnit (α : Type u_9) :

α × PUnit.{u_10 + 1} ≃ α

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

Instances For

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

def Equiv.punitProd (α : Type u_9) :

PUnit.{u_10 + 1} × α ≃ α

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

Instances For

@[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✝.2

def Equiv.sigmaPUnit (α : Type u_9) :

(_ : α) × PUnit.{u_10 + 1} ≃ α

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

Instances For

@[simp]

theorem Equiv.sigmaPUnit_symm_apply_fst (α : Type u_9) (a : α) :

((sigmaPUnit α).symm a).fst = a

@[simp]

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

(sigmaPUnit α) p = p.fst

@[simp]

theorem Equiv.sigmaPUnit_symm_apply_snd (α : Type u_9) (a : α) :

((sigmaPUnit α).symm a).snd = PUnit.unit

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

α × β ≃ α

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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.

Instances For

def Equiv.emptyProd (α : Type u_9) :

Empty × α ≃ Empty

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

Instances For

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.

Instances For

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.

Instances For

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

β₁ × α₁ ≃ β₂ × α₁

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

Instances For

@[simp]

theorem Equiv.prodCongrLeft_apply_fst {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (ab : β₁ × α₁) :

((prodCongrLeft e) ab).1 = (e ab.2) ab.1

@[simp]

theorem Equiv.prodCongrLeft_apply_snd {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (ab : β₁ × α₁) :

((prodCongrLeft e) ab).2 = ab.2

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

@[simp]

theorem Equiv.prodCongrLeft_symm {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) :

(prodCongrLeft e).symm = prodCongrLeft (Equiv.symm ∘ e)

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

α₁ × β₁ ≃ α₁ × β₂

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

Instances For

@[simp]

theorem Equiv.prodCongrRight_apply_snd {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (ab : α₁ × β₁) :

((prodCongrRight e) ab).2 = (e ab.1) ab.2

@[simp]

theorem Equiv.prodCongrRight_apply_fst {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (ab : α₁ × β₁) :

((prodCongrRight e) ab).1 = ab.1

@[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.prodCongrRight_symm {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) :

(prodCongrRight e).symm = prodCongrRight (Equiv.symm ∘ 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.

Instances For

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

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

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.

Instances For

@[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).1 = ab.1

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 β → γ.

Instances For

@[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.1 c, p.2 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).1, fun (c : α) => (f c).2)

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.

Instances For

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

Instances For

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

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

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 β.

Instances For

@[simp]

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

((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 : β) :

((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 : α) :

(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.

Instances For

@[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.1, a.2)

@[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.1, b.2)

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

Instances For

@[simp]

theorem Equiv.sigmaProdDistrib_apply {ι : Type u_9} (α : ι → Type u_10) (β : Type u_11) (p : ((i : ι) × α i) × β) :

(sigmaProdDistrib α β) p = ⟨p.1.fst, (p.1.snd, p.2)⟩

@[simp]

theorem Equiv.sigmaProdDistrib_symm_apply {ι : Type u_9} (α : ι → Type u_10) (β : Type u_11) (p : (i : ι) × α i × β) :

(sigmaProdDistrib α β).symm p = (⟨p.fst, p.snd.1⟩, p.snd.2)

def Equiv.boolProdEquivSum (α : Type u_9) :

Bool × α ≃ α ⊕ α

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

Instances For

@[simp]

theorem Equiv.boolProdEquivSum_apply (α : Type u_9) (p : Bool × α) :

(boolProdEquivSum α) p = if p.1 = true then Sum.inr p.2 else Sum.inl p.2

@[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 α × α.

Instances For

@[simp]

theorem Equiv.boolArrowEquivProd_symm_apply (α : Type u_9) (p : α × α) (b : Bool) :

(boolArrowEquivProd α).symm p b = if b = true then p.2 else p.1

@[simp]

theorem Equiv.boolArrowEquivProd_apply (α : Type u_9) (f : Bool → α) :

(boolArrowEquivProd α) f = (f false, f true)

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

@[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.1 ⟨x, h⟩ else f.2 ⟨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.

Instances For

@[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.1 else f.2 ⟨j, h⟩

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

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.

Instances For