metricSpaceMax — Mathlib

English

If γ and β are metric spaces, then the product γ × β is a metric space with the sup (maximum) distance d((g,b),(g',b')) = max{d_γ(g,g'), d_β(b,b')}.

Русский

Если γ и β — метрические пространства, то их произведение γ × β — метрическое пространство с метрикой-супремум: d((g,b),(g',b')) = max{d_γ(g,g'), d_β(b,b')}.

LaTeX

$$$d((x,y),(x',y'))=\\max\\{d_\\gamma(x,x'),\\; d_\\beta(y,y')\\}$$$

Lean4

instance metricSpaceMax [MetricSpace β] : MetricSpace (γ × β) :=
  .ofT0PseudoMetricSpace _

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