HepLean Documentation

Mathlib.Topology.MetricSpace.Pseudo.Real

Lemmas about distances between points in intervals in . #

theorem Real.dist_left_le_of_mem_uIcc {x y z : } (h : y Set.uIcc x z) :
dist x y dist x z
theorem Real.dist_right_le_of_mem_uIcc {x y z : } (h : y Set.uIcc x z) :
dist y z dist x z
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'
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'
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
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'