English
If V is a normed additive group and P is a AddTorsor over V, then P carries a metric defined by d(x,y) = ||x −ᵥ y||, satisfying the metric axioms.
Русский
Пусть V — нормированная аддитивная группа, а P — аддитивный торсор над V. Тогда на P можно определить метрику d(x,y) = ||x −ᵥ y||, удовлетворяющую метрике.
LaTeX
$$$\operatorname{dist}(x,y) = \|x -ᵥ y\|$$$
Lean4
/-- The distance defines a metric space structure on the torsor. This
is not an instance because it depends on `V` to define a `MetricSpace P`. -/
def metricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type*) [NormedAddCommGroup V] [AddTorsor V P] : MetricSpace P
where
dist x y := ‖(x -ᵥ y : V)‖
dist_self x := by simp
eq_of_dist_eq_zero h := by simpa using h
dist_comm x y := by simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]
dist_triangle x y
z := by
rw [← vsub_add_vsub_cancel]
apply norm_add_le
