Filter.subsingleton_iff_bot_or_pure
theorem Filter.subsingleton_iff_bot_or_pure :
∀ {α : Type u_1} {l : Filter α}, l.Subsingleton ↔ l = ⊥ ∨ ∃ a, l = pure a
This theorem states that for any filter `l` over a type `α`, `l` is a subsingleton (i.e., it contains at most one element) if and only if `l` is equal to the bottom filter `⊥` (which contains no elements) or `l` is equal to `pure a` for some element `a` of type `α`. In other words, a filter is a subsingleton only when it is either empty or contains exactly one element.
More concisely: A filter over type `α` is a subsingleton if and only if it is the bottom filter or equals `pure a` for some `a : α`.
|
Filter.Subsingleton.exists_eq_pure
theorem Filter.Subsingleton.exists_eq_pure :
∀ {α : Type u_1} {l : Filter α} [inst : l.NeBot], l.Subsingleton → ∃ a, l = pure a
This theorem states that for any nontrivial (i.e., not the bottom element) filter `l` on a type `α`, if `l` is a subsingleton (i.e., has at most one element), then there exists some element `a` such that `l` is equal to the pure filter of `a`. A pure filter of `a` is a filter that only contains sets which include `a`.
More concisely: If `l` is a nontrivial, subsingleton filter on type `α`, then `l` is the pure filter of some element `a` in `α`.
|
Filter.subsingleton_iff_exists_le_pure
theorem Filter.subsingleton_iff_exists_le_pure :
∀ {α : Type u_1} {l : Filter α} [inst : Nonempty α], l.Subsingleton ↔ ∃ a, l ≤ pure a
This theorem states that in a nonempty type `α`, a filter `l` is a subsingleton (i.e., it contains at most one element) if and only if there exists an element `a` such that `l` is less than or equal to the pure filter generated by `a`. A pure filter is a filter that contains all sets which include a specific element. The relation "less than or equal to" for filters indicates that all sets in `l` are also in the pure filter.
More concisely: A filter `l` over a nonempty type `α` is a subsingleton if and only if there exists an element `a` such that `l` is included in the pure filter generated by `a`.
|
Filter.Subsingleton.map
theorem Filter.Subsingleton.map :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α}, l.Subsingleton → ∀ (f : α → β), (Filter.map f l).Subsingleton := by
sorry
The theorem `Filter.Subsingleton.map` states that for all types `α` and `β`, and for any filter `l` on type `α`, if the filter `l` is a subsingleton (which means there exists a subsingleton set that belongs to the filter `l`), then for any function `f` from `α` to `β`, the filter resulting from mapping `f` onto `l` is also a subsingleton. In simple terms, it means that the property of being a subsingleton is preserved under the operation of mapping a function onto a filter.
More concisely: If `l` is a subsingleton filter on type `α` and `f` is a function from `α` to `β`, then the filter `Map (f) l` on `β` is also a subsingleton filter.
|
Filter.Subsingleton.exists_le_pure
theorem Filter.Subsingleton.exists_le_pure :
∀ {α : Type u_1} {l : Filter α} [inst : Nonempty α], l.Subsingleton → ∃ a, l ≤ pure a
This theorem states that for any filter `l` on a nonempty type `α`, if `l` is a subsingleton (i.e., it contains at most one element), then there exists an element `a` such that `l` is less than or equal to the filter generated by `pure a` (the principal filter generated by `a`). Essentially, it says that a subsingleton filter can always be bounded by a principal filter on some element of the set.
More concisely: If `l` is a subsingleton filter on a nonempty type `α`, then there exists an element `a` such that `l` is included in the principal filter `pure a`.
|
Mathlib.Order.Filter.Subsingleton._auxLemma.3
theorem Mathlib.Order.Filter.Subsingleton._auxLemma.3 : ∀ {α : Type u_1}, ⊥.Subsingleton = True
The theorem `Mathlib.Order.Filter.Subsingleton._auxLemma.3` states that, for any type `α`, the bottom filter (denoted by `⊥`) is a subsingleton. Recall that a filter is considered a subsingleton if there exists a subsingleton set that belongs to the filter. The bottom filter is a subsingleton because it contains only the empty set, which is a subsingleton set.
More concisely: The bottom filter (⊥) over any type α is a subsingleton due to it containing the subsingleton empty set.
|