exists_pair_ne
theorem exists_pair_ne : ∀ (α : Type u_3) [inst : Nontrivial α], ∃ x y, x ≠ y
This theorem, `exists_pair_ne`, asserts that for every type `α` that is nontrivial (i.e., it has at least two distinct elements), there exist two elements `x` and `y` such that `x` is not equal to `y`. In other words, in any nontrivial type, you can always find a pair of distinct elements.
More concisely: For any nontrivial type `α`, there exist `x` and `y` in `α` such that `x ≠ y`.
|
false_of_nontrivial_of_subsingleton
theorem false_of_nontrivial_of_subsingleton : ∀ (α : Type u_3) [inst : Nontrivial α] [inst : Subsingleton α], False
This theorem, `false_of_nontrivial_of_subsingleton`, states that for any type `α`, if `α` is both nontrivial and a subsingleton, then we can derive a contradiction (i.e., `False`). A nontrivial type is one that has at least two distinct elements, while a subsingleton type is one that has at most one element. Therefore, no type can be both nontrivial and a subsingleton at the same time.
More concisely: If a type `α` is both nontrivial (has at least two distinct elements) and a subsingleton (has at most one element), then we obtain a contradiction.
|
exists_ne
theorem exists_ne : ∀ {α : Type u_1} [inst : Nontrivial α] (x : α), ∃ y, y ≠ x
This theorem states that for all types `α` that are nontrivial (i.e., there are at least two distinct elements in `α`), given any element `x` from `α`, there exists another element `y` in `α` such that `y` is not equal to `x`. In other words, in any nontrivial type, for every element, there is always another distinct element.
More concisely: In any nontrivial type, every element has a distinct element.
|
subsingleton_or_nontrivial
theorem subsingleton_or_nontrivial : ∀ (α : Type u_3), Subsingleton α ∨ Nontrivial α
This theorem states that for any type 'α', it is either a subsingleton or nontrivial. In other words, for every type, it either contains at most one element (subsingleton), or it contains at least two distinct elements (nontrivial).
More concisely: Every type is either a subsingleton (has at most one element) or nontrivial (has at least two distinct elements).
|
Decidable.exists_ne
theorem Decidable.exists_ne : ∀ {α : Type u_1} [inst : Nontrivial α] [inst : DecidableEq α] (x : α), ∃ y, y ≠ x := by
sorry
This theorem, `Decidable.exists_ne`, asserts that for any type `α` that is nontrivial (i.e., has at least two distinct elements) and has decidable equality (meaning, given any two elements of `α`, it is decidable whether or not they are equal), if we have an element `x` of `α`, there exists another element `y` in `α` which is not equal to `x`. In essence, this theorem guarantees that in such a type `α`, for any given element, there is always another distinct element.
More concisely: For any nontrivial type `α` with decidable equality, there exists a distinct element in `α` for every given element.
|
nontrivial_iff_exists_ne
theorem nontrivial_iff_exists_ne : ∀ {α : Type u_1} (x : α), Nontrivial α ↔ ∃ y, y ≠ x
This theorem states that for any type `α` and any element `x` of that type, `α` is nontrivial if and only if there exists an element `y` in `α` which is not equal to `x`. In other words, a type is considered nontrivial when there's at least one instance of that type that's distinct from a given instance.
More concisely: A type `α` is nontrivial if and only if it has at least two distinct elements.
|
Nontrivial.exists_pair_ne
theorem Nontrivial.exists_pair_ne : ∀ {α : Type u_3} [self : Nontrivial α], ∃ x y, x ≠ y
This theorem states that for any nontrivial type `α`, there exists a pair of elements `x` and `y` such that `x` is not equal to `y`. In other words, it ensures that in any non-empty and non-singleton type, you can always find two different elements.
More concisely: For any non-empty and non-singleton type `α`, there exist `x` and `y` in `α` such that `x ≠ y`.
|
nontrivial_iff
theorem nontrivial_iff : ∀ {α : Type u_1}, Nontrivial α ↔ ∃ x y, x ≠ y
This theorem states that a type `α` is nontrivial if and only if there exist `x` and `y` of type `α` such that `x` is not equal to `y`. Here, 'nontrivial' is a property of a type; a type is nontrivial if it has at least two distinct elements. Specifically, the theorem establishes the equivalence between the nontriviality of a type and the existence of a pair of unequal elements in that type.
More concisely: A type `α` is nontrivial if and only if it has at least two distinct elements, which can be expressed as the existence of `x` and `y` in `α` such that `x ≠ y`.
|
subsingleton_iff
theorem subsingleton_iff : ∀ {α : Type u_1}, Subsingleton α ↔ ∀ (x y : α), x = y
This theorem, `subsingleton_iff`, states that for any type `α`, `α` is a subsingleton if and only if for any two elements `x` and `y` of `α`, `x` equals `y`. In other words, a type is a subsingleton when all its elements are equal. Subsingletons in Lean 4 are types that have at most one element.
More concisely: A type `α` is a subsingleton if and only if every two elements `x` and `y` in `α` are equal, i.e., `x = y`.
|
not_subsingleton
theorem not_subsingleton : ∀ (α : Type u_3) [inst : Nontrivial α], ¬Subsingleton α
This theorem states that for any type `α` that is non-trivial - that is, it contains at least two distinct elements - `α` cannot be a subsingleton. In other words, in a non-trivial type, there exists at least a pair of distinct elements, hence it cannot be a subsingleton (a type with at most one element).
More concisely: A non-trivial type cannot be a subsingleton. (In other words, a type with at least two distinct elements is not a subsingleton.)
|
nontrivial_of_ne
theorem nontrivial_of_ne : ∀ {α : Type u_1} (x y : α), x ≠ y → Nontrivial α
This theorem states that for any type `α` and any two elements `x` and `y` of that type, if `x` is not equal to `y`, then `α` is nontrivial. In mathematical terms, a type is nontrivial if it contains at least two distinct elements, thus if there exists two elements that are not equal, this directly confirms the nontriviality of the type.
More concisely: If `α` has distinct elements `x` and `y`, then `α` is nontrivial.
|
not_nontrivial_iff_subsingleton
theorem not_nontrivial_iff_subsingleton : ∀ {α : Type u_1}, ¬Nontrivial α ↔ Subsingleton α
This theorem states that for any type `α`, `α` is not nontrivial if and only if `α` is a subsingleton. In other words, for a given type, there is no pair of distinct elements (i.e., it is not nontrivial) if and only if every pair of elements in the type are identical (i.e., it is a subsingleton). This theorem bridges the concept of nontriviality and subsingularity in type theory.
More concisely: A type `α` is not nontrivial if and only if it is a subsingleton.
|
not_nontrivial
theorem not_nontrivial : ∀ (α : Type u_3) [inst : Subsingleton α], ¬Nontrivial α
This theorem states that for every type `α`, if `α` is a subsingleton, then `α` is not nontrivial. In other words, there cannot exist a nontrivial structure on a type which is a subsingleton. Recall that a type is a subsingleton when it has at most one element, and a type is nontrivial when there are at least two distinct elements in it.
More concisely: A subsingleton type, having at most one element, cannot be nontrivial, which requires the presence of at least two distinct elements.
|
Function.Surjective.nontrivial
theorem Function.Surjective.nontrivial :
∀ {α : Type u_1} {β : Type u_2} [inst : Nontrivial β] {f : α → β}, Function.Surjective f → Nontrivial α
The theorem `Function.Surjective.nontrivial` states that for any two types `α` and `β`, given that `β` is nontrivial (i.e., there are at least two distinct elements in `β`), and given a function `f` from `α` to `β` that is surjective (i.e., for every element `b` in `β`, there is some element `a` in `α` such that `f(a)` equals `b`), then `α` is also nontrivial. In other words, if we have a surjective function from `α` to a nontrivial type `β`, then `α` must be nontrivial as well.
More concisely: If `β` is a nontrivial type and `f` is a surjective function from `α` to `β`, then `α` is also a nontrivial type.
|