Sigma.eta
theorem Sigma.eta : ∀ {α : Type u_1} {β : α → Type u_4} (x : (a : α) × β a), ⟨x.fst, x.snd⟩ = x
This theorem, named `Sigma.eta`, states that for all types `α` and a type family `β` dependent on `α`, any dependent pair `(a : α) × β a` is equal to the pair constructed by explicitly taking its first and second components. In other words, if you take a dependent pair and then reassemble it using its own components, you get the original pair back.
More concisely: For all types `α` and type families `β` dependent on `α`, the dependent pair operation is equal to the projection function composition on `α × β`.
|
Sigma.forall
theorem Sigma.forall :
∀ {α : Type u_1} {β : α → Type u_4} {p : (a : α) × β a → Prop},
(∀ (x : (a : α) × β a), p x) ↔ ∀ (a : α) (b : β a), p ⟨a, b⟩
This theorem, `Sigma.forall`, defines an equivalence in predicate logic over dependent pair types in Lean 4. More specifically, for any type `α`, a type dependency `β : α → Type`, and a predicate `p` applicable to such dependent pairs, it asserts that the predicate holding for all elements of the dependent pair type is equivalent to the predicate holding for all possible first-and-second-element combinations. In other words, it's saying that if you can affirm a property for every individual element in a type-dependent pair, then you can affirm it for the whole pair and vice versa.
More concisely: For any type `α`, dependent type `β : α → Type`, and predicate `p` on dependent pairs `(a, b) : α × β a`, `Sigma.forall` asserts that `∀ (a : α), p a b ↔ ∀ (x, y : α × β), p x y`.
|
Function.eq_of_sigmaMk_comp
theorem Function.eq_of_sigmaMk_comp :
∀ {α : Type u_1} {β : α → Type u_4} {γ : Type u_7} [inst : Nonempty γ] {a b : α} {f : γ → β a} {g : γ → β b},
Sigma.mk a ∘ f = Sigma.mk b ∘ g → a = b ∧ HEq f g
This theorem, `Function.eq_of_sigmaMk_comp`, states that for any nonempty type `γ`, and functions `f : γ → β a` and `g : γ → β b`, if the composition of `Sigma.mk a` and `f` equals the composition of `Sigma.mk b` and `g`, then `a` must be equal to `b` and `f` is heterogeneously equal to `g`. In other words, if two function compositions that create sigma types are equal, then their inputs must be the same and the functions used must be heterogeneously equal.
More concisely: If `Sigma.mk a` composited with `f` equals `Sigma.mk b` composited with `g` for nonempty types `γ`, functions `f : γ → β a` and `g : γ → β b`, then `a = b` and `f` is heterogeneously equal to `g`.
|
Sigma.mk.inj_iff
theorem Sigma.mk.inj_iff :
∀ {α : Type u_1} {β : α → Type u_4} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂},
⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂
This theorem states that for any two pairs (a₁, b₁) and (a₂, b₂), where a₁ and a₂ are of some type α, and b₁ and b₂ are of type dependent on a₁ and a₂ respectively, these pairs are equal if and only if a₁ is equal to a₂ and b₁ is provably equal to b₂ under heterogeneous equality (HEq). In other words, two pairs are equal if their corresponding elements are equal, with the second element's equality being judged in the context of the first element's value.
More concisely: For any type α and pairs (a₁, b₁) and (a₂, b₂) with a₁, a₂ of type α and b₁, b₂ dependent on a₁, a₁ = a₂ and HEq (b₁) (b₂) are equivalent.
|
Mathlib.Data.Sigma.Basic._auxLemma.1
theorem Mathlib.Data.Sigma.Basic._auxLemma.1 :
∀ {α : Type u_1} {β : α → Type u_4} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂},
(⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) = (a₁ = a₂ ∧ HEq b₁ b₂)
This theorem, `Mathlib.Data.Sigma.Basic._auxLemma.1`, states that for all types `α` and `β`, where `β` is a function of `α`, and for all `a₁`, `a₂` of type `α` and `b₁`, `b₂` of type `β`, a pair with first element `a₁` and second element `b₁` is equal to a pair with first element `a₂` and second element `b₂` if and only if `a₁` is equal to `a₂` and `b₁` is heterogeneously equal (`HEq`) to `b₂`. In other words, two pairs are the same if and only if their corresponding elements are the same, with the second element's equality being type-dependent on the first.
More concisely: For all types `α` and `β`, and for all `a₁ a₂ : α` and `b₁ b₂ : β(α)`, the pairs `(a₁, b₁)` and `(a₂, b₂)` are equal if and only if `a₁ = a₂` and `b₁` is heterogeneously equal to `b₂`.
|
Sigma.exists
theorem Sigma.exists : ∀ {α : Type u_1} {β : α → Type u_4} {p : (a : α) × β a → Prop}, (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩
This theorem, `Sigma.exists`, states that for any types `α` and `β` (with `β` being a type dependent on `α`), and any property `p` that can be applied to a pair consisting of a value of type `α` and a value of type `β a` (where `a` is a value of type `α`), there exists a value `x` such that the property `p` holds for `x` if and only if there exist values `a` and `b` such that `p` holds for the pair (`a`, `b`). Essentially, this theorem states that an existential quantification over a dependent pair type is equivalent to an existential quantification over the components of the pair.
More concisely: For any types `α` and `β`, and any predicate `p` on `α × β`, the existence of `x : α × β` such that `p(x)` holds is equivalent to the existence of `a : α` and `b : β a` such that `p(a, b)` holds.
|
Mathlib.Data.Sigma.Basic._auxLemma.3
theorem Mathlib.Data.Sigma.Basic._auxLemma.3 :
∀ {α : Type u_1} {β : α → Type u_4} {p : (a : α) × β a → Prop},
(∀ (x : (a : α) × β a), p x) = ∀ (a : α) (b : β a), p ⟨a, b⟩
This theorem, `Mathlib.Data.Sigma.Basic._auxLemma.3`, asserts that for any type `α`, function `β` from `α` to another type, and predicate `p` over pairs `(a : α) × β a`, the statement "the predicate `p` holds true for all pairs `(x : α) × β x`" is equivalent to "for every `a : α` and `b : β a`, the predicate `p` holds for the pair composed of `a` and `b`". In other words, it's stating that quantification over the elements of a dependent pair is the same as separate quantification over each component of the pair.
More concisely: For any type `α`, function `β : α → *`, and predicate `p : ∀ (a : α), β a → Prop`, the statements `∀ (x : α) (b : β x), p x b` and `∀ a, ∀ b, p a b` are equivalent.
|
PSigma.subtype_ext
theorem PSigma.subtype_ext :
∀ {α : Sort u_1} {β : Sort u_3} {p : α → β → Prop} {x₀ x₁ : (a : α) ×' Subtype (p a)},
x₀.fst = x₁.fst → ↑x₀.snd = ↑x₁.snd → x₀ = x₁
This theorem states that for any types `α` and `β` and any property `p` that applies to an element of `α` and `β`, if we have two `PSigma` types, `x₀` and `x₁`, over an indexed subtype defined by `p`, then `x₀` and `x₁` are equal if and only if their first elements (`x₀.fst` and `x₁.fst`) are equal and the elements they index (`x₀.snd` and `x₁.snd`) are also equal when coerced to the same type. This theorem is a specialized extension lemma for the equality of `PSigma` types over an indexed subtype.
More concisely: For any types `α`, `β`, and property `p`, if `PSigma x i α β p x₀ = PSigma x i α β p x₁`, then `x₀ = x₁` if and only if `x₀.fst = x₁.fst` and `(coe to α x₀.snd) = (coe to α x₁.snd)`.
|
Sigma.subtype_ext
theorem Sigma.subtype_ext :
∀ {α : Type u_1} {β : Type u_7} {p : α → β → Prop} {x₀ x₁ : (a : α) × Subtype (p a)},
x₀.fst = x₁.fst → ↑x₀.snd = ↑x₁.snd → x₀ = x₁
This theorem, `Sigma.subtype_ext`, states that for any two sigma types `x₀` and `x₁`, that are formed over an indexed subtype, if the first elements (`fst`) of `x₀` and `x₁` are equal, and the underlying value (`↑`) of the second elements (`snd`) of both are equal, then `x₀` and `x₁` are themselves equal. Here, `α` and `β` are arbitrary types, and `p` is a property relating an element of type `α` to an element of type `β`. The sigma types `x₀` and `x₁` are tuples consisting of an `α` and a subtype of `β` satisfying property `p`.
More concisely: Given sigma types `(α, β × σ₀)` and `(α, β × σ₁)` formed over indices satisfying `σ₀ = σ₁`, `α × fst x₀ = α × fst x₁`, and `↑snd x₀ = ↑snd x₁`, then `x₀ = x₁`.
|
Mathlib.Data.Sigma.Basic._auxLemma.4
theorem Mathlib.Data.Sigma.Basic._auxLemma.4 :
∀ {α : Type u_1} {β : α → Type u_4} {p : (a : α) × β a → Prop}, (∃ x, p x) = ∃ a b, p ⟨a, b⟩
This theorem, `Mathlib.Data.Sigma.Basic._auxLemma.4`, states that for any type `α`, any type function `β` that maps an instance of `α` to a type, and any property `p` that applies to a pair consisting of an instance of `α` and an instance of `β a`, the statement "There exists an `x` such that property `p` holds for `x`" is equivalent to the statement "There exists an `a` and `b` such that property `p` holds for the pair whose first element is `a` and second element is `b`." Here, `a` is an instance of `α` and `b` is an instance of `β a`.
More concisely: For any type `α`, type function `β`, property `p`, and instances `a : α` and `b : β a`, the existence of an `x` such that `p(x)` holds is equivalent to the existence of `a` and `b` such that `p(a, b)` holds.
|
Function.Injective.sigma_map
theorem Function.Injective.sigma_map :
∀ {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} {f₁ : α₁ → α₂}
{f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)},
Function.Injective f₁ → (∀ (a : α₁), Function.Injective (f₂ a)) → Function.Injective (Sigma.map f₁ f₂)
The theorem `Function.Injective.sigma_map` states that for any two types `α₁` and `α₂`, and two type-dependent functions `β₁ : α₁ → Type` and `β₂ : α₂ → Type`, if we have functions `f₁ : α₁ → α₂` and `f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)` such that `f₁` is injective and for every `a` in `α₁`, `f₂ a` is also injective, then the function `Sigma.map f₁ f₂`, which maps the left and right components of a sigma type, is also injective. In mathematical terms, injectivity of component functions implies the injectivity of the resulting function after a sigma mapping.
More concisely: If `f₁ : α₁ → α₂` is injective and for all `a` in `α₁`, the function `β₁ a → β₂ (f₁ a)` given by `f₂` is also injective, then the function `Sigma.map f₁ f₂` on sigma types is injective.
|
Sigma.ext_iff
theorem Sigma.ext_iff :
∀ {α : Type u_1} {β : α → Type u_4} {x₀ x₁ : Sigma β}, x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ HEq x₀.snd x₁.snd
The theorem `Sigma.ext_iff` states that for any types `α` and `β`, and any two elements `x₀` and `x₁` of the dependent pair type `Sigma β`, `x₀` is equal to `x₁` if and only if the first component of `x₀` is equal to the first component of `x₁` and the second component of `x₀` is heterogeneously equal to the second component of `x₁`. Here, `HEq` denotes heterogeneous equality, which allows for equality between elements of possibly different types.
More concisely: For any types `α` and `β`, and dependent pair elements `(x\_0, h\_0)` and `(x\_1, h\_1)` of `Sigma β`, `x\_0 = x\_1` if and only if `x\_0.1 = x\_1.1` and `hEq h\_0 h\_1`.
|
sigma_mk_injective
theorem sigma_mk_injective : ∀ {α : Type u_1} {β : α → Type u_4} {i : α}, Function.Injective (Sigma.mk i)
The theorem `sigma_mk_injective` states that for any type `α`, for any type function `β` that maps from `α`, and for any instance `i` of `α`, the mapping function `Sigma.mk i` is injective. In other words, given two elements from the type `β i`, if they are mapped to the same value by the function `Sigma.mk i`, then they must have been the same element to begin with.
More concisely: For any type `α` and type function `β : α → Type`, the function `Sigma.mk : ∀ i : α, β i → Σ i, x ∈ β i ↦ Sigma.mk i x = Sigma.mk i y ↔ x = y` is a function identity.
|