instIsCountablyGeneratedProdUniformity

English

If α and β are uniform spaces with countably generated uniformities, then the product uniformity on α × β is countably generated.

Русский

Если пространства α и β являются равномерными пространствами с счетно порожденными униформностями, то униформность на произведении α × β также счетно порождается.

LaTeX

$$$[UniformSpace \alpha] \,[IsCountablyGenerated(\mathcal{U}(\alpha))] \,[UniformSpace \beta] \,[IsCountablyGenerated(\mathcal{U}(\beta))] \\Rightarrow IsCountablyGenerated(\mathcal{U}(\alpha \times \beta))$$$

Lean4

instance [UniformSpace α] [IsCountablyGenerated (𝓤 α)] [UniformSpace β] [IsCountablyGenerated (𝓤 β)] :
    IsCountablyGenerated (𝓤 (α × β)) := by
  rw [uniformity_prod]
  infer_instance

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