instProdPseudoEMetricSpace — Mathlib

English

There is an EMetricSpace structure on WithLp p (α × β) when α and β are EMetricSpaces.

Русский

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

LaTeX

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

Lean4

/-- `PseudoEMetricSpace` instance on the product of two pseudoemetric spaces, using the
`L^p` pseudoedistance, and having as uniformity the product uniformity. -/
instance instProdPseudoEMetricSpace [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
    PseudoEMetricSpace (WithLp p (α × β)) :=
  (prodPseudoEMetricAux p α β).replaceUniformity (prod_uniformity_aux p α β).symm

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