instMetricSpace — Mathlib

English

A pseudo-metric space structure is placed on PiLp p α when each α_i is a pseudo-metric space, compatible with the product uniformity.

Русский

На PiLp p α задаётся псевдометрическое пространство, если каждое α_i является псевдометрическим пространством.

LaTeX

$$PseudoMetricSpace (PiLp p α)$$

Lean4

/-- metric space instance on the product of finitely many metric spaces, using the `L^p` distance,
and having as uniformity the product uniformity. -/
instance [∀ i, MetricSpace (α i)] : MetricSpace (PiLp p α) :=
  MetricSpace.ofT0PseudoMetricSpace _

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