isCountablyGenerated_biInf_principal

English

If B is a countable set of sets, then the infimum over s ∈ B of principal s is countably generated.

Русский

Если B счётно множество множеств, инфимум по s∈B 𝓟 s счетно-порожден.

LaTeX

$$$B\\text{ Countable} \\Rightarrow \\operatorname{IsCountablyGenerated}\\left(\\bigwedge_{s\\in B} \\mathcal{P}(s)\\right)$$$

Lean4

theorem isCountablyGenerated_biInf_principal {B : Set (Set α)} (h : B.Countable) :
    IsCountablyGenerated (⨅ s ∈ B, 𝓟 s) :=
  isCountablyGenerated_of_seq (countable_biInf_principal_eq_seq_iInf h)

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