doc-next-gen

Mathlib.Data.Sigma.Basic

Module docstring

{"# Sigma types

This file proves basic results about sigma types.

A sigma type is a dependent pair type. Like α × β but where the type of the second component depends on the first component. More precisely, given β : ι → Type*, Sigma β is made of stuff which is of type β i for some i : ι, so the sigma type is a disjoint union of types. For example, the sum type X ⊕ Y can be emulated using a sigma type, by taking ι with exactly two elements (see Equiv.sumEquivSigmaBool).

Σ x, A x is notation for Sigma A (note that this is \\Sigma, not the sum operator ∑). Σ x y z ..., A x y z ... is notation for Σ x, Σ y, Σ z, ..., A x y z .... Here we have α : Type*, β : α → Type*, γ : Π a : α, β a → Type*, ..., A : Π (a : α) (b : β a) (c : γ a b) ..., Type* with x : α y : β x, z : γ x y, ...

Notes

The definition of Sigma takes values in Type*. This effectively forbids Prop- valued sigma types. To that effect, we have PSigma, which takes value in Sort* and carries a more complicated universe signature as a consequence. "}

Sigma.instInhabitedSigma instance
[Inhabited α] [Inhabited (β default)] : Inhabited (Sigma β)
Full source 
instance instInhabitedSigma [Inhabited α] [Inhabited (β default)] : Inhabited (Sigma β) :=
  ⟨⟨default, default⟩⟩
Inhabited Sigma Type from Inhabited Base and Fiber
Informal description
For any type $\alpha$ with a default element and a family of types $\beta : \alpha \to \text{Type}$ where $\beta$ evaluated at the default element of $\alpha$ also has a default element, the sigma type $\Sigma a, \beta a$ is inhabited.
Sigma.instDecidableEqSigma instance
[h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq (β a)] : DecidableEq (Sigma β)
Full source 
instance instDecidableEqSigma [h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq (β a)] :
    DecidableEq (Sigma β)
  | ⟨a₁, b₁⟩, ⟨a₂, b₂⟩ =>
    match a₁, b₁, a₂, b₂, h₁ a₁ a₂ with
    | _, b₁, _, b₂, isTrue (Eq.refl _) =>
      match b₁, b₂, h₂ _ b₁ b₂ with
      | _, _, isTrue (Eq.refl _) => isTrue rfl
      | _, _, isFalse n => isFalse fun h ↦ Sigma.noConfusion h fun _ e₂ ↦ n <| eq_of_heq e₂
    | _, _, _, _, isFalse n => isFalse fun h ↦ Sigma.noConfusion h fun e₁ _ ↦ n e₁
Decidable Equality of Sigma Types
Informal description
For any type $\alpha$ with decidable equality and any family of types $\beta : \alpha \to \text{Type}$ where each $\beta(a)$ has decidable equality, the sigma type $\Sigma a, \beta(a)$ also has decidable equality.
Sigma.mk.inj_iff theorem
{a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} : Sigma.mk a₁ b₁ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂
Full source 
theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
    Sigma.mkSigma.mk a₁ b₁ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂ := by simp
Injective Property of Sigma Constructor: $\langle a_1, b_1 \rangle = \langle a_2, b_2 \rangle \leftrightarrow (a_1 = a_2) \land (b_1 \equiv b_2)$
Informal description
For any elements $a_1, a_2 : \alpha$ and $b_1 : \beta(a_1)$, $b_2 : \beta(a_2)$, the equality $\langle a_1, b_1 \rangle = \langle a_2, b_2 \rangle$ holds if and only if $a_1 = a_2$ and $b_1$ is heq (heterogeneously equal) to $b_2$.
Sigma.eta theorem
: ∀ x : Σ a, β a, Sigma.mk x.1 x.2 = x
Full source 
@[simp]
theorem eta : ∀ x : Σa, β a, Sigma.mk x.1 x.2 = x
  | ⟨_, _⟩ => rfl
Eta Rule for Sigma Types
Informal description
For any dependent pair $x = (a, b)$ in the sigma type $\Sigma (a : \alpha), \beta(a)$, we have $(a, b) = x$.
Sigma.eq theorem
{α : Type*} {β : α → Type*} : ∀ {p₁ p₂ : Σ a, β a} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
Full source 
protected theorem eq {α : Type*} {β : α → Type*} : ∀ {p₁ p₂ : Σ a, β a} (h₁ : p₁.1 = p₂.1),
    (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
  | ⟨_, _⟩, _, rfl, rfl => rfl
Equality of Dependent Pairs via Component Equality
Informal description
For any type $\alpha$ and any family of types $\beta : \alpha \to \text{Type}^*$, given two dependent pairs $p_1 = \langle a_1, b_1 \rangle$ and $p_2 = \langle a_2, b_2 \rangle$ in $\Sigma a, \beta a$, if $a_1 = a_2$ and the transport of $b_1$ along this equality equals $b_2$, then $p_1 = p_2$.
Sigma.subtype_ext theorem
{β : Type*} {p : α → β → Prop} : ∀ {x₀ x₁ : Σ a, Subtype (p a)}, x₀.fst = x₁.fst → (x₀.snd : β) = x₁.snd → x₀ = x₁
Full source 
/-- A specialized ext lemma for equality of sigma types over an indexed subtype. -/
@[ext]
theorem subtype_ext {β : Type*} {p : α → β → Prop} :
    ∀ {x₀ x₁ : Σa, Subtype (p a)}, x₀.fst = x₁.fst → (x₀.snd : β) = x₁.snd → x₀ = x₁
  | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl, rfl => rfl
Extensionality for Sigma Types over Subtypes
Informal description
Let $α$ and $β$ be types, and let $p : α → β → \text{Prop}$ be a predicate. For any two dependent pairs $x₀, x₁$ in the sigma type $\Sigma (a : α), \{b : β \mid p(a, b)\}$, if the first components are equal ($x₀.1 = x₁.1$) and the second components (viewed as elements of $β$) are equal ($x₀.2 = x₁.2$), then $x₀ = x₁$.
Sigma.forall theorem
{p : (Σ a, β a) → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩
Full source 
theorem «forall» {p : (Σa, β a) → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩ :=
  ⟨fun h a b ↦ h ⟨a, b⟩, fun h ⟨a, b⟩ ↦ h a b⟩
Universal Quantification over Sigma Types
Informal description
For any predicate $p$ on a sigma type $\Sigma (a : \alpha), \beta(a)$, the universal quantification $\forall x, p(x)$ holds if and only if for every $a \in \alpha$ and every $b \in \beta(a)$, the predicate $p(\langle a, b \rangle)$ holds.
Sigma.exists theorem
{p : (Σ a, β a) → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩
Full source 
@[simp]
theorem «exists» {p : (Σa, β a) → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩ :=
  ⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩
Existence in Sigma Types is Component-wise
Informal description
For any predicate $p$ on a sigma type $\Sigma (a : \alpha), \beta(a)$, the statement $(\exists x, p(x))$ is equivalent to $(\exists (a : \alpha) (b : \beta(a)), p(\langle a, b \rangle))$.
Sigma.exists' theorem
{p : ∀ a, β a → Prop} : (∃ a b, p a b) ↔ ∃ x : Σ a, β a, p x.1 x.2
Full source 
lemma exists' {p : ∀ a, β a → Prop} : (∃ a b, p a b) ↔ ∃ x : Σ a, β a, p x.1 x.2 :=
  (Sigma.exists (p := fun x ↦ p x.1 x.2)).symm
Existence in Sigma Types via Components and Pairs
Informal description
For any predicate $p$ depending on elements $a \in \alpha$ and $b \in \beta(a)$, the statement that there exist $a$ and $b$ such that $p(a, b)$ holds is equivalent to the existence of a dependent pair $x = \langle a, b \rangle$ in the sigma type $\Sigma (a : \alpha), \beta(a)$ such that $p(x.1, x.2)$ holds, where $x.1$ and $x.2$ are the first and second components of $x$ respectively.
Sigma.forall' theorem
{p : ∀ a, β a → Prop} : (∀ a b, p a b) ↔ ∀ x : Σ a, β a, p x.1 x.2
Full source 
lemma forall' {p : ∀ a, β a → Prop} : (∀ a b, p a b) ↔ ∀ x : Σ a, β a, p x.1 x.2 :=
  (Sigma.forall (p := fun x ↦ p x.1 x.2)).symm
Universal Quantification over Sigma Types via Components
Informal description
For any predicate $p$ that takes an element $a$ of type $\alpha$ and an element $b$ of type $\beta(a)$, the universal quantification $\forall (a : \alpha) (b : \beta(a)), p(a, b)$ holds if and only if for every dependent pair $x = \langle a, b \rangle$ in the sigma type $\Sigma (a : \alpha), \beta(a)$, the predicate $p(x.1, x.2)$ holds, where $x.1$ and $x.2$ are the first and second components of $x$ respectively.
sigma_mk_injective theorem
{i : α} : Injective (@Sigma.mk α β i)
Full source 
theorem _root_.sigma_mk_injective {i : α} : Injective (@Sigma.mk α β i)
  | _, _, rfl => rfl
Injectivity of Dependent Pair Construction at Fixed Index
Informal description
For any fixed element $i$ of type $\alpha$, the function $\Sigma.\text{mk}$ that constructs a dependent pair $(i, b)$ from an element $b : \beta i$ is injective. That is, if $(i, b_1) = (i, b_2)$ as elements of $\Sigma a, \beta a$, then $b_1 = b_2$.
Sigma.fst_surjective theorem
[h : ∀ a, Nonempty (β a)] : Surjective (fst : (Σ a, β a) → α)
Full source 
theorem fst_surjective [h : ∀ a, Nonempty (β a)] : Surjective (fst : (Σ a, β a) → α) := fun a ↦
  let ⟨b⟩ := h a; ⟨⟨a, b⟩, rfl⟩
Surjectivity of the First Projection on Sigma Types with Nonempty Fibers
Informal description
For any type family $\beta : \alpha \to \text{Type}$ where $\beta(a)$ is nonempty for every $a \in \alpha$, the first projection $\text{fst} : (\Sigma a, \beta a) \to \alpha$ is surjective. That is, for every $a \in \alpha$, there exists some $b \in \beta(a)$ such that $\text{fst}((a, b)) = a$.
Sigma.fst_surjective_iff theorem
: Surjective (fst : (Σ a, β a) → α) ↔ ∀ a, Nonempty (β a)
Full source 
theorem fst_surjective_iff : SurjectiveSurjective (fst : (Σ a, β a) → α) ↔ ∀ a, Nonempty (β a) :=
  ⟨fun h a ↦ let ⟨x, hx⟩ := h a; hx ▸ ⟨x.2⟩, @fst_surjective _ _⟩
Surjectivity of First Projection on Sigma Types is Equivalent to Nonempty Fibers
Informal description
The first projection function $\text{fst} : (\Sigma a, \beta a) \to \alpha$ is surjective if and only if for every $a \in \alpha$, the type $\beta a$ is nonempty.
Sigma.fst_injective theorem
[h : ∀ a, Subsingleton (β a)] : Injective (fst : (Σ a, β a) → α)
Full source 
theorem fst_injective [h : ∀ a, Subsingleton (β a)] : Injective (fst : (Σ a, β a) → α) := by
  rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (rfl : a₁ = a₂)
  exact congr_arg (mk a₁) <| Subsingleton.elim _ _
Injectivity of First Projection for Sigma Types with Subsingleton Fibers
Informal description
For any type family $\beta : \alpha \to \text{Type}$ where each fiber $\beta(a)$ is a subsingleton (i.e., has at most one element), the first projection function $\text{fst} : (\Sigma a, \beta(a)) \to \alpha$ is injective.
Sigma.fst_injective_iff theorem
: Injective (fst : (Σ a, β a) → α) ↔ ∀ a, Subsingleton (β a)
Full source 
theorem fst_injective_iff : InjectiveInjective (fst : (Σ a, β a) → α) ↔ ∀ a, Subsingleton (β a) :=
  ⟨fun h _ ↦ ⟨fun _ _ ↦ sigma_mk_injective <| h rfl⟩, @fst_injective _ _⟩
Injectivity of First Projection for Sigma Types is Equivalent to Subsingleton Fibers
Informal description
The first projection function $\text{fst} : (\Sigma a, \beta(a)) \to \alpha$ is injective if and only if for every $a \in \alpha$, the type $\beta(a)$ is a subsingleton (i.e., has at most one element).
Sigma.map definition
(f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) (x : Sigma β₁) : Sigma β₂
Full source 
/-- Map the left and right components of a sigma -/
def map (f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) (x : Sigma β₁) : Sigma β₂ :=
  ⟨f₁ x.1, f₂ x.1 x.2⟩
Mapping of Sigma type components
Informal description
Given a function $f_1: \alpha_1 \to \alpha_2$ and a family of functions $f_2: \forall a, \beta_1(a) \to \beta_2(f_1(a))$, the function $\Sigma.\text{map}$ maps a dependent pair $\langle x, y \rangle \in \Sigma \beta_1$ to $\langle f_1(x), f_2(x)(y) \rangle \in \Sigma \beta_2$.
Sigma.map_mk theorem
(f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) (x : α₁) (y : β₁ x) : map f₁ f₂ ⟨x, y⟩ = ⟨f₁ x, f₂ x y⟩
Full source 
lemma map_mk (f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) (x : α₁) (y : β₁ x) :
    map f₁ f₂ ⟨x, y⟩ = ⟨f₁ x, f₂ x y⟩ := rfl
Mapping of Dependent Pair Components: $\Sigma.\text{map}(f_1, f_2)\langle x, y \rangle = \langle f_1(x), f_2(x)(y) \rangle$
Informal description
Given functions $f_1: \alpha_1 \to \alpha_2$ and $f_2: \forall a, \beta_1(a) \to \beta_2(f_1(a))$, and elements $x \in \alpha_1$ and $y \in \beta_1(x)$, the mapping of the dependent pair $\langle x, y \rangle$ under $\Sigma.\text{map}$ is equal to $\langle f_1(x), f_2(x)(y) \rangle$.
Function.Injective.sigma_map theorem
{f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)} (h₁ : Injective f₁) (h₂ : ∀ a, Injective (f₂ a)) : Injective (Sigma.map f₁ f₂)
Full source 
theorem Function.Injective.sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
    (h₁ : Injective f₁) (h₂ : ∀ a, Injective (f₂ a)) : Injective (Sigma.map f₁ f₂)
  | ⟨i, x⟩, ⟨j, y⟩, h => by
    obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1
    obtain rfl : x = y := h₂ i (sigma_mk_injective h)
    rfl
Injectivity of Sigma Mapping under Component-wise Injectivity
Informal description
Let $f_1: \alpha_1 \to \alpha_2$ be an injective function and $f_2: \forall a, \beta_1(a) \to \beta_2(f_1(a))$ be a family of injective functions. Then the mapping $\Sigma.\text{map}\, f_1\, f_2$ on dependent pairs, defined by $\langle x, y \rangle \mapsto \langle f_1(x), f_2(x)(y) \rangle$, is also injective.
Function.Injective.of_sigma_map theorem
{f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)} (h : Injective (Sigma.map f₁ f₂)) (a : α₁) : Injective (f₂ a)
Full source 
theorem Function.Injective.of_sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
    (h : Injective (Sigma.map f₁ f₂)) (a : α₁) : Injective (f₂ a) := fun x y hxy ↦
  sigma_mk_injective <| @h ⟨a, x⟩ ⟨a, y⟩ (Sigma.ext rfl (heq_of_eq hxy))
Injectivity of Component Functions from Injective Sigma Mapping
Informal description
Let $f_1: \alpha_1 \to \alpha_2$ and $f_2: \forall a, \beta_1(a) \to \beta_2(f_1(a))$ be functions. If the mapping $\Sigma.\text{map}\, f_1\, f_2$ is injective, then for any $a \in \alpha_1$, the function $f_2(a)$ is injective.
Function.Injective.sigma_map_iff theorem
{f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)} (h₁ : Injective f₁) : Injective (Sigma.map f₁ f₂) ↔ ∀ a, Injective (f₂ a)
Full source 
theorem Function.Injective.sigma_map_iff {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
    (h₁ : Injective f₁) : InjectiveInjective (Sigma.map f₁ f₂) ↔ ∀ a, Injective (f₂ a) :=
  ⟨fun h ↦ h.of_sigma_map, h₁.sigma_map⟩
Injectivity of Sigma Mapping is Equivalent to Component-wise Injectivity
Informal description
Let $f_1: \alpha_1 \to \alpha_2$ be an injective function and $f_2: \forall a, \beta_1(a) \to \beta_2(f_1(a))$ be a family of functions. Then the mapping $\Sigma.\mathrm{map}\, f_1\, f_2$ is injective if and only if for every $a \in \alpha_1$, the function $f_2(a)$ is injective.
Function.Surjective.sigma_map theorem
{f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)} (h₁ : Surjective f₁) (h₂ : ∀ a, Surjective (f₂ a)) : Surjective (Sigma.map f₁ f₂)
Full source 
theorem Function.Surjective.sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
    (h₁ : Surjective f₁) (h₂ : ∀ a, Surjective (f₂ a)) : Surjective (Sigma.map f₁ f₂) := by
  simp only [Surjective, Sigma.forall, h₁.forall]
  exact fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩
Surjectivity of Sigma Mapping under Componentwise Surjectivity
Informal description
Given functions $f_1: \alpha_1 \to \alpha_2$ and $f_2: \forall a, \beta_1(a) \to \beta_2(f_1(a))$, if $f_1$ is surjective and for every $a \in \alpha_1$, $f_2(a)$ is surjective, then the mapping $\Sigma.\text{map}\, f_1\, f_2$ on sigma types is surjective. That is, for any $\langle x, y \rangle \in \Sigma \beta_2$, there exists $\langle x', y' \rangle \in \Sigma \beta_1$ such that $\Sigma.\text{map}\, f_1\, f_2\, \langle x', y' \rangle = \langle x, y \rangle$.
Sigma.curry definition
{γ : ∀ a, β a → Type*} (f : ∀ x : Sigma β, γ x.1 x.2) (x : α) (y : β x) : γ x y
Full source 
/-- Interpret a function on `Σ x : α, β x` as a dependent function with two arguments.

This also exists as an `Equiv` as `Equiv.piCurry γ`. -/
def Sigma.curry {γ : ∀ a, β a → Type*} (f : ∀ x : Sigma β, γ x.1 x.2) (x : α) (y : β x) : γ x y :=
  f ⟨x, y⟩
Currying for sigma types
Informal description
Given a family of types $\gamma$ depending on $\alpha$ and $\beta$, the function `Sigma.curry` transforms a function $f$ defined on the sigma type $\Sigma x : \alpha, \beta x$ (i.e., taking pairs $\langle x, y\rangle$ where $x : \alpha$ and $y : \beta x$) into a dependent function with two arguments $x : \alpha$ and $y : \beta x$, producing a value in $\gamma x y$. Explicitly, for $f : \Pi (p : \Sigma x, \beta x), \gamma p.1 p.2$, the curried version satisfies $\mathrm{curry}(f)(x)(y) = f(\langle x, y\rangle)$.
Sigma.uncurry definition
{γ : ∀ a, β a → Type*} (f : ∀ (x) (y : β x), γ x y) (x : Sigma β) : γ x.1 x.2
Full source 
/-- Interpret a dependent function with two arguments as a function on `Σ x : α, β x`.

This also exists as an `Equiv` as `(Equiv.piCurry γ).symm`. -/
def Sigma.uncurry {γ : ∀ a, β a → Type*} (f : ∀ (x) (y : β x), γ x y) (x : Sigma β) : γ x.1 x.2 :=
  f x.1 x.2
Uncurrying of dependent functions on sigma types
Informal description
Given a family of types $\gamma$ depending on $\alpha$ and $\beta$, the function `Sigma.uncurry` transforms a dependent function $f$ that takes arguments $(x : \alpha)$ and $(y : \beta x)$ into a function that takes a pair $(x : \Sigma \beta)$ and returns $\gamma x.1 x.2$. More precisely, for any $f : \forall (x : \alpha) (y : \beta x), \gamma x y$ and any $x : \Sigma \beta$, `Sigma.uncurry f x` evaluates to $f x.1 x.2$.
Sigma.uncurry_curry theorem
{γ : ∀ a, β a → Type*} (f : ∀ x : Sigma β, γ x.1 x.2) : Sigma.uncurry (Sigma.curry f) = f
Full source 
@[simp]
theorem Sigma.uncurry_curry {γ : ∀ a, β a → Type*} (f : ∀ x : Sigma β, γ x.1 x.2) :
    Sigma.uncurry (Sigma.curry f) = f :=
  funext fun ⟨_, _⟩ ↦ rfl
Uncurry-Curry Identity for Sigma Types: $\mathrm{uncurry} \circ \mathrm{curry} = \mathrm{id}$
Informal description
For any family of types $\gamma$ depending on $\alpha$ and $\beta$, and any function $f$ defined on the sigma type $\Sigma x : \alpha, \beta x$ (i.e., $f$ takes pairs $\langle x, y\rangle$ where $x : \alpha$ and $y : \beta x$), the composition of uncurrying and currying $f$ returns $f$ itself. In other words, $\mathrm{uncurry}(\mathrm{curry}(f)) = f$.
Sigma.curry_uncurry theorem
{γ : ∀ a, β a → Type*} (f : ∀ (x) (y : β x), γ x y) : Sigma.curry (Sigma.uncurry f) = f
Full source 
@[simp]
theorem Sigma.curry_uncurry {γ : ∀ a, β a → Type*} (f : ∀ (x) (y : β x), γ x y) :
    Sigma.curry (Sigma.uncurry f) = f :=
  rfl
Curry-Uncurry Identity for Sigma Types
Informal description
For any family of types $\gamma$ depending on $\alpha$ and $\beta$, and any dependent function $f : \forall (x : \alpha) (y : \beta x), \gamma x y$, the composition of uncurrying followed by currying returns the original function, i.e., $\mathrm{curry}(\mathrm{uncurry}(f)) = f$.
Sigma.curry_update theorem
{γ : ∀ a, β a → Type*} [DecidableEq α] [∀ a, DecidableEq (β a)] (i : Σ a, β a) (f : (i : Σ a, β a) → γ i.1 i.2) (x : γ i.1 i.2) : Sigma.curry (Function.update f i x) = Function.update (Sigma.curry f) i.1 (Function.update (Sigma.curry f i.1) i.2 x)
Full source 
theorem Sigma.curry_update {γ : ∀ a, β a → Type*} [DecidableEq α] [∀ a, DecidableEq (β a)]
    (i : Σ a, β a) (f : (i : Σ a, β a) → γ i.1 i.2) (x : γ i.1 i.2) :
    Sigma.curry (Function.update f i x) =
      Function.update (Sigma.curry f) i.1 (Function.update (Sigma.curry f i.1) i.2 x) := by
  obtain ⟨ia, ib⟩ := i
  ext ja jb
  unfold Sigma.curry
  obtain rfl | ha := eq_or_ne ia ja
  · obtain rfl | hb := eq_or_ne ib jb
    · simp
    · simp only [update_self]
      rw [Function.update_of_ne (mt _ hb.symm), Function.update_of_ne hb.symm]
      rintro h
      injection h
  · rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]
    · exact ha.symm
    · exact ha.symm
Curry-Update Commutation for Sigma Types
Informal description
Let $\alpha$ be a type with decidable equality, $\beta : \alpha \to \text{Type}$ a family of types with decidable equality for each $\beta(a)$, and $\gamma : \Pi (a : \alpha), \beta(a) \to \text{Type}$ a family of types. Given a dependent function $f : \Pi (i : \Sigma a, \beta(a)), \gamma i.1 i.2$, an element $i = \langle a, b \rangle \in \Sigma a, \beta(a)$, and a value $x : \gamma a b$, the following equality holds: \[ \mathrm{curry}(\mathrm{update}(f, i, x)) = \mathrm{update}(\mathrm{curry}(f), a, \mathrm{update}(\mathrm{curry}(f)(a), b, x)) \] Here, $\mathrm{curry}$ converts a function on sigma types to a curried form, and $\mathrm{update}$ modifies a function at a given point.
Prod.toSigma definition
{α β} (p : α × β) : Σ _ : α, β
Full source 
/-- Convert a product type to a Σ-type. -/
def Prod.toSigma {α β} (p : α × β) : Σ_ : α, β :=
  ⟨p.1, p.2⟩
Conversion from product type to sigma type
Informal description
The function converts a product type $p : \alpha \times \beta$ to a sigma type $\Sigma\ (_ : \alpha), \beta$, where the first component of $p$ becomes the index and the second component becomes the value in the sigma type.
Prod.fst_comp_toSigma theorem
{α β} : Sigma.fst ∘ @Prod.toSigma α β = Prod.fst
Full source 
@[simp]
theorem Prod.fst_comp_toSigma {α β} : Sigma.fstSigma.fst ∘ @Prod.toSigma α β = Prod.fst :=
  rfl
First Projection Preserved Under Product-to-Sigma Conversion
Informal description
For any types $\alpha$ and $\beta$, the composition of the first projection function $\Sigma.\text{fst}$ with the conversion function $\text{Prod.toSigma}$ from the product type $\alpha \times \beta$ to the sigma type $\Sigma\ (_ : \alpha), \beta$ is equal to the first projection function $\text{Prod.fst}$ on the product type. In other words, $(\Sigma.\text{fst} \circ \text{Prod.toSigma}) = \text{Prod.fst}$.
Prod.fst_toSigma theorem
{α β} (x : α × β) : (Prod.toSigma x).fst = x.fst
Full source 
@[simp]
theorem Prod.fst_toSigma {α β} (x : α × β) : (Prod.toSigma x).fst = x.fst :=
  rfl
First Component Preservation in Sigma Conversion
Informal description
For any pair $x \in \alpha \times \beta$, the first component of the sigma type obtained by converting $x$ via `Prod.toSigma` equals the first component of $x$, i.e., $(\text{Prod.toSigma } x).\text{fst} = x.\text{fst}$.
Prod.snd_toSigma theorem
{α β} (x : α × β) : (Prod.toSigma x).snd = x.snd
Full source 
@[simp]
theorem Prod.snd_toSigma {α β} (x : α × β) : (Prod.toSigma x).snd = x.snd :=
  rfl
Second Component Preservation in Sigma Conversion: $(\text{toSigma } x).2 = x.2$
Informal description
For any pair $x = (a, b)$ in the product type $\alpha \times \beta$, the second component of the sigma type obtained by converting $x$ via `Prod.toSigma` equals the second component of $x$, i.e., $(\text{Prod.toSigma } x).\text{snd} = b$.
Prod.toSigma_mk theorem
{α β} (x : α) (y : β) : (x, y).toSigma = ⟨x, y⟩
Full source 
@[simp]
theorem Prod.toSigma_mk {α β} (x : α) (y : β) : (x, y).toSigma = ⟨x, y⟩ :=
  rfl
Conversion of Product Pair to Sigma Pair: $(x, y).toSigma = \langle x, y \rangle$
Informal description
For any elements $x \in \alpha$ and $y \in \beta$, the conversion of the pair $(x, y)$ to a sigma type via `Prod.toSigma` yields the dependent pair $\langle x, y \rangle$.
PSigma.elim definition
{γ} (f : ∀ a, β a → γ) (a : PSigma β) : γ
Full source 
/-- Nondependent eliminator for `PSigma`. -/
def elim {γ} (f : ∀ a, β a → γ) (a : PSigma β) : γ :=
  PSigma.casesOn a f
Nondependent eliminator for dependent pairs
Informal description
The function `PSigma.elim` takes a function `f` that maps each `a : α` and `b : β a` to an element of `γ`, and a dependent pair `⟨a, b⟩ : PSigma β`, and returns `f a b`. This serves as a nondependent eliminator for `PSigma`, allowing the extraction of values from a dependent pair without maintaining the dependency structure.
PSigma.elim_val theorem
{γ} (f : ∀ a, β a → γ) (a b) : PSigma.elim f ⟨a, b⟩ = f a b
Full source 
@[simp]
theorem elim_val {γ} (f : ∀ a, β a → γ) (a b) : PSigma.elim f ⟨a, b⟩ = f a b :=
  rfl
Eliminator Computation for Dependent Pairs: $\text{PSigma.elim}\, f\, \langle a, b \rangle = f\, a\, b$
Informal description
For any type $\gamma$, function $f \colon \prod_{a \colon \alpha} \beta(a) \to \gamma$, and elements $a \colon \alpha$ and $b \colon \beta(a)$, the application of the eliminator `PSigma.elim` to $f$ and the dependent pair $\langle a, b \rangle$ is equal to $f$ applied to $a$ and $b$, i.e., \[ \text{PSigma.elim}\, f\, \langle a, b \rangle = f\, a\, b. \]
PSigma.instInhabitedOfDefault_mathlib instance
[Inhabited α] [Inhabited (β default)] : Inhabited (PSigma β)
Full source 
instance [Inhabited α] [Inhabited (β default)] : Inhabited (PSigma β) :=
  ⟨⟨default, default⟩⟩
Inhabitedness of Sigma Types with Default Values
Informal description
For any type $\alpha$ with a default element and any dependent type family $\beta : \alpha \to \text{Type*}$ where $\beta(\text{default})$ is inhabited, the sigma type $\Sigma a : \alpha, \beta a$ is inhabited.
PSigma.decidableEq instance
[h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq (β a)] : DecidableEq (PSigma β)
Full source 
instance decidableEq [h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq (β a)] : DecidableEq (PSigma β)
  | ⟨a₁, b₁⟩, ⟨a₂, b₂⟩ =>
    match a₁, b₁, a₂, b₂, h₁ a₁ a₂ with
    | _, b₁, _, b₂, isTrue (Eq.refl _) =>
      match b₁, b₂, h₂ _ b₁ b₂ with
      | _, _, isTrue (Eq.refl _) => isTrue rfl
      | _, _, isFalse n => isFalse fun h ↦ PSigma.noConfusion h fun _ e₂ ↦ n <| eq_of_heq e₂
    | _, _, _, _, isFalse n => isFalse fun h ↦ PSigma.noConfusion h fun e₁ _ ↦ n e₁
Decidable Equality for Dependent Pairs
Informal description
Given a type family $\beta : \alpha \to \text{Type}$ and decidable equality on $\alpha$ and on each $\beta a$, there is a decidable equality on the dependent pair type $\Sigma' a, \beta a$.
PSigma.mk.inj_iff theorem
{a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} : @PSigma.mk α β a₁ b₁ = @PSigma.mk α β a₂ b₂ ↔ a₁ = a₂ ∧ HEq b₁ b₂
Full source 
theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
    @PSigma.mk α β a₁ b₁ = @PSigma.mk α β a₂ b₂ ↔ a₁ = a₂ ∧ HEq b₁ b₂ :=
  (Iff.intro PSigma.mk.inj) fun ⟨h₁, h₂⟩ ↦
    match a₁, a₂, b₁, b₂, h₁, h₂ with
    | _, _, _, _, Eq.refl _, HEq.refl _ => rfl
Equality Condition for Dependent Pairs: $\langle a_1, b_1 \rangle = \langle a_2, b_2 \rangle \leftrightarrow a_1 = a_2 \land b_1 \equiv b_2$
Informal description
For any elements $a_1, a_2 : \alpha$ and $b_1 : \beta(a_1)$, $b_2 : \beta(a_2)$, the equality $\langle a_1, b_1 \rangle = \langle a_2, b_2 \rangle$ in the sigma type $\Sigma' a, \beta a$ holds if and only if $a_1 = a_2$ and $b_1$ is heterogeneously equal to $b_2$.
PSigma.forall theorem
{p : (Σ' a, β a) → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩
Full source 
theorem «forall» {p : (Σ'a, β a) → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩ :=
  ⟨fun h a b ↦ h ⟨a, b⟩, fun h ⟨a, b⟩ ↦ h a b⟩
Universal Quantification over Dependent Pairs
Informal description
For any predicate $p$ on dependent pairs of the form $\Sigma' a, \beta a$, the universal quantification $\forall x, p(x)$ holds if and only if for every $a$ and every $b : \beta a$, the predicate $p(\langle a, b \rangle)$ holds.
PSigma.exists theorem
{p : (Σ' a, β a) → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩
Full source 
@[simp] lemma «exists» {p : (Σ' a, β a) → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩ :=
  ⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩
Existence in Dependent Pair Types
Informal description
For any predicate $p$ on a dependent pair type $\Sigma' a, \beta a$, the existence of an element $x$ satisfying $p(x)$ is equivalent to the existence of an element $a$ of type $\alpha$ and an element $b$ of type $\beta a$ such that $p(\langle a, b \rangle)$ holds. In other words: $$ (\exists x, p(x)) \leftrightarrow (\exists a\, b, p(\langle a, b \rangle)) $$
PSigma.subtype_ext theorem
{β : Sort*} {p : α → β → Prop} : ∀ {x₀ x₁ : Σ' a, Subtype (p a)}, x₀.fst = x₁.fst → (x₀.snd : β) = x₁.snd → x₀ = x₁
Full source 
/-- A specialized ext lemma for equality of `PSigma` types over an indexed subtype. -/
@[ext]
theorem subtype_ext {β : Sort*} {p : α → β → Prop} :
    ∀ {x₀ x₁ : Σ'a, Subtype (p a)}, x₀.fst = x₁.fst → (x₀.snd : β) = x₁.snd → x₀ = x₁
  | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl, rfl => rfl
Extensionality for Dependent Pairs over a Subtype
Informal description
For any type $β$ and predicate $p : α → β → \text{Prop}$, given two dependent pairs $x₀, x₁ : \Sigma' a, \{b : β \mid p\ a\ b\}$ (where $\Sigma'$ denotes a sigma type and $\{b : β \mid p\ a\ b\}$ is the subtype of $β$ satisfying $p\ a$), if their first components are equal ($x₀.\text{fst} = x₁.\text{fst}$) and their second components (viewed as elements of $β$) are equal ($x₀.\text{snd} = x₁.\text{snd}$), then $x₀ = x₁$.
PSigma.map definition
(f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) : PSigma β₁ → PSigma β₂
Full source 
/-- Map the left and right components of a sigma -/
def map (f₁ : α₁ → α₂) (f₂ : ∀ a, β₁ a → β₂ (f₁ a)) : PSigma β₁ → PSigma β₂
  | ⟨a, b⟩ => ⟨f₁ a, f₂ a b⟩
Mapping of dependent pairs
Informal description
Given a function $f_1: \alpha_1 \to \alpha_2$ and a family of functions $f_2(a): \beta_1(a) \to \beta_2(f_1(a))$ for each $a \in \alpha_1$, the function maps a dependent pair $\langle a, b \rangle$ in $\Sigma'_{a:\alpha_1} \beta_1(a)$ to the dependent pair $\langle f_1(a), f_2(a)(b) \rangle$ in $\Sigma'_{a:\alpha_2} \beta_2(a)$.