HepLean Documentation

Mathlib.Order.Filter.Subsingleton

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.

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

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

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

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

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

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

    source
    theorem Filter.subsingleton_iff_exists_le_pure {α : Type u_1} {l : Filter α} [Nonempty α] :
    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.

    source
    theorem Filter.subsingleton_iff_exists_singleton_mem {α : Type u_1} {l : Filter α} [Nonempty α] :
    l.Subsingleton ↔ ∃ (a : α), {a} ∈ l
    source
    theorem Filter.Subsingleton.exists_le_pure {α : Type u_1} {l : Filter α} [Nonempty α] :
    l.Subsingleton → ∃ (a : α), l ≤ pure a

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

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