instProdEMetricSpace — Mathlib

English

There is an EMetricSpace structure on WithLp p (α × β) coming from the product EMetric structure.

Русский

Существует структура EMetricSpace на WithLp p (α × β), наследуемая от произведения EMetric.

LaTeX

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

Lean4

/-- `EMetricSpace` instance on the product of two emetric spaces, using the `L^p`
edistance, and having as uniformity the product uniformity. -/
instance instProdEMetricSpace [EMetricSpace α] [EMetricSpace β] : EMetricSpace (WithLp p (α × β)) :=
  EMetricSpace.ofT0PseudoEMetricSpace (WithLp p (α × β))

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