dist_le_of_mem_uIcc — Mathlib

English

If x and y are in the uIcc around x' and y', then dist(x,y) ≤ dist(x',y').

Русский

Если x и y принадлежат uIcc между x' и y', то dist(x,y) ≤ dist(x',y').

LaTeX

$$$\mathrm{dist}(x,y) \le \mathrm{dist}(x',y')$ при условии, что x,y ∈ \mathrm{uIcc}(x',y').$$$

Lean4

theorem dist_le_of_mem_uIcc {x y x' y' : ℝ} (hx : x ∈ uIcc x' y') (hy : y ∈ uIcc x' y') : dist x y ≤ dist x' y' :=
  abs_sub_le_of_uIcc_subset_uIcc <| uIcc_subset_uIcc (by rwa [uIcc_comm]) (by rwa [uIcc_comm])

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