English
If α and β are pseudo-metric spaces, the product α × β carries a natural pseudo-metric given by the maximum of the coordinate distances: dist((a,b),(c,d)) = max(distα(a,c), distβ(b,d)).
Русский
Пусть α и β — псевдометрические пространства. Произведение α × β оборудовано метрической структурой, задаваемой максимальной дистанцией по координатам: dist((a,b),(c,d)) = max(distα(a,c), distβ(b,d)).
LaTeX
$$$\operatorname{dist}((a,b),(c,d)) = \max(\operatorname{dist}(a,c), \operatorname{dist}(b,d))$$$
Lean4
instance pseudoMetricSpaceMax : PseudoMetricSpace (α × β) :=
let i :=
PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun x y : α × β => dist x.1 y.1 ⊔ dist x.2 y.2)
(fun _ _ => (max_lt (edist_lt_top _ _) (edist_lt_top _ _)).ne) fun x y => by
simp only [dist_edist, ← ENNReal.toReal_max (edist_ne_top _ _) (edist_ne_top _ _), Prod.edist_eq]
i.replaceBornology fun s =>
by
simp only [← isBounded_image_fst_and_snd, isBounded_iff_eventually, forall_mem_image, ← eventually_and,
← forall_and, ← max_le_iff]
rfl
