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]