# Lemmas about distances between points in intervals in `ℝ`. #

source
theorem Real.dist_left_le_of_mem_uIcc {x y z : ℝ} (h : y ∈ Set.uIcc x z) :
dist x y ≤ dist x z
source
theorem Real.dist_right_le_of_mem_uIcc {x y z : ℝ} (h : y ∈ Set.uIcc x z) :
dist y z ≤ dist x z
source
theorem Real.dist_le_of_mem_uIcc {x y x' y' : ℝ} (hx : x ∈ Set.uIcc x' y') (hy : y ∈ Set.uIcc x' y') :
dist x y ≤ dist x' y'
source
theorem Real.dist_le_of_mem_Icc {x y x' y' : ℝ} (hx : x ∈ Set.Icc x' y') (hy : y ∈ Set.Icc x' y') :
dist x y ≤ y' - x'
source
theorem Real.dist_le_of_mem_Icc_01 {x y : ℝ} (hx : x ∈ Set.Icc 0 1) (hy : y ∈ Set.Icc 0 1) :
dist x y ≤ 1
source
theorem Real.dist_le_of_mem_pi_Icc {ι : Type u_1} [Fintype ι] {x y x' y' : ι → ℝ} (hx : x ∈ Set.Icc x' y') (hy : y ∈ Set.Icc x' y') :
dist x y ≤ dist x' y'