pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor

Mathlib.Analysis.Normed.Group.AddTorsor

URI: https://scilib.ai/kg/mathlib#pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor

Lean4

/-- The pseudodistance defines a pseudometric space structure on the torsor. This
is not an instance because it depends on `V` to define a `MetricSpace P`. -/
def pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type*) [SeminormedAddCommGroup V] [AddTorsor V P] :
    PseudoMetricSpace P where
  dist x y := ‖(x -ᵥ y : V)‖
  dist_self x := by simp
  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

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru