instCountableOrCountablyGeneratedOfCountablyGenerated

English

If β is countably generated and α has a measurable space, then CountableOrCountablyGenerated α β holds.

Русский

Если β счетно-генерируемо и α имеет пространство измерения, то выполняется CountableOrCountablyGenerated α β.

LaTeX

$$$[\text{MeasurableSpace } \alpha] \;[\text{CountablyGenerated } \beta] \Rightarrow \text{CountableOrCountablyGenerated } (\alpha, \beta)$$$

Lean4

instance instCountableOrCountablyGeneratedOfCountablyGenerated [MeasurableSpace β] [h : CountablyGenerated β] :
    CountableOrCountablyGenerated α β :=
  ⟨Or.inr h⟩

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