Subsingleton.eq_zero
theorem Subsingleton.eq_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Subsingleton α] (a : α), a = 0
This theorem, `Subsingleton.eq_zero`, states that for any type `α` which has a zero element (as per the `Zero` typeclass) and is a subsingleton (meaning it has at most one distinct element, as per the `Subsingleton` typeclass), any element `a` of type `α` equals zero. Essentially, in a subsingleton type that has a zero element, all elements are equal to zero.
More concisely: In a subsingleton type with a zero element, all elements equal zero.
|
Function.Injective.nontrivial
theorem Function.Injective.nontrivial :
∀ {α : Type u_1} {β : Type u_2} [inst : Nontrivial α] {f : α → β}, Function.Injective f → Nontrivial β
This theorem states that if there exists a function `f` from type `α` to type `β` that is injective, which means each input maps to a unique output in `β`, and `α` is nontrivial (that is, `α` contains at least two distinct elements), then `β` is also nontrivial. In other words, if we have a nontrivial type `α` and an injective function from `α` to `β`, there must be at least two distinct elements in `β` as well. The purpose of this theorem is to transfer the property of nontriviality from one type to another via an injective function.
More concisely: If `α` is a nontrivial type and `f : α → β` is an injective function, then `β` is also a nontrivial type.
|
Pi.nontrivial_at
theorem Pi.nontrivial_at :
∀ {I : Type u_3} {f : I → Type u_4} (i' : I) [inst : ∀ (i : I), Nonempty (f i)] [inst : Nontrivial (f i')],
Nontrivial ((i : I) → f i)
This theorem states that for any index type `I` and a function `f` that maps indices to types, if there exists a specific index `i'` such that the type `f i'` is nontrivial (i.e., it contains at least two distinct elements), and every type `f i` for all `i` in `I` is nonempty (i.e., it contains at least one element), then the pi type `(i : I) → f i`, which is a generalization of functions from `I` to types defined by `f`, is also nontrivial. Here, a type is called nonempty if it contains at least one element, and nontrivial if it contains at least two distinct elements.
More concisely: If for every index `i` in an index type `I`, the type `f i` is nonempty, and there exists an index `i'` such that `f i'` is nontrivial, then the type `(i : I) → f i` is also nontrivial.
|
Function.Injective.exists_ne
theorem Function.Injective.exists_ne :
∀ {α : Type u_1} {β : Type u_2} [inst : Nontrivial α] {f : α → β}, Function.Injective f → ∀ (y : β), ∃ x, f x ≠ y
This theorem states that for any injective function `f` mapping from a nontrivial type `α` to any type `β`, and for any value `y` of type `β`, there exists an element `x` in the domain of `f` such that `f(x)` does not equal `y`. In other words, no matter what value `y` you pick from the codomain, you can always find an element `x` in the domain which `f` maps to a different value. The nontriviality condition on `α` ensures that there are at least two distinct elements in `α`.
More concisely: For any injective function `f` from a non-empty type `α` to type `β`, there exists an `x` in `α` such that `f(x) ≠ y` for all `y` in `β`.
|