instProdPseudoMetricSpace — Mathlib

English

There is a PseudoMetricSpace structure on WithLp p (α × β) given by the product distance.

Русский

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

LaTeX

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

Lean4

/-- `PseudoMetricSpace` instance on the product of two pseudometric spaces, using the
`L^p` distance, and having as uniformity the product uniformity. -/
instance instProdPseudoMetricSpace [PseudoMetricSpace α] [PseudoMetricSpace β] : PseudoMetricSpace (WithLp p (α × β)) :=
  ((prodPseudoMetricAux p α β).replaceUniformity (prod_uniformity_aux p α β).symm).replaceBornology fun s =>
    Filter.ext_iff.1 (prod_cobounded_aux p α β).symm sᶜ

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