abs_sub_left_of_mem_uIcc — Mathlib

English

If c lies in the interval [a,b], then the distance from a to c is not larger than the distance from a to b.

Русский

Если c принадлежит интервалу [a,b], то расстояние от a до c не больше расстояния от a до b.

LaTeX

$$$c \in [[a,b]] \Rightarrow |c - a| \le |b - a|$$$

Lean4

/-- If `c ∈ [a, b]`, then the distance between `a` and `c` is less than or equal to
that of `a` and `b` -/
theorem abs_sub_left_of_mem_uIcc (h : c ∈ [[a, b]]) : |c - a| ≤ |b - a| :=
  abs_sub_le_of_uIcc_subset_uIcc <| uIcc_subset_uIcc_left h

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