isCountablyGenerated_iff_exists_antitone_basis

English

A filter is countably generated iff there exists an antitone basis x with f.HasAntitoneBasis x.

Русский

Фильтр счетно порожден тогда и только тогда, когда существует антитонное основание x с f.HasAntitoneBasis x.

LaTeX

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

Lean4

theorem isCountablyGenerated_iff_exists_antitone_basis {f : Filter α} :
    IsCountablyGenerated f ↔ ∃ x : ℕ → Set α, f.HasAntitoneBasis x :=
  by
  constructor
  · intro h
    exact f.exists_antitone_basis
  · rintro ⟨x, h⟩
    rw [h.1.eq_iInf]
    exact isCountablyGenerated_seq x

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