dist_right_le_of_mem_uIcc

Mathlib.Topology.MetricSpace.Pseudo.Real

URI: https://scilib.ai/kg/mathlib#Real.dist_right_le_of_mem_uIcc

← MathLib Explorer

English

If y ∈ uIcc(x,z), then dist(y,z) ≤ dist(x,z).

Русский

Если y ∈ uIcc(x,z), то dist(y,z) ≤ dist(x,z).

LaTeX

$$$\mathrm{dist}(y,z) \le \mathrm{dist}(x,z)\quad (y \in \mathrm{uIcc}(x,z)).$$$

Lean4

theorem dist_right_le_of_mem_uIcc {x y z : ℝ} (h : y ∈ uIcc x z) : dist y z ≤ dist x z := by
  simpa only [dist_comm _ z] using abs_sub_right_of_mem_uIcc h

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

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

Разделы

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

Аффилиация

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