emetricSpacePi — Mathlib

English

The product of a finite family of emetric spaces is an emetric space.

Русский

Произведение конечной семьи эм-метрических пространств является эм-метрическим пространством.

LaTeX

$$$$ \\operatorname{EMetricSpace}((b:\\beta) \\to X(b)). $$$$

Lean4

/-- The product of a finite number of emetric spaces, with the max distance, is still
an emetric space.
This construction would also work for infinite products, but it would not give rise
to the product topology. Hence, we only formalize it in the good situation of finitely many
spaces. -/
instance emetricSpacePi [∀ b, EMetricSpace (X b)] : EMetricSpace (∀ b, X b) :=
  .ofT0PseudoEMetricSpace _

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