le_of_inf_neBot' — Mathlib

English

If NeBot (g ⊓ f) then f ≤ g, where g is a filter and f is an ultrafilter.

Русский

Если NeBot (g ⊓ f), то f ≤ g, где g — фильтр, f — ульрафильтр.

LaTeX

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

Lean4

theorem le_of_inf_neBot' (f : Ultrafilter α) {g : Filter α} (hg : NeBot (g ⊓ f)) : ↑f ≤ g :=
  f.le_of_inf_neBot <| by rwa [inf_comm]

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