instProdMetricSpace — Mathlib

English

There is a MetricSpace structure on WithLp p (α × β) when α, β are MetricSpaces.

Русский

Существует метрическое пространство на WithLp p (α × β), если α и β — метрические пространства.

LaTeX

$$$ [\\text{MetricSpace} \\ (\\mathrm{WithLp}_{p}(\\alpha \\times \\beta))] $$$

Lean4

/-- `MetricSpace` instance on the product of two metric spaces, using the `L^p` distance,
and having as uniformity the product uniformity. -/
instance instProdMetricSpace [MetricSpace α] [MetricSpace β] : MetricSpace (WithLp p (α × β)) :=
  MetricSpace.ofT0PseudoMetricSpace _

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