instEMetricSpace — Mathlib

English

The emetric space structure on PiLp p β is defined using the Lp-based edistance with product uniformity.

Русский

Структура эметрического пространства на PiLp p β определяется через Lp-расстояние и произведение равномерностей.

LaTeX

$$EMetricSpace (PiLp p β)$$

Lean4

/-- emetric space instance on the product of finitely many emetric spaces, using the `L^p`
edistance, and having as uniformity the product uniformity. -/
instance [∀ i, EMetricSpace (α i)] : EMetricSpace (PiLp p α) :=
  @EMetricSpace.ofT0PseudoEMetricSpace (PiLp p α) _ Pi.instT0Space

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