instIsCountablyGeneratedProdSumUniformity

English

If both 𝓤 α and 𝓤 β are countably generated, then 𝓤(α ⊕ β) is also countably generated.

Русский

Если 𝓤 α и 𝓤 β счётно порождаются, то и 𝓤(α ⊕ β) счётно порождается.

LaTeX

$$IsCountablyGenerated(𝓤(α ⊕ β)) given IsCountablyGenerated(𝓤 α) and IsCountablyGenerated(𝓤 β)$$

Lean4

instance [IsCountablyGenerated (𝓤 α)] [IsCountablyGenerated (𝓤 β)] : IsCountablyGenerated (𝓤 (α ⊕ β)) :=
  by
  rw [Sum.uniformity]
  infer_instance

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