le_cofinite_or_eq_pure — Mathlib

English

An ultrafilter on an infinite set is either above the cofinite filter or principal at some point.

Русский

Ульрафильтр на бесконечном множестве либо содержит все кофинитные множества, либо является чистым (порождённым точкой).

LaTeX

$$$(f:\! Ultrafilter\ α) \\le cofinite \\lor \\exists a, f = pure a$$

Lean4

theorem le_cofinite_or_eq_pure (f : Ultrafilter α) : (f : Filter α) ≤ cofinite ∨ ∃ a, f = pure a :=
  or_iff_not_imp_left.2 fun h =>
    let ⟨_, hs, hfin⟩ := Filter.disjoint_cofinite_right.1 (disjoint_iff_not_le.2 h)
    let ⟨a, _, hf⟩ := eq_pure_of_finite_mem hfin hs
    ⟨a, hf⟩

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