instCountableOrCountablyGeneratedOfCountable

English

If α is countable and β has a measurable space structure, then CountableOrCountablyGenerated α β holds.

Русский

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

LaTeX

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

Lean4

instance instCountableOrCountablyGeneratedOfCountable [h1 : Countable α] [MeasurableSpace β] :
    CountableOrCountablyGenerated α β :=
  ⟨Or.inl h1⟩

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