instIsCountablyGeneratedFinsetFilterConditionalOfAtTopOfAtBot

English

If atTop and atBot are countably generated, then (conditional β).filter is IsCountablyGenerated.

Русский

Если atTop и atBot счётно порождены, то (conditional β).filter — счетно порожденный.

LaTeX

$$$[\\text{IsCountablyGenerated}(atTop)]\\;[\\IsCountablyGenerated](atBot)\\;\\Rightarrow\\; IsCountablyGenerated(conditional(\\beta).filter)$$$

Lean4

instance [IsCountablyGenerated (atTop : Filter β)] [IsCountablyGenerated (atBot : Filter β)] :
    IsCountablyGenerated (conditional β).filter :=
  map.isCountablyGenerated ..

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