sInf_neBot_of_directed' — Mathlib

English

In a directed family of filters, if the set of filters is nonempty and not contained in ⊥, then sInf is nontrivial.

Русский

В направленной семье фильтров, если она не пуста и не лежит в ⊥, то sInf не тривиален.

LaTeX

$$s.Nonempty → DirectedOn (· ≥ ·) s → ⊥ ∉ s → (sInf s).NeBot$$

Lean4

theorem sInf_neBot_of_directed' {s : Set (Filter α)} (hne : s.Nonempty) (hd : DirectedOn (· ≥ ·) s) (hbot : ⊥ ∉ s) :
    NeBot (sInf s) :=
  (sInf_eq_iInf' s).symm ▸
    @iInf_neBot_of_directed' _ _ _ hne.to_subtype hd.directed_val fun ⟨_, hf⟩ => ⟨ne_of_mem_of_not_mem hf hbot⟩

Похожие утверждения