dist_triangle_right

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

theorem dist_triangle_right (x y z : α) : dist x y ≤ dist x z + dist y z := by rw [dist_comm y]; apply dist_triangle

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

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

Разделы

Аффилиация

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