English
Let x, y, x', y' be real numbers with x and y belonging to the closed interval [x', y']. Then the distance between x and y satisfies dist(x, y) ≤ y' − x'.
Русский
Пусть x, y, x', y' — вещественные числа, причём x и y принадлежат отрезку [x', y']. Тогда расстояние между x и y удовлетворяет dist(x, y) ≤ y' − x'.
LaTeX
$$$\\forall x, y, x', y' \\in \\mathbb{R},\\ (x \\in Icc(x',y') \\land y \\in Icc(x',y')) \\Rightarrow \\operatorname{dist}(x,y) \\le y' - x'.$$$
Lean4
theorem dist_le_of_mem_Icc {x y x' y' : ℝ} (hx : x ∈ Icc x' y') (hy : y ∈ Icc x' y') : dist x y ≤ y' - x' := by
simpa only [Real.dist_eq, abs_of_nonpos (sub_nonpos.2 <| hx.1.trans hx.2), neg_sub] using
Real.dist_le_of_mem_uIcc (Icc_subset_uIcc hx) (Icc_subset_uIcc hy)
