countable_biInf_principal_eq_seq_iInf

English

For a countable family B of sets, the infimum of principal filters over B equals the infimum over a sequence of principal filters indexed by ℕ.

Русский

Для счетной семьи B множеств инфимуум над фильтрами 'principal' над B равен инфимууму по последовательности над ℕ.

LaTeX

$$$$\\exists x: \\mathbb N \\to \\mathcal P(\\alpha),\\; \\bigwedge_{t \\in B} \\mathcal P(t) = \\bigwedge_{i} \\mathcal P(x(i)).$$$$

Lean4

theorem countable_biInf_principal_eq_seq_iInf {B : Set (Set α)} (Bcbl : B.Countable) :
    ∃ x : ℕ → Set α, ⨅ t ∈ B, 𝓟 t = ⨅ i, 𝓟 (x i) :=
  countable_biInf_eq_iInf_seq' Bcbl 𝓟 principal_univ

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