instProd — Mathlib

English

A product of spaces with discrete uniformity again carries a discrete uniformity.

Русский

Произведение пространств с дискретной равномерностью опять наделено дискретной равномерностью.

LaTeX

$$$\text{DiscreteUniformity} (X \times Y)$$$

Lean4

/-- A product of spaces with discrete uniformity has a discrete uniformity. -/
instance {Y : Type*} [UniformSpace Y] [DiscreteUniformity Y] : DiscreteUniformity (X × Y) := by
  simp [discreteUniformity_iff_eq_principal_idRel, uniformity_prod_eq_comap_prod, eq_principal_idRel, idRel,
    Set.prod_eq, Prod.ext_iff, Set.setOf_and]

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