dist_triangle

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

For all x,y,z ∈ α, dist(x,z) ≤ dist(x,y) + dist(y,z).

Русский

Пусть x,y,z ∈ α. Тогда dist(x,z) ≤ dist(x,y) + dist(y,z).

LaTeX

$$$dist(x,z) \le dist(x,y) + dist(y,z)$$$

Lean4

@[bound]
theorem dist_triangle (x y z : α) : dist x z ≤ dist x y + dist y z :=
  PseudoMetricSpace.dist_triangle x y z

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

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

Разделы

Аффилиация

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