isCountablyGenerated — Mathlib

English

The coproduct (coprod) of two countably generated filters is countably generated.

Русский

Копродукт фильтров счетно порожден.

LaTeX

$$$(la)\\text{ і }(lb) : \\operatorname{IsCountablyGenerated}(la) \\land \\operatorname{IsCountablyGenerated}(lb) \\rightarrow \\operatorname{IsCountablyGenerated}(la.coprod(lb))$$$

Lean4

instance isCountablyGenerated (la : Filter α) (lb : Filter β) [IsCountablyGenerated la] [IsCountablyGenerated lb] :
    IsCountablyGenerated (la.coprod lb) :=
  Filter.Sup.isCountablyGenerated _ _

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