instIsCountablyGeneratedFinsetFilterUnconditionalOfCountable

English

If β is countable, then the filter (unconditional β).filter is IsCountablyGenerated.

Русский

Если β счётно, то фильтр (unconditional β).filter является счетно порожденным.

LaTeX

$$$[\\text{Countable }\\beta]\\;\\Rightarrow\\; (\\text{unconditional }\\beta).\\text{filter}.IsCountablyGenerated$$$

Lean4

/-- This instance is useful for some measure-theoretic statements. -/
instance [Countable β] : IsCountablyGenerated (unconditional β).filter :=
  atTop.isCountablyGenerated

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