doc-next-gen

Mathlib.Logic.Equiv.Prod

Module docstring

{"# 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 "}

Equiv.pprodEquivProd definition
{α β} : PProd α β ≃ α × β
Full source 
/-- `PProd α β` is equivalent to `α × β` -/
@[simps apply symm_apply]
def pprodEquivProd {α β} : PProdPProd α β ≃ α × β where
  toFun x := (x.1, x.2)
  invFun x := ⟨x.1, x.2⟩
  left_inv := fun _ => rfl
  right_inv := fun _ => rfl
Equivalence between `PProd` and Cartesian product
Informal description
The equivalence between the product types `PProd α β` and `α × β` is given by the bijection that maps a pair `⟨a, b⟩` in `PProd α β` to the pair `(a, b)` in `α × β`, and vice versa. This bijection preserves the components of the pairs in both directions.
Equiv.pprodCongr definition
(e₁ : α ≃ β) (e₂ : γ ≃ δ) : PProd α γ ≃ PProd β δ
Full source 
/-- Product of two equivalences, in terms of `PProd`. If `α ≃ β` and `γ ≃ δ`, then
`PProd α γ ≃ PProd β δ`. -/
@[simps apply]
def pprodCongr (e₁ : α ≃ β) (e₂ : γ ≃ δ) : PProdPProd α γ ≃ PProd β δ where
  toFun x := ⟨e₁ x.1, e₂ x.2⟩
  invFun x := ⟨e₁.symm x.1, e₂.symm x.2⟩
  left_inv := fun ⟨x, y⟩ => by simp
  right_inv := fun ⟨x, y⟩ => by simp
Equivalence of product types via component-wise equivalences
Informal description
Given equivalences $e_1 : \alpha \simeq \beta$ and $e_2 : \gamma \simeq \delta$, the function maps a pair $\langle x, y \rangle$ in the product type $\text{PProd} \alpha \gamma$ to the pair $\langle e_1 x, e_2 y \rangle$ in $\text{PProd} \beta \delta$, and its inverse maps $\langle u, v \rangle$ back to $\langle e_1^{-1} u, e_2^{-1} v \rangle$. This defines a bijection between $\text{PProd} \alpha \gamma$ and $\text{PProd} \beta \delta$.
Equiv.pprodProd definition
{α₂ β₂} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : PProd α₁ β₁ ≃ α₂ × β₂
Full source 
/-- Combine two equivalences using `PProd` in the domain and `Prod` in the codomain. -/
@[simps! apply symm_apply]
def pprodProd {α₂ β₂} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) :
    PProdPProd α₁ β₁ ≃ α₂ × β₂ :=
  (ea.pprodCongr eb).trans pprodEquivProd
Equivalence between `PProd` and Cartesian product via component-wise equivalences
Informal description
Given equivalences $e_a : \alpha_1 \simeq \alpha_2$ and $e_b : \beta_1 \simeq \beta_2$, the function maps a pair $\langle x, y \rangle$ in the product type $\text{PProd} \alpha_1 \beta_1$ to the pair $(e_a x, e_b y)$ in $\alpha_2 \times \beta_2$, and its inverse maps $(u, v)$ back to $\langle e_a^{-1} u, e_b^{-1} v \rangle$. This defines a bijection between $\text{PProd} \alpha_1 \beta_1$ and $\alpha_2 \times \beta_2$ by first applying the component-wise equivalences and then converting the product type.
Equiv.prodPProd definition
{α₁ β₁} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ × β₁ ≃ PProd α₂ β₂
Full source 
/-- Combine two equivalences using `PProd` in the codomain and `Prod` in the domain. -/
@[simps! apply symm_apply]
def prodPProd {α₁ β₁} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) :
    α₁ × β₁α₁ × β₁ ≃ PProd α₂ β₂ :=
  (ea.symm.pprodProd eb.symm).symm
Equivalence between Cartesian product and `PProd` via component-wise equivalences
Informal description
Given equivalences $e_a : \alpha_1 \simeq \alpha_2$ and $e_b : \beta_1 \simeq \beta_2$, the function maps a pair $(x, y)$ in the product type $\alpha_1 \times \beta_1$ to the pair $\langle e_a x, e_b y \rangle$ in the product type $\text{PProd} \alpha_2 \beta_2$, and its inverse maps $\langle u, v \rangle$ back to $(e_a^{-1} u, e_b^{-1} v)$. This defines a bijection between $\alpha_1 \times \beta_1$ and $\text{PProd} \alpha_2 \beta_2$ by first applying the component-wise equivalences and then converting the product type.
Equiv.pprodEquivProdPLift definition
: PProd α β ≃ PLift α × PLift β
Full source 
/-- `PProd α β` is equivalent to `PLift α × PLift β` -/
@[simps! apply symm_apply]
def pprodEquivProdPLift : PProdPProd α β ≃ PLift α × PLift β :=
  Equiv.plift.symm.pprodProd Equiv.plift.symm
Equivalence between `PProd` and lifted product types
Informal description
The equivalence between the product type `PProd α β` and the Cartesian product `PLift α × PLift β`, where `PLift` is a wrapper type that lifts its argument to a higher universe. This equivalence is constructed by applying the inverse of the `plift` equivalence to each component of the product.
Equiv.prodCongr definition
{α₁ α₂ β₁ β₂} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂
Full source 
/-- Product of two equivalences. If `α₁ ≃ α₂` and `β₁ ≃ β₂`, then `α₁ × β₁ ≃ α₂ × β₂`. This is
`Prod.map` as an equivalence. -/
@[simps -fullyApplied apply]
def prodCongr {α₁ α₂ β₁ β₂} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : α₁ × β₁α₁ × β₁ ≃ α₂ × β₂ :=
  ⟨Prod.map e₁ e₂, Prod.map e₁.symm e₂.symm, fun ⟨a, b⟩ => by simp, fun ⟨a, b⟩ => by simp⟩
Product type equivalence via component-wise equivalences
Informal description
Given equivalences (bijections with inverses) $e₁ : α₁ ≃ α₂$ and $e₂ : β₁ ≃ β₂$, the function `Equiv.prodCongr` constructs an equivalence between the product types $α₁ × β₁$ and $α₂ × β₂$ by applying $e₁$ to the first component and $e₂$ to the second component of each pair. The inverse is constructed similarly by applying the inverses of $e₁$ and $e₂$.
Equiv.prodCongr_symm theorem
{α₁ α₂ β₁ β₂} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (prodCongr e₁ e₂).symm = prodCongr e₁.symm e₂.symm
Full source 
@[simp]
theorem prodCongr_symm {α₁ α₂ β₁ β₂} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
    (prodCongr e₁ e₂).symm = prodCongr e₁.symm e₂.symm :=
  rfl
Inverse of Product Equivalence is Component-wise Inverses
Informal description
Given equivalences (bijections with inverses) $e₁ : α₁ ≃ α₂$ and $e₂ : β₁ ≃ β₂$, the inverse of the product equivalence $\text{prodCongr}(e₁, e₂) : α₁ × β₁ ≃ α₂ × β₂$ is equal to the product equivalence formed by the inverses of $e₁$ and $e₂$, i.e., $(\text{prodCongr}(e₁, e₂))^{-1} = \text{prodCongr}(e₁^{-1}, e₂^{-1})$.
Equiv.prodComm definition
(α β) : α × β ≃ β × α
Full source 
/-- Type product is commutative up to an equivalence: `α × β ≃ β × α`. This is `Prod.swap` as an
equivalence. -/
def prodComm (α β) : α × βα × β ≃ β × α :=
  ⟨Prod.swap, Prod.swap, Prod.swap_swap, Prod.swap_swap⟩
Commutativity of product types via swapping
Informal description
The equivalence between the product types $\alpha \times \beta$ and $\beta \times \alpha$ is given by the swap function, which exchanges the two components of a pair. This is a bijection with itself as its own inverse.
Equiv.coe_prodComm theorem
(α β) : (⇑(prodComm α β) : α × β → β × α) = Prod.swap
Full source 
@[simp]
theorem coe_prodComm (α β) : (⇑(prodComm α β) : α × β → β × α) = Prod.swap :=
  rfl
Equivalence Between Product Types is Component Swapping
Informal description
For any types $\alpha$ and $\beta$, the underlying function of the equivalence $\alpha \times \beta \simeq \beta \times \alpha$ is equal to the swap function $\text{Prod.swap} : \alpha \times \beta \to \beta \times \alpha$ that exchanges the components of a pair.
Equiv.prodComm_apply theorem
{α β} (x : α × β) : prodComm α β x = x.swap
Full source 
@[simp]
theorem prodComm_apply {α β} (x : α × β) : prodComm α β x = x.swap :=
  rfl
Application of Product Commutativity Equivalence is Pair Swapping
Informal description
For any pair $x = (a, b)$ in the product type $\alpha \times \beta$, the application of the equivalence `prodComm α β` to $x$ yields the swapped pair $(b, a)$, i.e., $\text{prodComm}_{\alpha,\beta}(a, b) = (b, a)$.
Equiv.prodComm_symm theorem
(α β) : (prodComm α β).symm = prodComm β α
Full source 
@[simp]
theorem prodComm_symm (α β) : (prodComm α β).symm = prodComm β α :=
  rfl
Inverse of Product Commutativity Equivalence is Commutativity in Reverse Order
Informal description
For any types $\alpha$ and $\beta$, the inverse of the equivalence $\alpha \times \beta \simeq \beta \times \alpha$ (given by swapping components) is equal to the equivalence $\beta \times \alpha \simeq \alpha \times \beta$ (also given by swapping components).
Equiv.prodAssoc definition
(α β γ) : (α × β) × γ ≃ α × β × γ
Full source 
/-- Type product is associative up to an equivalence. -/
@[simps]
def prodAssoc (α β γ) : (α × β) × γ(α × β) × γ ≃ α × β × γ :=
  ⟨fun p => (p.1.1, p.1.2, p.2), fun p => ((p.1, p.2.1), p.2.2), fun ⟨⟨_, _⟩, _⟩ => rfl,
    fun ⟨_, ⟨_, _⟩⟩ => rfl⟩
Associativity equivalence for product types
Informal description
The equivalence $(α × β) × γ ≃ α × (β × γ)$ is defined by the bijection that reassociates the components of the product as follows: for any $((a, b), c)$ in $(α × β) × γ$, the corresponding element in $α × (β × γ)$ is $(a, (b, c))$. The inverse function similarly reassociates $(a, (b, c))$ back to $((a, b), c)$.
Equiv.prodProdProdComm definition
(α β γ δ) : (α × β) × γ × δ ≃ (α × γ) × β × δ
Full source 
/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
@[simps apply]
def prodProdProdComm (α β γ δ) : (α × β) × γ × δ(α × β) × γ × δ ≃ (α × γ) × β × δ where
  toFun abcd := ((abcd.1.1, abcd.2.1), (abcd.1.2, abcd.2.2))
  invFun acbd := ((acbd.1.1, acbd.2.1), (acbd.1.2, acbd.2.2))
  left_inv := fun ⟨⟨_a, _b⟩, ⟨_c, _d⟩⟩ => rfl
  right_inv := fun ⟨⟨_a, _c⟩, ⟨_b, _d⟩⟩ => rfl
Rearrangement equivalence for quadruple products
Informal description
The equivalence $(α × β) × γ × δ ≃ (α × γ) × β × δ$ is defined by the bijection that rearranges the components of the quadruple product as follows: for any $((a, b), (c, d))$ in $(α × β) × γ × δ$, the corresponding element in $(α × γ) × β × δ$ is $((a, c), (b, d))$. The inverse function similarly rearranges $((a, c), (b, d))$ back to $((a, b), (c, d))$.
Equiv.prodProdProdComm_symm theorem
(α β γ δ) : (prodProdProdComm α β γ δ).symm = prodProdProdComm α γ β δ
Full source 
@[simp]
theorem prodProdProdComm_symm (α β γ δ) :
    (prodProdProdComm α β γ δ).symm = prodProdProdComm α γ β δ :=
  rfl
Inverse of Product Rearrangement Equivalence
Informal description
For any types $\alpha, \beta, \gamma, \delta$, the inverse of the equivalence $(α × β) × (γ × δ) ≃ (α × γ) × (β × δ)$ is equal to the equivalence $(α × γ) × (β × δ) ≃ (α × β) × (γ × δ)$.
Equiv.curry definition
(α β γ) : (α × β → γ) ≃ (α → β → γ)
Full source 
/-- `γ`-valued functions on `α × β` are equivalent to functions `α → β → γ`. -/
@[simps -fullyApplied]
def curry (α β γ) : (α × β → γ) ≃ (α → β → γ) where
  toFun := Function.curry
  invFun := uncurry
  left_inv := uncurry_curry
  right_inv := curry_uncurry
Currying equivalence for functions on product types
Informal description
The equivalence between the type of functions from the product type $\alpha \times \beta$ to $\gamma$ and the type of curried functions $\alpha \to \beta \to \gamma$. This is established by the bijection that converts a function $f : \alpha \times \beta \to \gamma$ to its curried form $\lambda a \, b, f (a, b)$ and vice versa via uncurrying.
Equiv.prodPUnit definition
(α) : α × PUnit ≃ α
Full source 
/-- `PUnit` is a right identity for type product up to an equivalence. -/
@[simps]
def prodPUnit (α) : α × PUnitα × PUnit ≃ α :=
  ⟨fun p => p.1, fun a => (a, PUnit.unit), fun ⟨_, PUnit.unit⟩ => rfl, fun _ => rfl⟩
Equivalence between product with unit and base type
Informal description
The equivalence between the product type $\alpha \times \text{PUnit}$ and $\alpha$, where $\text{PUnit}$ is the unit type with a single element. The equivalence maps each pair $(a, ())$ to its first component $a$, and inversely maps each element $a$ of $\alpha$ to the pair $(a, ())$.
Equiv.punitProd definition
(α) : PUnit × α ≃ α
Full source 
/-- `PUnit` is a left identity for type product up to an equivalence. -/
@[simps!]
def punitProd (α) : PUnitPUnit × αPUnit × α ≃ α :=
  calc
    PUnit × α ≃ α × PUnit := prodComm _ _
    _ ≃ α := prodPUnit _
Equivalence between product with unit on the left and base type
Informal description
The equivalence between the product type $\text{PUnit} \times \alpha$ and $\alpha$, where $\text{PUnit}$ is the unit type with a single element. The equivalence maps each pair $((), a)$ to its second component $a$, and inversely maps each element $a$ of $\alpha$ to the pair $((), a)$.
Equiv.sigmaPUnit definition
(α) : (_ : α) × PUnit ≃ α
Full source 
/-- `PUnit` is a right identity for dependent type product up to an equivalence. -/
@[simps]
def sigmaPUnit (α) : (_ : α) × PUnit(_ : α) × PUnit ≃ α :=
  ⟨fun p => p.1, fun a => ⟨a, PUnit.unit⟩, fun ⟨_, PUnit.unit⟩ => rfl, fun _ => rfl⟩
Equivalence between dependent product with unit and base type
Informal description
The equivalence between the dependent product type `Σ (a : α), PUnit` and the type `α`, where `PUnit` is the unit type with a single element. The equivalence maps each pair `(a, ())` to its first component `a`, and inversely maps each element `a` of `α` to the pair `(a, ())`.
Equiv.prodUnique definition
(α β) [Unique β] : α × β ≃ α
Full source 
/-- Any `Unique` type is a right identity for type product up to equivalence. -/
def prodUnique (α β) [Unique β] : α × βα × β ≃ α :=
  ((Equiv.refl α).prodCongr <| equivPUnit.{_,1} β).trans <| prodPUnit α
Equivalence between product with unique type and base type
Informal description
For any type $\alpha$ and a type $\beta$ with a unique element, there is an equivalence between the product type $\alpha \times \beta$ and $\alpha$. This equivalence maps each pair $(a, b)$ to its first component $a$, and inversely maps each element $a$ of $\alpha$ to the pair $(a, b_0)$, where $b_0$ is the unique element of $\beta$.
Equiv.coe_prodUnique theorem
{α β} [Unique β] : (⇑(prodUnique α β) : α × β → α) = Prod.fst
Full source 
@[simp]
theorem coe_prodUnique {α β} [Unique β] : (⇑(prodUnique α β) : α × β → α) = Prod.fst :=
  rfl
Canonical Function of Product-Unique Equivalence Equals First Projection
Informal description
For any type $\alpha$ and a type $\beta$ with a unique element, the canonical function associated with the equivalence $\alpha \times \beta \simeq \alpha$ is equal to the first projection function $\mathrm{fst} : \alpha \times \beta \to \alpha$.
Equiv.prodUnique_apply theorem
{α β} [Unique β] (x : α × β) : prodUnique α β x = x.1
Full source 
theorem prodUnique_apply {α β} [Unique β] (x : α × β) : prodUnique α β x = x.1 :=
  rfl
First Projection via Product with Unique Type Equivalence
Informal description
For any type $\alpha$ and a type $\beta$ with a unique element, the equivalence `prodUnique α β` maps a pair $(a, b) \in \alpha \times \beta$ to its first component $a$.
Equiv.prodUnique_symm_apply theorem
{α β} [Unique β] (x : α) : (prodUnique α β).symm x = (x, default)
Full source 
@[simp]
theorem prodUnique_symm_apply {α β} [Unique β] (x : α) : (prodUnique α β).symm x = (x, default) :=
  rfl
Inverse of Product-Unique Equivalence Maps to Pair with Default Element
Informal description
For any type $\alpha$ and a type $\beta$ with a unique element, the inverse of the equivalence $\alpha \times \beta \simeq \alpha$ maps an element $x \in \alpha$ to the pair $(x, b_0)$, where $b_0$ is the unique element of $\beta$.
Equiv.uniqueProd definition
(α β) [Unique β] : β × α ≃ α
Full source 
/-- Any `Unique` type is a left identity for type product up to equivalence. -/
def uniqueProd (α β) [Unique β] : β × αβ × α ≃ α :=
  ((equivPUnit.{_,1} β).prodCongr <| Equiv.refl α).trans <| punitProd α
Equivalence between product with unique type and base type
Informal description
For any type $\alpha$ and a type $\beta$ with a unique element, there exists an equivalence between the product type $\beta \times \alpha$ and $\alpha$. This equivalence is constructed by first establishing a bijection between $\beta$ and the singleton type `PUnit` (using `equivPUnit`), then taking the product with $\alpha$ (using `prodCongr` with the identity equivalence on $\alpha$), and finally composing with the equivalence between `PUnit × α` and $\alpha$ (using `punitProd`). The resulting equivalence maps any pair $(b, a)$ to $a$, and its inverse maps any $a \in \alpha$ to $(b_0, a)$ where $b_0$ is the unique element of $\beta$.
Equiv.coe_uniqueProd theorem
{α β} [Unique β] : (⇑(uniqueProd α β) : β × α → α) = Prod.snd
Full source 
@[simp]
theorem coe_uniqueProd {α β} [Unique β] : (⇑(uniqueProd α β) : β × α → α) = Prod.snd :=
  rfl
Equivalence Function for Product with Unique Type Equals Second Projection
Informal description
For any types $\alpha$ and $\beta$ where $\beta$ has a unique element, the function associated with the equivalence $\beta \times \alpha \simeq \alpha$ is equal to the second projection function $\operatorname{snd} : \beta \times \alpha \to \alpha$.
Equiv.uniqueProd_apply theorem
{α β} [Unique β] (x : β × α) : uniqueProd α β x = x.2
Full source 
theorem uniqueProd_apply {α β} [Unique β] (x : β × α) : uniqueProd α β x = x.2 :=
  rfl
Application of Product Equivalence with Unique Type: $(b, a) \mapsto a$
Informal description
For any types $\alpha$ and $\beta$ where $\beta$ has a unique element, the equivalence `uniqueProd α β` maps a pair $(b, a) \in \beta \times \alpha$ to its second component $a$.
Equiv.uniqueProd_symm_apply theorem
{α β} [Unique β] (x : α) : (uniqueProd α β).symm x = (default, x)
Full source 
@[simp]
theorem uniqueProd_symm_apply {α β} [Unique β] (x : α) :
    (uniqueProd α β).symm x = (default, x) :=
  rfl
Inverse of Product Equivalence with Unique Type Maps to Default Pair
Informal description
For any type $\alpha$ and a type $\beta$ with a unique element, the inverse of the equivalence `uniqueProd α β` maps an element $x \in \alpha$ to the pair $(b_0, x)$, where $b_0$ is the unique element of $\beta$. In other words, $(\text{uniqueProd}\ \alpha\ \beta)^{-1}(x) = (\text{default}, x)$.
Equiv.sigmaUnique definition
(α) (β : α → Type*) [∀ a, Unique (β a)] : (a : α) × (β a) ≃ α
Full source 
/-- Any family of `Unique` types is a right identity for dependent type product up to
equivalence. -/
def sigmaUnique (α) (β : α → Type*) [∀ a, Unique (β a)] : (a : α) × (β a)(a : α) × (β a) ≃ α :=
  (Equiv.sigmaCongrRight fun a ↦ equivPUnit.{_,1} (β a)).trans <| sigmaPUnit α
Equivalence between dependent product with unique fibers and base type
Informal description
For any type $\alpha$ and a family of types $\beta : \alpha \to \text{Type}^*$ where each $\beta a$ has a unique element, there is an equivalence between the dependent product type $\Sigma (a : \alpha), \beta a$ and $\alpha$. This equivalence is constructed by first applying a component-wise equivalence to replace each $\beta a$ with the unit type, and then using the equivalence between $\Sigma (a : \alpha), \text{PUnit}$ and $\alpha$.
Equiv.coe_sigmaUnique theorem
{α} {β : α → Type*} [∀ a, Unique (β a)] : (⇑(sigmaUnique α β) : (a : α) × (β a) → α) = Sigma.fst
Full source 
@[simp]
theorem coe_sigmaUnique {α} {β : α → Type*} [∀ a, Unique (β a)] :
    (⇑(sigmaUnique α β) : (a : α) × (β a) → α) = Sigma.fst :=
  rfl
Equivalence Function for Unique-Fibered Sigma Type Coincides with First Projection
Informal description
For any type $\alpha$ and a family of types $\beta : \alpha \to \text{Type}^*$ where each $\beta a$ has a unique element, the underlying function of the equivalence `sigmaUnique α β` is equal to the first projection function $\Sigma.fst : \Sigma (a : \alpha), \beta a \to \alpha$.
Equiv.sigmaUnique_apply theorem
{α} {β : α → Type*} [∀ a, Unique (β a)] (x : (a : α) × β a) : sigmaUnique α β x = x.1
Full source 
theorem sigmaUnique_apply {α} {β : α → Type*} [∀ a, Unique (β a)] (x : (a : α) × β a) :
    sigmaUnique α β x = x.1 :=
  rfl
First Projection of Dependent Product with Unique Fibers
Informal description
For any type $\alpha$ and a family of types $\beta : \alpha \to \text{Type}$ where each $\beta a$ has a unique element, the equivalence $\text{sigmaUnique} \alpha \beta$ maps a pair $(a, b) \in \Sigma (a : \alpha), \beta a$ to its first component $a$.
Equiv.sigmaUnique_symm_apply theorem
{α} {β : α → Type*} [∀ a, Unique (β a)] (x : α) : (sigmaUnique α β).symm x = ⟨x, default⟩
Full source 
@[simp]
theorem sigmaUnique_symm_apply {α} {β : α → Type*} [∀ a, Unique (β a)] (x : α) :
    (sigmaUnique α β).symm x = ⟨x, default⟩ :=
  rfl
Inverse of Sigma-Unique Equivalence Maps to Canonical Pair
Informal description
For any type $\alpha$ and a family of types $\beta : \alpha \to \text{Type}^*$ where each $\beta a$ has a unique element, the inverse of the equivalence `sigmaUnique α β` maps an element $x : \alpha$ to the pair $\langle x, \text{default} \rangle$, where $\text{default}$ is the unique element of $\beta x$.
Equiv.uniqueSigma definition
{α} (β : α → Type*) [Unique α] : (i : α) × β i ≃ β default
Full source 
/-- Any `Unique` type is a left identity for type sigma up to equivalence. Compare with `uniqueProd`
which is non-dependent. -/
def uniqueSigma {α} (β : α → Type*) [Unique α] : (i:α) × β i(i:α) × β i ≃ β default :=
  ⟨fun p ↦ (Unique.eq_default _).rec p.2,
   fun b ↦ ⟨default, b⟩,
   fun _ ↦ Sigma.ext (Unique.default_eq _) (eqRec_heq _ _),
   fun _ ↦ rfl⟩
Equivalence between dependent product and fiber at default element
Informal description
For any type $\alpha$ with a unique element and any family of types $\beta : \alpha \to \text{Type}^*$, the dependent product type $(i : \alpha) \times \beta i$ is equivalent to $\beta$ evaluated at the default element of $\alpha$. The equivalence is given by: - The forward map sends a pair $\langle a, b \rangle$ to $b$ (after using uniqueness to show $a$ must be the default element) - The backward map sends an element $b : \beta \text{default}$ to $\langle \text{default}, b \rangle$
Equiv.uniqueSigma_apply theorem
{α} {β : α → Type*} [Unique α] (x : (a : α) × β a) : uniqueSigma β x = (Unique.eq_default _).rec x.2
Full source 
theorem uniqueSigma_apply {α} {β : α → Type*} [Unique α] (x : (a : α) × β a) :
    uniqueSigma β x = (Unique.eq_default _).rec x.2 :=
  rfl
Application of the equivalence between dependent product and fiber at default element
Informal description
For any type $\alpha$ with a unique element and any family of types $\beta : \alpha \to \text{Type}^*$, the equivalence `uniqueSigma β` maps a pair $\langle a, b \rangle$ in the dependent product type $(a : \alpha) \times \beta a$ to $b$, after using the uniqueness of $a$ to show that $a$ must be the default element of $\alpha$.
Equiv.uniqueSigma_symm_apply theorem
{α} {β : α → Type*} [Unique α] (y : β default) : (uniqueSigma β).symm y = ⟨default, y⟩
Full source 
@[simp]
theorem uniqueSigma_symm_apply {α} {β : α → Type*} [Unique α] (y : β default) :
    (uniqueSigma β).symm y = ⟨default, y⟩ :=
  rfl
Inverse of the equivalence between dependent product and fiber at default element
Informal description
For any type $\alpha$ with a unique element and any family of types $\beta : \alpha \to \text{Type}^*$, the inverse of the equivalence `uniqueSigma β` maps an element $y : \beta \text{default}$ to the pair $\langle \text{default}, y \rangle$.
Equiv.prodEmpty definition
(α) : α × Empty ≃ Empty
Full source 
/-- `Empty` type is a right absorbing element for type product up to an equivalence. -/
def prodEmpty (α) : α × Emptyα × Empty ≃ Empty :=
  equivEmpty _
Equivalence between product with empty type and empty type
Informal description
For any type $\alpha$, the product type $\alpha \times \text{Empty}$ is equivalent to the empty type $\text{Empty}$. This equivalence arises because the empty type acts as a right absorbing element for the product operation on types.
Equiv.emptyProd definition
(α) : Empty × α ≃ Empty
Full source 
/-- `Empty` type is a left absorbing element for type product up to an equivalence. -/
def emptyProd (α) : EmptyEmpty × αEmpty × α ≃ Empty :=
  equivEmpty _
Equivalence between $\text{Empty} \times \alpha$ and $\text{Empty}$
Informal description
The empty type is a left absorbing element for the product type up to an equivalence. Specifically, for any type $\alpha$, the product type $\text{Empty} \times \alpha$ is equivalent to $\text{Empty}$.
Equiv.prodPEmpty definition
(α) : α × PEmpty ≃ PEmpty
Full source 
/-- `PEmpty` type is a right absorbing element for type product up to an equivalence. -/
def prodPEmpty (α) : α × PEmptyα × PEmpty ≃ PEmpty :=
  equivPEmpty _
Equivalence between $\alpha \times \text{PEmpty}$ and $\text{PEmpty}$
Informal description
For any type $\alpha$, the product type $\alpha \times \text{PEmpty}$ is equivalent to the polymorphic empty type $\text{PEmpty}$. This equivalence arises because the second component of the product is empty, making the entire product type empty.
Equiv.pemptyProd definition
(α) : PEmpty × α ≃ PEmpty
Full source 
/-- `PEmpty` type is a left absorbing element for type product up to an equivalence. -/
def pemptyProd (α) : PEmptyPEmpty × αPEmpty × α ≃ PEmpty :=
  equivPEmpty _
Equivalence between `PEmpty × α` and `PEmpty`
Informal description
The polymorphic empty type `PEmpty` is a left absorbing element for the product type up to an equivalence. Specifically, for any type $\alpha$, there is a bijection between the product type `PEmpty × α` and `PEmpty`.
Equiv.prodCongrLeft definition
: β₁ × α₁ ≃ β₂ × α₁
Full source 
/-- A family of equivalences `∀ (a : α₁), β₁ ≃ β₂` generates an equivalence
between `β₁ × α₁` and `β₂ × α₁`. -/
def prodCongrLeft : β₁ × α₁β₁ × α₁ ≃ β₂ × α₁ where
  toFun ab := ⟨e ab.2 ab.1, ab.2⟩
  invFun ab := ⟨(e ab.2).symm ab.1, ab.2⟩
  left_inv := by
    rintro ⟨a, b⟩
    simp
  right_inv := by
    rintro ⟨a, b⟩
    simp
Equivalence of product types by left congruence
Informal description
Given a family of equivalences \( e : \forall (a : \alpha_1), \beta_1 \simeq \beta_2 \), the function `prodCongrLeft` constructs an equivalence between the product types \( \beta_1 \times \alpha_1 \) and \( \beta_2 \times \alpha_1 \). Specifically, it maps a pair \((b, a)\) to \((e(a)(b), a)\) and its inverse maps \((b', a)\) to \((e(a)^{-1}(b'), a)\).
Equiv.prodCongrLeft_apply theorem
(b : β₁) (a : α₁) : prodCongrLeft e (b, a) = (e a b, a)
Full source 
@[simp]
theorem prodCongrLeft_apply (b : β₁) (a : α₁) : prodCongrLeft e (b, a) = (e a b, a) :=
  rfl
Application of Product Left Congruence Equivalence
Informal description
For any elements $b \in \beta_1$ and $a \in \alpha_1$, the application of the equivalence $\text{prodCongrLeft}\, e$ to the pair $(b, a)$ yields $(e(a)(b), a)$.
Equiv.prodCongr_refl_right theorem
(e : β₁ ≃ β₂) : prodCongr e (Equiv.refl α₁) = prodCongrLeft fun _ => e
Full source 
theorem prodCongr_refl_right (e : β₁ ≃ β₂) :
    prodCongr e (Equiv.refl α₁) = prodCongrLeft fun _ => e := by
  ext ⟨a, b⟩ : 1
  simp
Equality of product congruences with right identity equivalence
Informal description
Given an equivalence $e : \beta_1 \simeq \beta_2$, the equivalence $\text{prodCongr}(e, \text{id}_{\alpha_1})$ between $\beta_1 \times \alpha_1$ and $\beta_2 \times \alpha_1$ is equal to the equivalence $\text{prodCongrLeft}$ constructed from the constant family of equivalences sending every $a \in \alpha_1$ to $e$.
Equiv.prodCongrRight definition
: α₁ × β₁ ≃ α₁ × β₂
Full source 
/-- A family of equivalences `∀ (a : α₁), β₁ ≃ β₂` generates an equivalence
between `α₁ × β₁` and `α₁ × β₂`. -/
def prodCongrRight : α₁ × β₁α₁ × β₁ ≃ α₁ × β₂ where
  toFun ab := ⟨ab.1, e ab.1 ab.2⟩
  invFun ab := ⟨ab.1, (e ab.1).symm ab.2⟩
  left_inv := by
    rintro ⟨a, b⟩
    simp
  right_inv := by
    rintro ⟨a, b⟩
    simp
Equivalence between product types with right component transformation
Informal description
Given a family of equivalences $e : \forall (a : \alpha_1), \beta_1 \simeq \beta_2$, the equivalence $\text{prodCongrRight} : \alpha_1 \times \beta_1 \simeq \alpha_1 \times \beta_2$ is defined by mapping $(a, b)$ to $(a, e(a)(b))$ and its inverse maps $(a, b)$ to $(a, e(a)^{-1}(b))$.
Equiv.prodCongrRight_apply theorem
(a : α₁) (b : β₁) : prodCongrRight e (a, b) = (a, e a b)
Full source 
@[simp]
theorem prodCongrRight_apply (a : α₁) (b : β₁) : prodCongrRight e (a, b) = (a, e a b) :=
  rfl
Application of Product Right Congruence Equivalence
Informal description
Given a family of equivalences $e : \alpha_1 \to (\beta_1 \simeq \beta_2)$, the application of the equivalence $\text{prodCongrRight}$ to a pair $(a, b) \in \alpha_1 \times \beta_1$ yields the pair $(a, e(a)(b)) \in \alpha_1 \times \beta_2$.
Equiv.prodCongr_refl_left theorem
(e : β₁ ≃ β₂) : prodCongr (Equiv.refl α₁) e = prodCongrRight fun _ => e
Full source 
theorem prodCongr_refl_left (e : β₁ ≃ β₂) :
    prodCongr (Equiv.refl α₁) e = prodCongrRight fun _ => e := by
  ext ⟨a, b⟩ : 1
  simp
Identity Equivalence Combined with $e$ Equals Right Component Transformation by $e$
Informal description
For any equivalence $e : \beta_1 \simeq \beta_2$, the equivalence obtained by combining the identity equivalence on $\alpha_1$ with $e$ is equal to the equivalence that applies $e$ to the second component of each pair while leaving the first component unchanged.
Equiv.prodCongrLeft_trans_prodComm theorem
: (prodCongrLeft e).trans (prodComm _ _) = (prodComm _ _).trans (prodCongrRight e)
Full source 
@[simp]
theorem prodCongrLeft_trans_prodComm :
    (prodCongrLeft e).trans (prodComm _ _) = (prodComm _ _).trans (prodCongrRight e) := by
  ext ⟨a, b⟩ : 1
  simp
Commutativity of Product Congruence and Swap Operations
Informal description
Given a family of equivalences $e : \forall (a : \alpha_1), \beta_1 \simeq \beta_2$, the composition of the left congruence equivalence $\text{prodCongrLeft} : \beta_1 \times \alpha_1 \simeq \beta_2 \times \alpha_1$ with the product commutativity equivalence $\text{prodComm} : \beta_2 \times \alpha_1 \simeq \alpha_1 \times \beta_2$ is equal to the composition of $\text{prodComm} : \beta_1 \times \alpha_1 \simeq \alpha_1 \times \beta_1$ with the right congruence equivalence $\text{prodCongrRight} : \alpha_1 \times \beta_1 \simeq \alpha_1 \times \beta_2$. In other words, the following diagram commutes: $$\begin{CD} \beta_1 \times \alpha_1 @>{\text{prodCongrLeft}}>> \beta_2 \times \alpha_1 \\ @V{\text{prodComm}}VV @VV{\text{prodComm}}V \\ \alpha_1 \times \beta_1 @>{\text{prodCongrRight}}>> \alpha_1 \times \beta_2 \end{CD}$$
Equiv.prodCongrRight_trans_prodComm theorem
: (prodCongrRight e).trans (prodComm _ _) = (prodComm _ _).trans (prodCongrLeft e)
Full source 
@[simp]
theorem prodCongrRight_trans_prodComm :
    (prodCongrRight e).trans (prodComm _ _) = (prodComm _ _).trans (prodCongrLeft e) := by
  ext ⟨a, b⟩ : 1
  simp
Commutativity of Product Congruence and Swap: $\text{prodCongrRight} \circ \text{prodComm} = \text{prodComm} \circ \text{prodCongrLeft}$
Informal description
Given a family of equivalences $e : \forall (a : \alpha_1), \beta_1 \simeq \beta_2$, the composition of the right congruence equivalence $\text{prodCongrRight} : \alpha_1 \times \beta_1 \simeq \alpha_1 \times \beta_2$ with the product commutativity equivalence $\text{prodComm} : \alpha_1 \times \beta_2 \simeq \beta_2 \times \alpha_1$ is equal to the composition of the product commutativity equivalence $\text{prodComm} : \beta_1 \times \alpha_1 \simeq \alpha_1 \times \beta_1$ with the left congruence equivalence $\text{prodCongrLeft} : \beta_1 \times \alpha_1 \simeq \beta_2 \times \alpha_1$. In other words, the following diagram commutes: $$ \begin{CD} \alpha_1 \times \beta_1 @>{\text{prodCongrRight}}>> \alpha_1 \times \beta_2 \\ @V{\text{prodComm}}VV @VV{\text{prodComm}}V \\ \beta_1 \times \alpha_1 @>{\text{prodCongrLeft}}>> \beta_2 \times \alpha_1 \end{CD} $$
Equiv.sigmaCongrRight_sigmaEquivProd theorem
: (sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂) = (sigmaEquivProd α₁ β₁).trans (prodCongrRight e)
Full source 
theorem sigmaCongrRight_sigmaEquivProd :
    (sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂)
    = (sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
  ext ⟨a, b⟩ : 1
  simp
Commutative Diagram: Sigma Congruence Right and Sigma-Product Equivalence
Informal description
Let $\alpha_1$ be a type, and let $\beta_1, \beta_2 : \alpha_1 \to \text{Type}$ be type families indexed by $\alpha_1$. Given a family of equivalences $e : \forall a, \beta_1 a \simeq \beta_2 a$, the following diagram commutes: $$ \begin{CD} (\Sigma a, \beta_1 a) @>\text{sigmaCongrRight }e>> (\Sigma a, \beta_2 a) \\ @V\text{sigmaEquivProd } \alpha_1 \beta_1 VV @VV\text{sigmaEquivProd } \alpha_1 \beta_2 V \\ \alpha_1 \times \beta_1 @>>\text{prodCongrRight }e> \alpha_1 \times \beta_2 \end{CD} $$ That is, the composition of `sigmaCongrRight e` followed by `sigmaEquivProd α₁ β₂` is equal to the composition of `sigmaEquivProd α₁ β₁` followed by `prodCongrRight e`.
Equiv.sigmaEquivProd_sigmaCongrRight theorem
: (sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e) = (prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm
Full source 
theorem sigmaEquivProd_sigmaCongrRight :
    (sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e)
    = (prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm := by
  ext ⟨a, b⟩ : 1
  simp only [trans_apply, sigmaCongrRight_apply, prodCongrRight_apply]
  rfl
Commutative Diagram: Sigma-Product Equivalence and Sigma Congruence Right
Informal description
Let $\alpha_1$ be a type and $\beta_1, \beta_2 : \alpha_1 \to \text{Type}$ be type families indexed by $\alpha_1$. Given a family of equivalences $e : \forall a, \beta_1 a \simeq \beta_2 a$, the following diagram commutes: $$ \begin{CD} \alpha_1 \times \beta_1 @>\text{prodCongrRight }e>> \alpha_1 \times \beta_2 \\ @A\text{sigmaEquivProd } \alpha_1 \beta_1 AA @AA\text{sigmaEquivProd } \alpha_1 \beta_2 A \\ (\Sigma a, \beta_1 a) @>>\text{sigmaCongrRight }e> (\Sigma a, \beta_2 a) \end{CD} $$ That is, the composition of the inverse of $\text{sigmaEquivProd } \alpha_1 \beta_1$ with $\text{sigmaCongrRight } e$ is equal to the composition of $\text{prodCongrRight } e$ with the inverse of $\text{sigmaEquivProd } \alpha_1 \beta_2$.
Equiv.prodShear definition
(e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂
Full source 
/-- 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. -/
@[simps -fullyApplied]
def prodShear (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) : α₁ × β₁α₁ × β₁ ≃ α₂ × β₂ where
  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 := by
    rintro ⟨x₁, y₁⟩
    simp only [symm_apply_apply]
  right_inv := by
    rintro ⟨x₁, y₁⟩
    simp only [apply_symm_apply]
Dependent Product Equivalence (Shear Mapping)
Informal description
Given an equivalence $e_1 : \alpha_1 \simeq \alpha_2$ and a family of equivalences $e_2 : \alpha_1 \to (\beta_1 \simeq \beta_2)$, the equivalence $\text{prodShear}$ constructs a bijection between $\alpha_1 \times \beta_1$ and $\alpha_2 \times \beta_2$. The forward map sends $(x, y)$ to $(e_1(x), e_2(x)(y))$, while the inverse map sends $(x', y')$ to $(e_1^{-1}(x'), e_2(e_1^{-1}(x'))^{-1}(y'))$. This is a generalization of $\text{prodCongr}$ where the second equivalence can depend on the first component.
Equiv.Perm.prodExtendRight definition
: Perm (α₁ × β₁)
Full source 
/-- `prodExtendRight a e` extends `e : Perm β` to `Perm (α × β)` by sending `(a, b)` to
`(a, e b)` and keeping the other `(a', b)` fixed. -/
def prodExtendRight : Perm (α₁ × β₁) where
  toFun ab := if ab.fst = a then (a, e ab.snd) else ab
  invFun ab := if ab.fst = a then (a, e.symm ab.snd) else ab
  left_inv := by
    rintro ⟨k', x⟩
    dsimp only
    split_ifs with h₁ h₂
    · simp [h₁]
    · simp at h₂
    · simp
  right_inv := by
    rintro ⟨k', x⟩
    dsimp only
    split_ifs with h₁ h₂
    · simp [h₁]
    · simp at h₂
    · simp
Extension of a permutation to a product type
Informal description
Given a fixed element $a \in \alpha_1$ and a permutation $e$ of $\beta_1$, the function `prodExtendRight` extends $e$ to a permutation of $\alpha_1 \times \beta_1$ by applying $e$ to the second component of pairs $(a, b)$ while keeping all other pairs $(a', b)$ with $a' \neq a$ unchanged.
Equiv.Perm.prodExtendRight_apply_eq theorem
(b : β₁) : prodExtendRight a e (a, b) = (a, e b)
Full source 
@[simp]
theorem prodExtendRight_apply_eq (b : β₁) : prodExtendRight a e (a, b) = (a, e b) :=
  if_pos rfl
Action of $\text{prodExtendRight}$ on Pairs with Fixed First Component
Informal description
For any element $b$ in $\beta_1$, the permutation $\text{prodExtendRight}$ applied to the pair $(a, b)$ yields $(a, e(b))$, where $e$ is the given permutation on $\beta_1$.
Equiv.Perm.prodExtendRight_apply_ne theorem
{a a' : α₁} (h : a' ≠ a) (b : β₁) : prodExtendRight a e (a', b) = (a', b)
Full source 
theorem prodExtendRight_apply_ne {a a' : α₁} (h : a' ≠ a) (b : β₁) :
    prodExtendRight a e (a', b) = (a', b) :=
  if_neg h
Fixed Point Property of Product Permutation Extension for Distinct First Components
Informal description
For any elements $a, a' \in \alpha_1$ with $a' \neq a$ and any $b \in \beta_1$, the permutation `prodExtendRight` applied to the pair $(a', b)$ returns $(a', b)$ unchanged.
Equiv.Perm.fst_prodExtendRight theorem
(ab : α₁ × β₁) : (prodExtendRight a e ab).fst = ab.fst
Full source 
@[simp]
theorem fst_prodExtendRight (ab : α₁ × β₁) : (prodExtendRight a e ab).fst = ab.fst := by
  rw [prodExtendRight]
  dsimp
  split_ifs with h
  · rw [h]
  · rfl
First Projection Invariance Under $\text{prodExtendRight}$ Permutation
Informal description
For any element $(a', b) \in \alpha_1 \times \beta_1$, the first projection of the permutation $\text{prodExtendRight}(a, e)$ applied to $(a', b)$ equals $a'$, i.e., $$(\text{prodExtendRight}(a, e)(a', b)).1 = a'.$$
Equiv.arrowProdEquivProdArrow definition
(α : Type*) (β γ : α → Type*) : ((i : α) → β i × γ i) ≃ ((i : α) → β i) × ((i : α) → γ i)
Full source 
/-- The type of functions to a product `β × γ` is equivalent to the type of pairs of functions
`α → β` and `β → γ`. -/
@[simps]
def arrowProdEquivProdArrow (α : Type*) (β γ : α → Type*) :
    ((i : α) → β i × γ i) ≃ ((i : α) → β i) × ((i : α) → γ i) where
  toFun := fun f => (fun c => (f c).1, fun c => (f c).2)
  invFun := fun p c => (p.1 c, p.2 c)
  left_inv := fun _ => rfl
  right_inv := fun p => by cases p; rfl
Equivalence between product-valued functions and pairs of functions
Informal description
For any type $\alpha$ and type families $\beta, \gamma : \alpha \to \text{Type}$, the type of functions $\prod_{i \in \alpha} (\beta(i) \times \gamma(i))$ is equivalent to the product type $\left(\prod_{i \in \alpha} \beta(i)\right) \times \left(\prod_{i \in \alpha} \gamma(i)\right)$. The equivalence is given by: - The forward map splits a function $f$ into two functions $(f_1, f_2)$ where $f_1(i) = (f(i)).1$ and $f_2(i) = (f(i)).2$ - The inverse map combines two functions $p = (p_1, p_2)$ into a single function $\lambda i \mapsto (p_1(i), p_2(i))$
Equiv.sumPiEquivProdPi definition
{ι ι'} (π : ι ⊕ ι' → Type*) : (∀ i, π i) ≃ (∀ i, π (inl i)) × ∀ i', π (inr i')
Full source 
/-- 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`. -/
@[simps]
def sumPiEquivProdPi {ι ι'} (π : ι ⊕ ι' → Type*) :
    (∀ i, π i) ≃ (∀ i, π (inl i)) × ∀ i', π (inr i') where
  toFun f := ⟨fun i => f (inl i), fun i' => f (inr i')⟩
  invFun g := Sum.rec g.1 g.2
  left_inv f := by ext (i | i) <;> rfl
  right_inv _ := Prod.ext rfl rfl
Equivalence between dependent functions on a sum type and product of dependent functions
Informal description
For any types $\iota$ and $\iota'$ and any family of types $\pi$ indexed by $\iota \oplus \iota'$, the type of dependent functions $\prod_{i \in \iota \oplus \iota'} \pi(i)$ is equivalent to the product type $\left(\prod_{i \in \iota} \pi(\text{inl}(i))\right) \times \left(\prod_{i' \in \iota'} \pi(\text{inr}(i'))\right)$. Here, $\text{inl}$ and $\text{inr}$ are the left and right inclusion maps into the sum type $\iota \oplus \iota'$.
Equiv.prodPiEquivSumPi definition
{ι ι'} (π : ι → Type u) (π' : ι' → Type u) : ((∀ i, π i) × ∀ i', π' i') ≃ ∀ i, Sum.elim π π' i
Full source 
/-- The equivalence between a product of two dependent functions types and a single dependent
function type. Basically a symmetric version of `Equiv.sumPiEquivProdPi`. -/
@[simps!]
def prodPiEquivSumPi {ι ι'} (π : ι → Type u) (π' : ι' → Type u) :
    ((∀ i, π i) × ∀ i', π' i') ≃ ∀ i, Sum.elim π π' i :=
  sumPiEquivProdPi (Sum.elim π π') |>.symm
Equivalence between product of dependent functions and dependent functions on a sum type
Informal description
For any types $\iota$ and $\iota'$ and type families $\pi : \iota \to \text{Type}$ and $\pi' : \iota' \to \text{Type}$, the product type $\left(\prod_{i \in \iota} \pi(i)\right) \times \left(\prod_{i' \in \iota'} \pi'(i')\right)$ is equivalent to the type of dependent functions $\prod_{i \in \iota \oplus \iota'} \text{Sum.elim}\ \pi\ \pi'(i)$, where $\text{Sum.elim}\ \pi\ \pi'$ is the function that applies $\pi$ to $\text{inl}(i)$ and $\pi'$ to $\text{inr}(i')$. This equivalence is obtained as the inverse of the equivalence between $\prod_{i \in \iota \oplus \iota'} \text{Sum.elim}\ \pi\ \pi'(i)$ and $\left(\prod_{i \in \iota} \pi(i)\right) \times \left(\prod_{i' \in \iota'} \pi'(i')\right)$.
Equiv.sumArrowEquivProdArrow definition
(α β γ : Type*) : (α ⊕ β → γ) ≃ (α → γ) × (β → γ)
Full source 
/-- The type of functions on a sum type `α ⊕ β` is equivalent to the type of pairs of functions
on `α` and on `β`. -/
def sumArrowEquivProdArrow (α β γ : Type*) : (α ⊕ β → γ) ≃ (α → γ) × (β → γ) :=
  ⟨fun f => (f ∘ inl, f ∘ inr), fun p => Sum.elim p.1 p.2, fun f => by ext ⟨⟩ <;> rfl, fun p => by
    cases p
    rfl⟩
Equivalence between functions on a sum type and product of functions
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, the type of functions from the sum type $\alpha \oplus \beta$ to $\gamma$ is equivalent to the product type $(\alpha \to \gamma) \times (\beta \to \gamma)$. The equivalence is given by the pair of functions $(f \circ \text{inl}, f \circ \text{inr})$ for the forward direction and $\text{Sum.elim} p.1 p.2$ for the backward direction, where $p$ is a pair of functions.
Equiv.sumArrowEquivProdArrow_apply_fst theorem
{α β γ} (f : α ⊕ β → γ) (a : α) : (sumArrowEquivProdArrow α β γ f).1 a = f (inl a)
Full source 
@[simp]
theorem sumArrowEquivProdArrow_apply_fst {α β γ} (f : α ⊕ β → γ) (a : α) :
    (sumArrowEquivProdArrow α β γ f).1 a = f (inl a) :=
  rfl
First Component of Sum-to-Product Function Equivalence Evaluates Left Injection
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, given a function $f : \alpha \oplus \beta \to \gamma$ and an element $a : \alpha$, the first component of the equivalence $\text{sumArrowEquivProdArrow}_{\alpha,\beta,\gamma}(f)$ evaluated at $a$ is equal to $f$ applied to $\text{inl}(a)$. In other words, $(\text{sumArrowEquivProdArrow}_{\alpha,\beta,\gamma}(f))_1(a) = f(\text{inl}(a))$.
Equiv.sumArrowEquivProdArrow_apply_snd theorem
{α β γ} (f : α ⊕ β → γ) (b : β) : (sumArrowEquivProdArrow α β γ f).2 b = f (inr b)
Full source 
@[simp]
theorem sumArrowEquivProdArrow_apply_snd {α β γ} (f : α ⊕ β → γ) (b : β) :
    (sumArrowEquivProdArrow α β γ f).2 b = f (inr b) :=
  rfl
Second Component of Sum-to-Product Function Equivalence Evaluates Right Injection
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, given a function $f : \alpha \oplus \beta \to \gamma$ and an element $b : \beta$, the second component of the equivalence $\text{sumArrowEquivProdArrow}$ applied to $f$ evaluated at $b$ is equal to $f$ applied to $\text{inr}(b)$. In other words, $(\text{sumArrowEquivProdArrow}_{\alpha,\beta,\gamma}(f))_2(b) = f(\text{inr}(b))$.
Equiv.sumArrowEquivProdArrow_symm_apply_inl theorem
{α β γ} (f : α → γ) (g : β → γ) (a : α) : ((sumArrowEquivProdArrow α β γ).symm (f, g)) (inl a) = f a
Full source 
@[simp]
theorem sumArrowEquivProdArrow_symm_apply_inl {α β γ} (f : α → γ) (g : β → γ) (a : α) :
    ((sumArrowEquivProdArrow α β γ).symm (f, g)) (inl a) = f a :=
  rfl
Inverse Sum-to-Product Equivalence Evaluates Left Injection as First Function
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, given functions $f : \alpha \to \gamma$ and $g : \beta \to \gamma$, and an element $a : \alpha$, the inverse of the equivalence $\text{sumArrowEquivProdArrow}_{\alpha,\beta,\gamma}$ applied to the pair $(f, g)$ and evaluated at $\text{inl}(a)$ is equal to $f(a)$. In other words, $(\text{sumArrowEquivProdArrow}_{\alpha,\beta,\gamma})^{-1}(f, g)(\text{inl}(a)) = f(a)$.
Equiv.sumArrowEquivProdArrow_symm_apply_inr theorem
{α β γ} (f : α → γ) (g : β → γ) (b : β) : ((sumArrowEquivProdArrow α β γ).symm (f, g)) (inr b) = g b
Full source 
@[simp]
theorem sumArrowEquivProdArrow_symm_apply_inr {α β γ} (f : α → γ) (g : β → γ) (b : β) :
    ((sumArrowEquivProdArrow α β γ).symm (f, g)) (inr b) = g b :=
  rfl
Inverse Sum-to-Product Equivalence Evaluates Right Injection as Second Function
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, given functions $f : \alpha \to \gamma$ and $g : \beta \to \gamma$, and an element $b \in \beta$, the inverse of the equivalence $\alpha \oplus \beta \to \gamma \simeq (\alpha \to \gamma) \times (\beta \to \gamma)$ applied to $(f, g)$ and evaluated at $\text{inr}(b)$ equals $g(b)$. In other words, if $e$ is the equivalence between functions from a sum type and pairs of functions, then $e^{-1}(f, g)(\text{inr}(b)) = g(b)$.
Equiv.sumProdDistrib definition
(α β γ) : (α ⊕ β) × γ ≃ α × γ ⊕ β × γ
Full source 
/-- Type product is right distributive with respect to type sum up to an equivalence. -/
def sumProdDistrib (α β γ) : (α ⊕ β) × γ(α ⊕ β) × γ ≃ α × γ ⊕ β × γ :=
  ⟨fun p => p.1.map (fun x => (x, p.2)) fun x => (x, p.2),
    fun s => s.elim (Prod.map inl id) (Prod.map inr id), by
      rintro ⟨_ | _, _⟩ <;> rfl, by rintro (⟨_, _⟩ | ⟨_, _⟩) <;> rfl⟩
Right distributivity of product over sum
Informal description
The equivalence $(α ⊕ β) × γ ≃ (α × γ) ⊕ (β × γ)$ shows that the product type is right distributive with respect to the sum type. It maps a pair $(x, c)$ where $x$ is either in $α$ or $β$ to either $(a, c)$ if $x = \text{inl } a$ or $(b, c)$ if $x = \text{inr } b$.
Equiv.sumProdDistrib_apply_left theorem
{α β γ} (a : α) (c : γ) : sumProdDistrib α β γ (Sum.inl a, c) = Sum.inl (a, c)
Full source 
@[simp]
theorem sumProdDistrib_apply_left {α β γ} (a : α) (c : γ) :
    sumProdDistrib α β γ (Sum.inl a, c) = Sum.inl (a, c) :=
  rfl
Application of Sum-Product Distributivity Equivalence on Left Injection
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, given an element $a \in \alpha$ and $c \in \gamma$, the equivalence $\text{sumProdDistrib}$ maps the pair $(\text{inl } a, c)$ to $\text{inl } (a, c)$.
Equiv.sumProdDistrib_apply_right theorem
{α β γ} (b : β) (c : γ) : sumProdDistrib α β γ (Sum.inr b, c) = Sum.inr (b, c)
Full source 
@[simp]
theorem sumProdDistrib_apply_right {α β γ} (b : β) (c : γ) :
    sumProdDistrib α β γ (Sum.inr b, c) = Sum.inr (b, c) :=
  rfl
Application of Sum-Product Distributivity Equivalence on Right Injection
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, given an element $b \in \beta$ and $c \in \gamma$, the equivalence $\text{sumProdDistrib}$ maps the pair $(\text{inr } b, c)$ to $\text{inr } (b, c)$.
Equiv.sumProdDistrib_symm_apply_left theorem
{α β γ} (a : α × γ) : (sumProdDistrib α β γ).symm (inl a) = (inl a.1, a.2)
Full source 
@[simp]
theorem sumProdDistrib_symm_apply_left {α β γ} (a : α × γ) :
    (sumProdDistrib α β γ).symm (inl a) = (inl a.1, a.2) :=
  rfl
Inverse of Sum-Product Distributivity on Left Injection
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, and any pair $(a, c) \in \alpha \times \gamma$, the inverse of the sum-product distributivity equivalence maps the left injection of $(a, c)$ to the pair consisting of the left injection of $a$ and $c$. That is, $(\text{sumProdDistrib } \alpha \beta \gamma)^{-1}(\text{inl } (a, c)) = (\text{inl } a, c)$.
Equiv.sumProdDistrib_symm_apply_right theorem
{α β γ} (b : β × γ) : (sumProdDistrib α β γ).symm (inr b) = (inr b.1, b.2)
Full source 
@[simp]
theorem sumProdDistrib_symm_apply_right {α β γ} (b : β × γ) :
    (sumProdDistrib α β γ).symm (inr b) = (inr b.1, b.2) :=
  rfl
Inverse of Sum-Product Distributivity on Right Injection
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, and any pair $(b, c) \in \beta \times \gamma$, the inverse of the sum-product distributivity equivalence maps the right injection of $(b, c)$ to the pair consisting of the right injection of $b$ and $c$. That is, $(\text{sumProdDistrib } \alpha \beta \gamma)^{-1}(\text{inr } (b, c)) = (\text{inr } b, c)$.
Equiv.sigmaProdDistrib definition
{ι} (α : ι → Type*) (β) : (Σ i, α i) × β ≃ Σ i, α i × β
Full source 
/-- 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 × β)`. -/
@[simps apply symm_apply]
def sigmaProdDistrib {ι} (α : ι → Type*) (β) : (Σ i, α i) × β(Σ i, α i) × β ≃ Σ i, α i × β :=
  ⟨fun p => ⟨p.1.1, (p.1.2, p.2)⟩, fun p => (⟨p.1, p.2.1⟩, p.2.2), fun p => by
    rcases p with ⟨⟨_, _⟩, _⟩
    rfl, fun p => by
    rcases p with ⟨_, ⟨_, _⟩⟩
    rfl⟩
Distributivity of product over indexed sum
Informal description
The equivalence states that for an indexed family of types $\alpha_i$ (where $i$ ranges over some index type $\iota$) and a type $\beta$, the product $(\Sigma i, \alpha_i) \times \beta$ is equivalent to the sum $\Sigma i, (\alpha_i \times \beta)$. More precisely, the equivalence maps a pair $((i, a), b)$ to $(i, (a, b))$ and vice versa, establishing a bijection between these two types.
Equiv.boolProdEquivSum definition
(α) : Bool × α ≃ α ⊕ α
Full source 
/-- The product `Bool × α` is equivalent to `α ⊕ α`. -/
@[simps]
def boolProdEquivSum (α) : BoolBool × αBool × α ≃ α ⊕ α where
  toFun p := p.1.casesOn (inl p.2) (inr p.2)
  invFun := Sum.elim (Prod.mk false) (Prod.mk true)
  left_inv := by rintro ⟨_ | _, _⟩ <;> rfl
  right_inv := by rintro (_ | _) <;> rfl
Equivalence between Boolean product and sum of two copies
Informal description
The product type $\text{Bool} \times \alpha$ is equivalent to the sum type $\alpha \oplus \alpha$. More precisely, the equivalence maps: - A pair $(\text{false}, a)$ to $\text{inl}\, a$ (left injection) - A pair $(\text{true}, a)$ to $\text{inr}\, a$ (right injection) - Conversely, $\text{inl}\, a$ maps to $(\text{false}, a)$ - $\text{inr}\, a$ maps to $(\text{true}, a)$
Equiv.boolArrowEquivProd definition
(α) : (Bool → α) ≃ α × α
Full source 
/-- The function type `Bool → α` is equivalent to `α × α`. -/
@[simps]
def boolArrowEquivProd (α) : (Bool → α) ≃ α × α where
  toFun f := (f false, f true)
  invFun p b := b.casesOn p.1 p.2
  left_inv _ := funext <| Bool.forall_bool.2 ⟨rfl, rfl⟩
  right_inv := fun _ => rfl
Equivalence between Boolean functions and pairs
Informal description
The function type $\text{Bool} \to \alpha$ is equivalent to the product type $\alpha \times \alpha$. More precisely, the equivalence maps: - A function $f : \text{Bool} \to \alpha$ to the pair $(f(\text{false}), f(\text{true}))$ - A pair $(a_1, a_2) \in \alpha \times \alpha$ to the function that sends $\text{false}$ to $a_1$ and $\text{true}$ to $a_2$
Equiv.subtypeProdEquivProd definition
{α β} {p : α → Prop} {q : β → Prop} : { c : α × β // p c.1 ∧ q c.2 } ≃ { a // p a } × { b // q b }
Full source 
/-- A subtype of a product defined by componentwise conditions
is equivalent to a product of subtypes. -/
def subtypeProdEquivProd {α β} {p : α → Prop} {q : β → Prop} :
    { c : α × β // p c.1 ∧ q c.2 }{ c : α × β // p c.1 ∧ q c.2 } ≃ { a // p a } × { b // q b } where
  toFun := fun x => ⟨⟨x.1.1, x.2.1⟩, ⟨x.1.2, x.2.2⟩⟩
  invFun := fun x => ⟨⟨x.1.1, x.2.1⟩, ⟨x.1.2, x.2.2⟩⟩
  left_inv := fun ⟨⟨_, _⟩, ⟨_, _⟩⟩ => rfl
  right_inv := fun ⟨⟨_, _⟩, ⟨_, _⟩⟩ => rfl
Equivalence between Subtype of Product and Product of Subtypes
Informal description
For any types $\alpha$ and $\beta$ with predicates $p : \alpha \to \text{Prop}$ and $q : \beta \to \text{Prop}$, the subtype $\{ c : \alpha \times \beta \mid p\, c.1 \land q\, c.2 \}$ of pairs $(a, b)$ where $a$ satisfies $p$ and $b$ satisfies $q$ is equivalent to the product $\{ a \mid p\, a \} \times \{ b \mid q\, b \}$ of the individual subtypes.
Equiv.prodSubtypeFstEquivSubtypeProd definition
{α β} {p : α → Prop} : { s : α × β // p s.1 } ≃ { a // p a } × β
Full source 
/-- 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. -/
def prodSubtypeFstEquivSubtypeProd {α β} {p : α → Prop} :
    {s : α × β // p s.1}{s : α × β // p s.1} ≃ {a // p a} × β where
  toFun x := ⟨⟨x.1.1, x.2⟩, x.1.2⟩
  invFun x := ⟨⟨x.1.1, x.2⟩, x.1.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between product subtype (first component restricted) and product of restricted type
Informal description
For any types $\alpha$ and $\beta$ with a predicate $p : \alpha \to \text{Prop}$, the subtype $\{ s : \alpha \times \beta \mid p\, s.1 \}$ of pairs $(a, b)$ where the first component $a$ satisfies $p$ is equivalent to the product $\{ a \mid p\, a \} \times \beta$ of the subtype of $\alpha$ satisfying $p$ with $\beta$. More precisely, the equivalence maps: - A pair $(a, b)$ in the subtype (where $p\, a$ holds) to $(\langle a, \text{proof of } p\, a \rangle, b)$ - An element $(\langle a, h \rangle, b)$ of the product back to $\langle (a, b), h \rangle$
Equiv.subtypeProdEquivSigmaSubtype definition
{α β} (p : α → β → Prop) : { x : α × β // p x.1 x.2 } ≃ Σ a, { b : β // p a b }
Full source 
/-- A subtype of a `Prod` is equivalent to a sigma type whose fibers are subtypes. -/
def subtypeProdEquivSigmaSubtype {α β} (p : α → β → Prop) :
    { x : α × β // p x.1 x.2 }{ x : α × β // p x.1 x.2 } ≃ Σa, { b : β // p a b } where
  toFun x := ⟨x.1.1, x.1.2, x.property⟩
  invFun x := ⟨⟨x.1, x.2⟩, x.2.property⟩
  left_inv x := by ext <;> rfl
  right_inv := fun ⟨_, _, _⟩ => rfl
Equivalence between Subtype of Product and Sigma Type of Subtypes
Informal description
For any types $\alpha$ and $\beta$ and a predicate $p : \alpha \to \beta \to \text{Prop}$, the subtype $\{ x : \alpha \times \beta \mid p\, x.1\, x.2 \}$ of pairs $(a, b)$ satisfying $p\, a\, b$ is equivalent to the sigma type $\Sigma a, \{ b : \beta \mid p\, a\, b \}$ consisting of pairs $(a, b)$ where $a$ is in $\alpha$ and $b$ is in $\beta$ satisfying $p\, a\, b$.
Equiv.piEquivPiSubtypeProd definition
{α : Type*} (p : α → Prop) (β : α → Type*) [DecidablePred p] : (∀ i : α, β i) ≃ (∀ i : { x // p x }, β i) × ∀ i : { x // ¬p x }, β i
Full source 
/-- 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. -/
@[simps]
def piEquivPiSubtypeProd {α : Type*} (p : α → Prop) (β : α → Type*) [DecidablePred p] :
    (∀ i : α, β i) ≃ (∀ i : { x // p x }, β i) × ∀ i : { x // ¬p x }, β i where
  toFun f := (fun x => f x, fun x => f x)
  invFun f x := if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
  right_inv := by
    rintro ⟨f, g⟩
    ext1 <;>
      · ext y
        rcases y with ⟨val, property⟩
        simp only [property, dif_pos, dif_neg, not_false_iff, Subtype.coe_mk]
  left_inv f := by
    ext x
    by_cases h : p x <;>
      · simp only [h, dif_neg, dif_pos, not_false_iff]
Equivalence between dependent functions and product of restricted functions
Informal description
For a type $\alpha$ with a decidable predicate $p : \alpha \to \text{Prop}$ and a type family $\beta : \alpha \to \text{Type}$, the type of dependent functions $\forall i : \alpha, \beta i$ is equivalent to the product of the types of dependent functions over the subtypes $\{x \mid p x\}$ and $\{x \mid \neg p x\}$. More precisely, the equivalence maps a function $f$ to the pair $(f \restriction_{\{x \mid p x\}}, f \restriction_{\{x \mid \neg p x\}})$, and its inverse reconstructs $f$ by case analysis on $p x$.
Equiv.piSplitAt definition
{α : Type*} [DecidableEq α] (i : α) (β : α → Type*) : (∀ j, β j) ≃ β i × ∀ j : { j // j ≠ i }, β j
Full source 
/-- A product of types can be split as the binary product of one of the types and the product
  of all the remaining types. -/
@[simps]
def piSplitAt {α : Type*} [DecidableEq α] (i : α) (β : α → Type*) :
    (∀ j, β j) ≃ β i × ∀ j : { j // j ≠ i }, β j where
  toFun f := ⟨f i, fun j => f j⟩
  invFun f j := if h : j = i then h.symm.rec f.1 else f.2 ⟨j, h⟩
  right_inv f := by
    ext x
    exacts [dif_pos rfl, (dif_neg x.2).trans (by cases x; rfl)]
  left_inv f := by
    ext x
    dsimp only
    split_ifs with h
    · subst h; rfl
    · rfl
Splitting dependent functions at a point
Informal description
For a type $\alpha$ with decidable equality and a type family $\beta : \alpha \to \text{Type}$, the type of dependent functions $\forall j, \beta j$ is equivalent to the product of $\beta i$ and the type of dependent functions $\forall j \in \{j \mid j \neq i\}, \beta j$. The equivalence maps a function $f$ to the pair $(f(i), f \restriction_{\{j \mid j \neq i\}})$, and its inverse reconstructs $f$ by evaluating at $i$ or using the restriction as appropriate.
Equiv.funSplitAt definition
{α : Type*} [DecidableEq α] (i : α) (β : Type*) : (α → β) ≃ β × ({ j // j ≠ i } → β)
Full source 
/-- 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. -/
@[simps!]
def funSplitAt {α : Type*} [DecidableEq α] (i : α) (β : Type*) :
    (α → β) ≃ β × ({ j // j ≠ i } → β) :=
  piSplitAt i _
Splitting functions at a point
Informal description
For a type $\alpha$ with decidable equality and a type $\beta$, the type of functions $\alpha \to \beta$ is equivalent to the product of $\beta$ and the type of functions $\{j \mid j \neq i\} \to \beta$. The equivalence maps a function $f$ to the pair $(f(i), f \restriction_{\{j \mid j \neq i\}})$, and its inverse reconstructs $f$ by evaluating at $i$ or using the restriction as appropriate.
subsingletonProdSelfEquiv definition
{α} [Subsingleton α] : α × α ≃ α
Full source 
/-- If `α` is a subsingleton, then it is equivalent to `α × α`. -/
def subsingletonProdSelfEquiv {α} [Subsingleton α] : α × αα × α ≃ α where
  toFun p := p.1
  invFun a := (a, a)
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _
Equivalence between a subsingleton and its product with itself
Informal description
For a type $\alpha$ that is a subsingleton (i.e., any two elements of $\alpha$ are equal), the product type $\alpha \times \alpha$ is equivalent to $\alpha$ itself. The equivalence maps a pair $(a, b)$ to $a$ (or equivalently to $b$ since $\alpha$ is a subsingleton), and its inverse maps an element $a$ to the pair $(a, a)$.