exists_antitone_seq — Mathlib

English

If f is countably generated, there exists a decreasing sequence x: ℕ → Set α such that for all s, s ∈ f iff ∃ i, x(i) ⊆ s.

Русский

Если f счетно порожден, существует убывающая последовательность x: ℕ → Set α такая, что для любого s: s ∈ f тогда и только если ∃ i, x(i) ⊆ s.

LaTeX

$$$\\exists x:\\mathbb{N}\\to \\mathrm{Set}(\\alpha),\\ \\mathrm{Antitone}(x) \\wedge \\forall \\{s\\},\\ s\\in f \\iff \\exists i, x(i)\\subseteq s$$$

Lean4

theorem exists_antitone_seq (f : Filter α) [f.IsCountablyGenerated] :
    ∃ x : ℕ → Set α, Antitone x ∧ ∀ {s}, s ∈ f ↔ ∃ i, x i ⊆ s :=
  let ⟨x, hx⟩ := f.exists_antitone_basis
  ⟨x, hx.antitone, by simp [hx.1.mem_iff]⟩

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