inf_neBot_iff — Mathlib

English

For any ultrafilter f and filter g, NeBot (f ⊓ g) if and only if f ≤ g.

Русский

Для любого ульрафильтра f и фильтра g NeBot (f ⊓ g) тогда и только тогда, когда f ≤ g.

LaTeX

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

Lean4

theorem inf_neBot_iff {f : Ultrafilter α} {g : Filter α} : NeBot (↑f ⊓ g) ↔ ↑f ≤ g :=
  ⟨le_of_inf_neBot f, fun h => (inf_of_le_left h).symm ▸ f.neBot⟩

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