triangle

Mathlib.Topology.MetricSpace.BundledFun

URI: https://scilib.ai/kg/mathlib#PseudoMetric.triangle

English

Triangle inequality: d(x,z) ≤ d(x,y) + d(y,z).

Русский

Неравенство треугольника: d(x,z) ≤ d(x,y) + d(y,z).

LaTeX

$$$d(x,z) \le d(x,y) + d(y,z).$$$

Lean4

protected theorem triangle (x y z : X) : d x z ≤ d x y + d y z :=
  d.triangle' x y z

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

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

Разделы

Аффилиация

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