emetricSpaceMax — Mathlib

English

The product of two emetric spaces with the max distance yields an emetric space.

Русский

Произведение двух эмметрических пространств с расстоянием по максимуму образует эмметрическое пространство.

LaTeX

$$Prod.emetricSpaceMax$$

Lean4

/-- The product of two emetric spaces, with the max distance, is an extended
metric spaces. We make sure that the uniform structure thus constructed is the one
corresponding to the product of uniform spaces, to avoid diamond problems. -/
instance emetricSpaceMax [EMetricSpace β] : EMetricSpace (γ × β) :=
  .ofT0PseudoEMetricSpace _

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