dist_triangle_left

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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