isCountablyGenerated — Mathlib

English

The supremum (join) of two countably generated filters is countably generated.

Русский

Супремум (наим. верх. предел) двух счетно порожденных фильтров счетно порожден.

LaTeX

$$$(\\text{IsCountablyGenerated}\\ f) \\land (\\text{IsCountablyGenerated}\\ g) \\Rightarrow \\text{IsCountablyGenerated}(f \\sqcup g)$$$

Lean4

instance isCountablyGenerated (f g : Filter α) [IsCountablyGenerated f] [IsCountablyGenerated g] :
    IsCountablyGenerated (f ⊔ g) := by
  rcases f.exists_antitone_basis with ⟨s, hs⟩
  rcases g.exists_antitone_basis with ⟨t, ht⟩
  exact HasCountableBasis.isCountablyGenerated ⟨hs.1.sup ht.1, Set.to_countable _⟩

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