# Subsingleton filters #

We say that a filter l is a subsingleton if there exists a subsingleton set s ∈ l. Equivalently, l is either ⊥ or pure a for some a.

def Filter.Subsingleton {α : Type u_1} (l : ) :

We say that a filter is a subsingleton if there exists a subsingleton set that belongs to the filter.

Equations
• l.Subsingleton = sl, s.Subsingleton
Instances For
theorem Filter.HasBasis.subsingleton_iff {α : Type u_1} {l : } {ι : Sort u_3} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) :
l.Subsingleton ∃ (i : ι), p i (s i).Subsingleton
theorem Filter.Subsingleton.anti {α : Type u_1} {l : } {l' : } (hl : l.Subsingleton) (hl' : l' l) :
l'.Subsingleton
theorem Filter.Subsingleton.of_subsingleton {α : Type u_1} {l : } [] :
l.Subsingleton
theorem Filter.Subsingleton.map {α : Type u_1} {β : Type u_2} {l : } (hl : l.Subsingleton) (f : αβ) :
().Subsingleton
theorem Filter.Subsingleton.prod {α : Type u_1} {β : Type u_2} {l : } (hl : l.Subsingleton) {l' : } (hl' : l'.Subsingleton) :
(l ×ˢ l').Subsingleton
@[simp]
theorem Filter.subsingleton_pure {α : Type u_1} {a : α} :
(pure a).Subsingleton
@[simp]
theorem Filter.subsingleton_bot {α : Type u_1} :
.Subsingleton
theorem Filter.Subsingleton.exists_eq_pure {α : Type u_1} {l : } [l.NeBot] (hl : l.Subsingleton) :
∃ (a : α), l = pure a

A nontrivial subsingleton filter is equal to pure a for some a.

theorem Filter.subsingleton_iff_bot_or_pure {α : Type u_1} {l : } :
l.Subsingleton l = ∃ (a : α), l = pure a

A filter is a subsingleton iff it is equal to ⊥ or to pure a for some a.

theorem Filter.subsingleton_iff_exists_le_pure {α : Type u_1} {l : } [] :
l.Subsingleton ∃ (a : α), l pure a

In a nonempty type, a filter is a subsingleton iff it is less than or equal to a pure filter.

theorem Filter.subsingleton_iff_exists_singleton_mem {α : Type u_1} {l : } [] :
l.Subsingleton ∃ (a : α), {a} l
theorem Filter.Subsingleton.exists_le_pure {α : Type u_1} {l : } [] :
l.Subsingleton∃ (a : α), l pure a

A subsingleton filter on a nonempty type is less than or equal to pure a for some a.

theorem Filter.Subsingleton.isCountablyGenerated {α : Type u_1} {l : } (hl : l.Subsingleton) :
l.IsCountablyGenerated