English
Let p be monotone. Then for any g, (for all f, NeBot f and f ≤ g, p f) holds if and only if (for all ultrafilters f, f ≤ g, p f) holds.
Русский
Пусть p монотонна. Тогда для любого g верно: (для всех f с NeBot f и f ≤ g выполняется p f) тогда и только тогда, когда (для всех ультрафильтров f, f ≤ g выполняется p f).
LaTeX
$$$\\text{Monotone}(p) \\Rightarrow \\Big(\\forall f : \\mathrm{Filter} \\; \\alpha, \\mathrm{NeBot}(f) \\to f \\le g \\to p f\\Big) \\iff \\Big(\\forall f : \\mathrm{Ultrafilter} \\; \\alpha, f \\le g \\to p f\\Big)$$$
Lean4
theorem forall_neBot_le_iff {g : Filter α} {p : Filter α → Prop} (hp : Monotone p) :
(∀ f : Filter α, NeBot f → f ≤ g → p f) ↔ ∀ f : Ultrafilter α, ↑f ≤ g → p f :=
by
refine ⟨fun H f hf => H f f.neBot hf, ?_⟩
intro H f hf hfg
exact hp (of_le f) (H _ ((of_le f).trans hfg))
