isCountablyGenerated — Mathlib

English

The infimum over a countable family of principal filters is countably generated.

Русский

Инфинтим над счётной семейством простых фильтров счетно-порожден.

LaTeX

$$$\\operatorname{IsCountablyGenerated}_{B}(\\bigwedge_{s\\in B} \\mathcal{P}(s))$$$

Lean4

instance isCountablyGenerated {ι : Sort*} {α : Type*} [Countable ι] (f : ι → Filter α)
    [∀ i, IsCountablyGenerated (f i)] : IsCountablyGenerated (⨅ i, f i) :=
  by
  choose s hs using fun i => exists_antitone_basis (f i)
  rw [← PLift.down_surjective.iInf_comp]
  refine HasCountableBasis.isCountablyGenerated ⟨.iInf fun n => (hs _).1, ?_⟩
  refine (countable_range <| Sigma.map ((↑) : Finset (PLift ι) → Set (PLift ι)) fun _ => id).mono ?_
  rintro ⟨I, f⟩ ⟨hI, -⟩
  lift I to Finset (PLift ι) using hI
  exact ⟨⟨I, f⟩, rfl⟩

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