metricSpacePi — Mathlib

English

A finite product of metric spaces is a metric space with the sup metric: for f,g ∈ ∀ b, X(b), d(f,g) = max_{b∈β} d_b(f(b), g(b)).

Русский

Конечное произведение метрических пространств является метрическим пространством с метрикой-суп: для f,g ∈ ∀b, X(b) выполняется d(f,g) = max_{b∈β} d_b(f(b), g(b)).

LaTeX

$$$d(f,g)=\\max_{b\\in\\beta} d_b(f(b),g(b))$$$

Lean4

/-- A finite product of metric spaces is a metric space, with the sup distance. -/
instance metricSpacePi : MetricSpace (∀ b, X b) :=
  .ofT0PseudoMetricSpace _

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