le_of_inf_neBot — Mathlib

English

If the infimum of f with a filter g is nontrivial, then f ≤ g.

Русский

Если наименьшее индетерминированное пересечение ульрафильтра f с фильтром g не нулевое, то f ≤ g.

LaTeX

$$$\\\\forall f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha), \\\\forall g \\\\in \\\\mathrm{Filter}(\\\\alpha), NeBot (\\\\uparrow f \\\\cap g) \\\\Rightarrow (\\\\uparrow f) \\\\le g$$$

Lean4

theorem le_of_inf_neBot (f : Ultrafilter α) {g : Filter α} (hg : NeBot (↑f ⊓ g)) : ↑f ≤ g :=
  le_of_inf_eq (f.unique inf_le_left hg)

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