English
If a point y lies in the open ball around x with radius ε, then ε is positive: edist(y,x) < ε implies ε > 0.
Русский
Если точка y принадлежит открытой окрестности x радиуса ε, тогда ε>0: edist(y,x) < ε ⇒ ε > 0.
LaTeX
$$$\operatorname{edist}(y,x) < \varepsilon \implies 0 < \varepsilon.$$$
Lean4
/-- The product of two pseudoemetric spaces, with the max distance, is an extended
pseudometric spaces. We make sure that the uniform structure thus constructed is the one
corresponding to the product of uniform spaces, to avoid diamond problems. -/
instance pseudoEMetricSpaceMax [PseudoEMetricSpace β] : PseudoEMetricSpace (α × β)
where
edist x y := edist x.1 y.1 ⊔ edist x.2 y.2
edist_self x := by simp
edist_comm x y := by simp [edist_comm]
edist_triangle _ _
_ :=
max_le (le_trans (edist_triangle _ _ _) (add_le_add (le_max_left _ _) (le_max_left _ _)))
(le_trans (edist_triangle _ _ _) (add_le_add (le_max_right _ _) (le_max_right _ _)))
uniformity_edist := uniformity_prod.trans <| by simp [PseudoEMetricSpace.uniformity_edist, ← iInf_inf_eq, setOf_and]
toUniformSpace := inferInstance
