isCountablyGenerated — Mathlib

English

The intersection (infimum) of two countably generated filters is countably generated.

Русский

Пересечение двух счетно порожденных фильтров счетно порождено.

LaTeX

$$$(\\text{IsCountablyGenerated}\\ f) \\land (\\text{IsCountablyGenerated}\\ g) \\Rightarrow \\text{IsCountablyGenerated}(f \\sqcap 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.inf ht.1, Set.to_countable _⟩

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