Set.Subsingleton.eq_empty_or_singleton
theorem Set.Subsingleton.eq_empty_or_singleton : ∀ {α : Type u} {s : Set α}, s.Subsingleton → s = ∅ ∨ ∃ x, s = {x} := by
sorry
The theorem `Set.Subsingleton.eq_empty_or_singleton` states that for any type `α` and any set `s` of type `α`, if `s` is a subsingleton set (i.e., it has at most one element), then `s` must either be equal to the empty set or there exists an element `x` such that `s` is the singleton set containing only `x`.
More concisely: If `α` is a type and `s : Set α` is a subsingleton set, then `s = ∅` or `s = {x : α}`.
|
Set.Nontrivial.coe_sort
theorem Set.Nontrivial.coe_sort : ∀ {α : Type u} {s : Set α}, s.Nontrivial → Nontrivial ↑s
The theorem `Set.Nontrivial.coe_sort` states that for all types `α` and for any set `s` of type `α`, if `s` is a nontrivial set, then the type that `s` is coerced to is a nontrivial type. In other words, if a set `s` has more than one distinct element, then the type obtained by considering `s` as a type also has more than one distinct element.
More concisely: If `s` is a nontrivial set of type `α`, then the type `{x : α | x ∈ s}` is also a nontrivial type.
|
Set.subsingleton_singleton
theorem Set.subsingleton_singleton : ∀ {α : Type u} {a : α}, {a}.Subsingleton
The theorem `Set.subsingleton_singleton` states that for any type `α` and any element `a` of that type, the set containing only `a` is a `Subsingleton` set. In other words, a set that contains a single element is a `Subsingleton` set, meaning it has at most one element, which in this case is `a`.
More concisely: For any type `α` and element `a` in `α`, the singleton set `{a}` is a `Subsingleton` set.
|
Set.Nontrivial.exists_ne
theorem Set.Nontrivial.exists_ne : ∀ {α : Type u} {s : Set α}, s.Nontrivial → ∀ (z : α), ∃ x ∈ s, x ≠ z
This theorem states that for any type `α` and any set `s` of that type, if the set `s` is nontrivial (that is, it has at least two distinct elements), then for any element `z` of the type `α`, there exists an element `x` in the set `s` such that `x` is not equal to `z`. In other words, in any nontrivial set, we can always find an element which is different from a given element of the same type.
More concisely: If `α` is a type and `s` is a non-empty set of `α`, then for all `z` in `α`, there exists `x` in `s` such that `x ≠ z`.
|
Set.Nontrivial.mono
theorem Set.Nontrivial.mono : ∀ {α : Type u} {s t : Set α}, s.Nontrivial → s ⊆ t → t.Nontrivial
The theorem `Set.Nontrivial.mono` states that for any type `α` and for any sets `s` and `t` of type `α`, if `s` is a nontrivial set and `s` is a subset of `t`, then `t` is also a nontrivial set. Here, a set is considered nontrivial if it contains at least two distinct elements. In other words, the nontriviality of a set is preserved under taking subsets.
More concisely: If `α` is a type, `s` is a nontrivial subset of `t` (both of type `α`), then `t` is also a nontrivial set.
|
Set.subsingleton_coe
theorem Set.subsingleton_coe : ∀ {α : Type u} (s : Set α), Subsingleton ↑s ↔ s.Subsingleton
Given a set `s` of some type `α`, this theorem states that the type of `s` (when `s` is coerced to a type) is a subsingleton type if and only if `s` itself is a subsingleton set. In other words, the set `s` has at most one element if and only if the type of `s` has at most one element. Here, a subsingleton type is a type that has at most one inhabitant and a subsingleton set is a set that contains at most one element.
More concisely: The type of a set is a subsingleton type if and only if the set itself is a subsingleton.
|
Set.nontrivial_univ
theorem Set.nontrivial_univ : ∀ {α : Type u} [inst : Nontrivial α], Set.univ.Nontrivial
This theorem states that for any type `α` that is non-trivial (meaning it has at least two distinct elements), the universal set of `α` (which includes all elements of `α`) is also non-trivial. In other words, if a type has at least two distinct elements, then the set containing all elements of this type also has at least two distinct elements.
More concisely: If `α` is a non-empty type with at least two distinct elements, then the universal set of `α` also has at least two distinct elements.
|
Set.Nontrivial.nonempty
theorem Set.Nontrivial.nonempty : ∀ {α : Type u} {s : Set α}, s.Nontrivial → s.Nonempty
This theorem states that for any type `α` and any set `s` of this type, if the set `s` is nontrivial, then it is also nonempty. In other words, if a set has at least two distinct elements (which is the definition of a nontrivial set), then it also has at least one element (which is the definition of a nonempty set). This is a fundamental property of sets in mathematics, and is expressed here in the language of Lean 4 theorem proving.
More concisely: If a set is nontrivial (has at least two distinct elements), then it is nonempty (has at least one element).
|
Set.subsingleton_empty
theorem Set.subsingleton_empty : ∀ {α : Type u}, ∅.Subsingleton
The theorem `Set.subsingleton_empty` asserts that for any type `α`, the empty set is a `Subsingleton`. In other words, the empty set has at most one element for any given type. This is intuitively true as the empty set doesn't contain any elements.
More concisely: The empty set is a Propositional Equivalence type with no elements. (In Lean, this is represented as an instance of `Subsingleton`.)
|
Set.Subsingleton.induction_on
theorem Set.Subsingleton.induction_on :
∀ {α : Type u} {s : Set α} {p : Set α → Prop}, s.Subsingleton → p ∅ → (∀ (x : α), p {x}) → p s
This theorem, `Set.Subsingleton.induction_on`, is a principle of induction for subsets of a type `α` that have at most one element (also known as subsingleton sets). It states that for any property `p` of subsets of `α`, if `p` is true for the empty set and for any singleton set `{x}` where `x` is an element of `α`, then `p` is true for any subsingleton set `s`. In other words, given a property `p`, if `p` holds for the empty set and all singleton sets, it must also hold for all subsingleton sets.
More concisely: If a property holds for the empty set and singletons, it holds for all subsingletons (subsets with at most one element) in a type `α`.
|
Set.nontrivial_coe_sort
theorem Set.nontrivial_coe_sort : ∀ {α : Type u} {s : Set α}, Nontrivial ↑s ↔ s.Nontrivial
The theorem `Set.nontrivial_coe_sort` states that for any type `α` and a set `s` of type `α`, `s` is a nontrivial type if and only if `s` is a nontrivial set. In other words, the set `s` is considered nontrivial (having at least two distinct elements) as a type if and only if it is nontrivial in the set sense.
More concisely: The theorem `Set.nontrivial_coe_sort` asserts that a type `α`'s set instance `s : α` is nontrivial as a type if and only if `s` is a nontrivial set.
|
Set.Nontrivial.not_subsingleton
theorem Set.Nontrivial.not_subsingleton : ∀ {α : Type u} {s : Set α}, s.Nontrivial → ¬s.Subsingleton
This theorem states that for any given type `α` and any set `s` of this type, if the set `s` is Nontrivial (i.e., it contains at least two different elements), then the set `s` is not a Subsingleton. In mathematical terms, a Subsingleton is a set with at most one element, so the theorem is saying that a set with at least two different elements cannot have at most one element, which is a logical necessity.
More concisely: If a set `s` of type `α` contains at least two distinct elements, then `s` is not a subsingleton.
|
Set.Subsingleton.anti
theorem Set.Subsingleton.anti : ∀ {α : Type u} {s t : Set α}, t.Subsingleton → s ⊆ t → s.Subsingleton
The theorem `Set.Subsingleton.anti` states that for any type `α` and any two sets `s` and `t` of type `α`, if `t` is a `Subsingleton` (meaning that `t` contains at most one element) and `s` is a subset of `t`, then `s` is also a `Subsingleton`. In other words, any subset of a set that contains at most one element must also contain at most one element.
More concisely: If `t` is a subsingleton set and `s` is a subset of `t`, then `s` is also a subsingleton.
|
Set.subsingleton_iff_singleton
theorem Set.subsingleton_iff_singleton : ∀ {α : Type u} {s : Set α} {x : α}, x ∈ s → (s.Subsingleton ↔ s = {x}) := by
sorry
This theorem states that for any type `α`, a set `s` of `α`, and an element `x` of `α`, if `x` is an element of `s`, then `s` is a subsingleton set (a set with at most one element) if and only if `s` is the set containing only the element `x`. In other words, a set `s` being a subsingleton is equivalent to `s` being a singleton set `{x}`, given that `x` is an element of `s`.
More concisely: For any type `α` and set `s` of `α` containing an element `x`, `s` is a subsingleton if and only if `s = {x}`.
|
Set.not_subsingleton_iff
theorem Set.not_subsingleton_iff : ∀ {α : Type u} {s : Set α}, ¬s.Subsingleton ↔ s.Nontrivial
The theorem `Set.not_subsingleton_iff` states that for every set `s` of a type `α`, the set `s` is not a subsingleton if and only if `s` is nontrivial. In mathematical terms, a set is defined as nontrivial (has at least two distinct elements) if and only if it is not a subsingleton (has at most one element). This theorem is providing a characterization of nontrivial sets in terms of the negation of being a subsingleton set.
More concisely: A set is nontrivial if and only if it is not a subsingleton.
|
Set.not_nontrivial_iff
theorem Set.not_nontrivial_iff : ∀ {α : Type u} {s : Set α}, ¬s.Nontrivial ↔ s.Subsingleton
The theorem `Set.not_nontrivial_iff` states that for any type `α` and for any set `s` of type `α`, the set `s` is not nontrivial if and only if it is a subsingleton. In other words, a set is not nontrivial, meaning it doesn't have at least two distinct elements, if and only if it is a subsingleton, which means it has at most one element. This theorem provides a logical equivalence between the absence of nontriviality and the presence of subsingleton property in a set.
More concisely: A set is not nontrivial if and only if it is a subsingleton. (In other words, a set has at most one element if and only if it does not have at least two distinct elements.)
|
Set.Subsingleton.eq_singleton_of_mem
theorem Set.Subsingleton.eq_singleton_of_mem :
∀ {α : Type u} {s : Set α}, s.Subsingleton → ∀ {x : α}, x ∈ s → s = {x}
This theorem states that for any given type `α` and a set `s` of that type, if `s` is a `Subsingleton` (meaning it has at most one element), then for any element `x` of type `α` that belongs to `s`, `s` is equal to the singleton set containing only `x`. In other words, if a set has at most one element and an element `x` is in that set, then the set must be exactly the set containing `x`.
More concisely: If `s` is a subsingleton set of type `α` containing an element `x`, then `s` is equal to the singleton set `{x}`.
|
Set.Subsingleton.not_nontrivial
theorem Set.Subsingleton.not_nontrivial : ∀ {α : Type u} {s : Set α}, s.Subsingleton → ¬s.Nontrivial
This theorem, named `Set.Subsingleton.not_nontrivial`, states that for all sets `s` of some type `α`, if `s` is a subsingleton set (a set with at most one element), then it is not nontrivial. In other words, a subsingleton set cannot have two distinct elements. The 'not nontrivial' condition is equivalent to saying that it's impossible for there to exist two distinct elements in the set.
More concisely: A set of type `α` is subsingleton if and only if it does not have two distinct elements.
|
Set.nontrivial_of_nontrivial_coe
theorem Set.nontrivial_of_nontrivial_coe : ∀ {α : Type u} {s : Set α}, Nontrivial ↑s → Nontrivial α
The theorem `Set.nontrivial_of_nontrivial_coe` states that for any type `α` and a set `s` of that type, if the coercive type of `s` is nontrivial, then the type `α` is also nontrivial. Here, a nontrivial type is one that contains at least two distinct elements. This theorem is related to the concept of 'Subtype.nontrivial_iff_exists_ne', which provides a similar result for subtypes.
More concisely: If the coercion of a set is nontrivial, then the type of its elements is also nontrivial.
|
Set.eq_singleton_or_nontrivial
theorem Set.eq_singleton_or_nontrivial : ∀ {α : Type u} {a : α} {s : Set α}, a ∈ s → s = {a} ∨ s.Nontrivial
The theorem `Set.eq_singleton_or_nontrivial` states that for any set `s` of type `α` and any element `a` of type `α`, if `a` is in `s`, then `s` is either a singleton set containing only `a` or `s` is nontrivial. In this context, a set is considered nontrivial if it contains at least two distinct elements.
More concisely: If a set `s` contains an element `a`, then `s` is a singleton containing only `a` or `s` is a nontrivial set with at least two distinct elements.
|
Set.subsingleton_of_subsingleton
theorem Set.subsingleton_of_subsingleton : ∀ {α : Type u} [inst : Subsingleton α] {s : Set α}, s.Subsingleton := by
sorry
The theorem `Set.subsingleton_of_subsingleton` states that for any type `α` that is a subsingleton, and for any set `s` of that type `α`, the set `s` is also a subsingleton. In other words, if a type `α` can have at most one instance (meaning it is a subsingleton), then any set of elements of type `α` can also have at most one element, thus making it a subsingleton set.
More concisely: If `α` is a subsingleton type, then any set `s` of type `α` is also a subsingleton.
|
Set.subsingleton_univ
theorem Set.subsingleton_univ : ∀ {α : Type u} [inst : Subsingleton α], Set.univ.Subsingleton
This theorem states that for any type `α`, given that `α` is a `Subsingleton` (meaning it can have at most one element), the universal set on `α` is also a `Subsingleton`. In other words, if a type `α` has at most one element, then the set of all elements of `α` also has at most one element.
More concisely: If `α` is a subsingleton type, then the universe set `Set α` is also a subsingleton.
|
Set.exists_eq_singleton_iff_nonempty_subsingleton
theorem Set.exists_eq_singleton_iff_nonempty_subsingleton :
∀ {α : Type u} {s : Set α}, (∃ a, s = {a}) ↔ s.Nonempty ∧ s.Subsingleton
This theorem, `Set.exists_eq_singleton_iff_nonempty_subsingleton`, states that for any set `s` of a given type `α`, there exists an element `a` such that `s` is the singleton set containing only `a` if and only if `s` is both non-empty and a subsingleton set. Here, a set being non-empty (`Set.Nonempty`) means there exists at least one element in the set, and a set being a subsingleton (`Set.Subsingleton`) means that it contains at most one distinct element. In other words, a set is equivalent to a singleton set if it is non-empty and all its elements are the same.
More concisely: A set is equal to a singleton set if and only if it is both non-empty and has at most one element.
|