exists_antitone_basis — Mathlib

English

A countably generated filter admits an antitone basis; there exists a sequence x of sets such that f.HasAntitoneBasis x.

Русский

У счетно порожденного фильтра существует антитонное основание; существует последовательность x such that f.HasAntitoneBasis x.

LaTeX

$$$\\exists x:\\\\mathbb{N}\\to \\mathrm{Set}(\\alpha),\\ f.HasAntitoneBasis x$$$

Lean4

/-- A countably generated filter admits a basis formed by an antitone sequence of sets. -/
theorem exists_antitone_basis (f : Filter α) [f.IsCountablyGenerated] : ∃ x : ℕ → Set α, f.HasAntitoneBasis x :=
  let ⟨x, _, hx⟩ := f.basis_sets.exists_antitone_subbasis
  ⟨x, hx⟩

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