English
The finite product of emetric spaces, endowed with the maximum distance, is again an emetric space.
Русский
Конечное произведение эм-метрик ограничено максимум-дистанцией, и является эм-метрическим пространством.
LaTeX
$$$$ \\text{PseudoEMetricSpace}((b:\\beta) \\to X(b)). $$$$
Lean4
/-- The product of a finite number of pseudoemetric spaces, with the max distance, is still
a pseudoemetric 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 pseudoEMetricSpacePi [∀ b, PseudoEMetricSpace (X b)] : PseudoEMetricSpace (∀ b, X b)
where
edist_self f := bot_unique <| Finset.sup_le <| by simp
edist_comm f g := by simp [edist_pi_def, edist_comm]
edist_triangle _ g
_ :=
edist_pi_le_iff.2 fun b =>
le_trans (edist_triangle _ (g b) _) (add_le_add (edist_le_pi_edist _ _ _) (edist_le_pi_edist _ _ _))
toUniformSpace := Pi.uniformSpace _
uniformity_edist :=
by
simp only [Pi.uniformity, PseudoEMetricSpace.uniformity_edist, comap_iInf, gt_iff_lt, preimage_setOf_eq,
comap_principal, edist_pi_def]
rw [iInf_comm]; congr; funext ε
rw [iInf_comm]; congr; funext εpos
simp [setOf_forall, εpos]
