English
For the product α×β, edist is the maximum of the componentwise distances: edist((x1,x2),(y1,y2)) = max(edist(x1,y1), edist(x2,y2)).
Русский
На произведении α×β расстояние edist равно максимуму расстояний компонент: edist((x1,x2),(y1,y2)) = max(edist(x1,y1), edist(x2,y2)).
LaTeX
$$$\operatorname{edist}((x_1,x_2),(y_1,y_2)) = \max\bigl(\operatorname{edist}(x_1,y_1),\operatorname{edist}(x_2,y_2)\bigr).$$$
Lean4
/-- Consider an extended distance on a topological space, for which the neighborhoods can be
expressed in terms of the distance. Then we define the emetric space structure associated to this
distance, with a topology defeq to the initial one. -/
@[reducible]
noncomputable def ofEdistOfTopology {α : Type*} [TopologicalSpace α] (d : α → α → ℝ≥0∞) (h_self : ∀ x, d x x = 0)
(h_comm : ∀ x y, d x y = d y x) (h_triangle : ∀ x y z, d x z ≤ d x y + d y z)
(h_basis : ∀ x, (𝓝 x).HasBasis (fun c ↦ 0 < c) (fun c ↦ {y | d x y < c})) : PseudoEMetricSpace α
where
edist := d
edist_self := h_self
edist_comm := h_comm
edist_triangle := h_triangle
toUniformSpace := uniformSpaceOfEDistOfHasBasis d h_self h_comm h_triangle h_basis
uniformity_edist := rfl
