le_iff_ultrafilter — Mathlib

English

Let f1 and f2 be filters on α. Then f1 ≤ f2 if and only if for every Ultrafilter g on α, g ≤ f1 implies g ≤ f2.

Русский

Пусть f1 и f2 — фильтры на α. Тогда f1 ≤ f2 тогда и только тогда, когда для каждого ульрафильтра g на α выполняется: g ≤ f1 ⇒ g ≤ f2.

LaTeX

$$$f_1 \\le f_2 \\iff \\forall g : \\mathrm{Ultrafilter} \\; \\alpha,\\; g \\le f_1 \\rightarrow g \\le f_2$$$

Lean4

theorem le_iff_ultrafilter {f₁ f₂ : Filter α} : f₁ ≤ f₂ ↔ ∀ g : Ultrafilter α, ↑g ≤ f₁ → ↑g ≤ f₂ :=
  ⟨fun h _ h₁ => h₁.trans h, fun h _ hs => mem_iff_ultrafilter.2 fun g hg => h g hg hs⟩

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