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