English
A pseudo metric space on a vector space E can be obtained from a SeminormedSpace.Core by defining dist(x,y) = ||x − y||; the induced uniformity and topology follow from this distance.
Русский
Для вектора E можно получить псевдометрическое пространство, задав dist(x,y) = ||x − y||; полученные равномерность и топология задаются этим расстоянием.
LaTeX
$$$\\operatorname{dist}(x,y) = \\|x - y\\|$, defining a PseudoMetricSpace on E$$
Lean4
/-- Produces a `PseudoMetricSpace E` instance from a `SeminormedSpace.Core`. Note that
if this is used to define an instance on a type, it also provides a new uniformity and
topology on the type. See note [reducible non-instances]. -/
abbrev ofSeminormedSpaceCore {𝕜 E : Type*} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E]
(core : SeminormedSpace.Core 𝕜 E) : PseudoMetricSpace E
where
dist x y := ‖x - y‖
dist_self
x := by
show ‖x - x‖ = 0
simp only [sub_self]
have : (0 : E) = (0 : 𝕜) • (0 : E) := by simp
rw [this, core.norm_smul]
simp
dist_comm x
y := by
show ‖x - y‖ = ‖y - x‖
have : y - x = (-1 : 𝕜) • (x - y) := by simp
rw [this, core.norm_smul]
simp
dist_triangle x y
z := by
show ‖x - z‖ ≤ ‖x - y‖ + ‖y - z‖
have : x - z = (x - y) + (y - z) := by abel
rw [this]
exact core.norm_triangle _ _
edist_dist x y := by exact (ENNReal.ofReal_eq_coe_nnreal _).symm
