abs_sub_right_of_mem_uIcc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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