dist_dist_dist_le_right

Mathlib.Topology.MetricSpace.Pseudo.Defs

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

← MathLib Explorer

English

Similarly, dist(dist(x,y), dist(x,z)) ≤ dist(y,z).

Русский

Аналогично, dist(dist(x,y), dist(x,z)) ≤ dist(y,z).

LaTeX

$$$\operatorname{dist}(\operatorname{dist}(x,y), \operatorname{dist}(x,z)) \le \operatorname{dist}(y,z)$$$

Lean4

theorem dist_dist_dist_le_right (x y z : α) : dist (dist x y) (dist x z) ≤ dist y z := by
  simpa only [dist_comm x] using dist_dist_dist_le_left y z x

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

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

Разделы

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

Аффилиация

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