isCountablyGenerated_seq — Mathlib

English

For a countable index set, the infimum of principal filters is countably generated.

Русский

Для счётного множества индексов инфимум простых фильтров счетно-порожден.

LaTeX

$$$[Countable\\ ι'] (x : ι' \\to Set\\ α)\\; :\\; \\operatorname{IsCountablyGenerated}\\left(\\bigwedge_i \\mathcal{P}(x_i)\\right)$$$

Lean4

theorem isCountablyGenerated_seq [Countable ι'] (x : ι' → Set α) : IsCountablyGenerated (⨅ i, 𝓟 (x i)) :=
  by
  use range x, countable_range x
  rw [generate_eq_biInf, iInf_range]

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