Mathlib.Topology.MetricSpace.Pseudo.Real

Real.dist_left_le_of_mem_uIcc theorem

{x y z : ℝ} (h : y ∈ uIcc x z) : dist x y ≤ dist x z

Full source

lemma dist_left_le_of_mem_uIcc {x y z : ℝ} (h : y ∈ uIcc x z) : dist x y ≤ dist x z := by
  simpa only [dist_comm x] using abs_sub_left_of_mem_uIcc h

Distance Bound for Left Endpoint in Unordered Interval: $d(x, y) \leq d(x, z)$ when $y \in [x, z]$

Informal description

For any real numbers $x$, $y$, and $z$ such that $y$ belongs to the unordered closed interval $[x, z]$, the distance between $x$ and $y$ is less than or equal to the distance between $x$ and $z$, i.e., $d(x, y) \leq d(x, z)$.

Real.dist_right_le_of_mem_uIcc theorem

{x y z : ℝ} (h : y ∈ uIcc x z) : dist y z ≤ dist x z

Full source

lemma dist_right_le_of_mem_uIcc {x y z : ℝ} (h : y ∈ uIcc x z) : dist y z ≤ dist x z := by
  simpa only [dist_comm _ z] using abs_sub_right_of_mem_uIcc h

Distance Bound for Right Endpoint in Unordered Interval: $d(y, z) \leq d(x, z)$ when $y \in [x, z]$

Informal description

For any real numbers $x$, $y$, and $z$ such that $y$ belongs to the unordered closed interval $[x, z]$, the distance between $y$ and $z$ is less than or equal to the distance between $x$ and $z$, i.e., $d(y, z) \leq d(x, z)$.

Real.dist_le_of_mem_uIcc theorem

{x y x' y' : ℝ} (hx : x ∈ uIcc x' y') (hy : y ∈ uIcc x' y') : dist x y ≤ dist x' y'

Full source

lemma 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])

Distance Bound for Points in Unordered Interval: $d(x, y) \leq d(x', y')$ when $x, y \in [[x', y']]$

Informal description

For any real numbers $x, y, x', y'$ such that $x$ and $y$ belong to the unordered closed interval $[[x', y']]$, the distance between $x$ and $y$ is less than or equal to the distance between $x'$ and $y'$, i.e., $d(x, y) \leq d(x', y')$.

Real.dist_le_of_mem_Icc theorem

{x y x' y' : ℝ} (hx : x ∈ Icc x' y') (hy : y ∈ Icc x' y') : dist x y ≤ y' - x'

Full source

lemma 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)

Distance Bound for Points in Closed Interval: $d(x, y) \leq y' - x'$ when $x, y \in [x', y']$

Informal description

For any real numbers $x, y, x', y'$ such that $x$ and $y$ belong to the closed interval $[x', y']$, the distance between $x$ and $y$ is less than or equal to the length of the interval $y' - x'$, i.e., $d(x, y) \leq y' - x'$.

Real.dist_le_of_mem_Icc_01 theorem

{x y : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 1) : dist x y ≤ 1

Full source

lemma dist_le_of_mem_Icc_01 {x y : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 1) :
    dist x y ≤ 1 := by simpa only [sub_zero] using Real.dist_le_of_mem_Icc hx hy

Distance Bound for Points in Unit Interval: $d(x, y) \leq 1$ when $x, y \in [0,1]$

Informal description

For any real numbers $x$ and $y$ in the closed interval $[0, 1]$, the distance between $x$ and $y$ is less than or equal to $1$, i.e., $d(x, y) \leq 1$.

Real.dist_le_of_mem_pi_Icc theorem

(hx : x ∈ Icc x' y') (hy : y ∈ Icc x' y') : dist x y ≤ dist x' y'

Full source

lemma dist_le_of_mem_pi_Icc (hx : x ∈ Icc x' y') (hy : y ∈ Icc x' y') : dist x y ≤ dist x' y' := by
  refine (dist_pi_le_iff dist_nonneg).2 fun b =>
    (Real.dist_le_of_mem_uIcc ?_ ?_).trans (dist_le_pi_dist x' y' b) <;> refine Icc_subset_uIcc ?_
  exacts [⟨hx.1 _, hx.2 _⟩, ⟨hy.1 _, hy.2 _⟩]

Distance Bound for Points in Closed Interval: $d(x, y) \leq d(x', y')$ when $x, y \in [x', y']$

Informal description

For any real numbers $x, y, x', y'$ such that $x$ and $y$ belong to the closed interval $[x', y']$, the distance between $x$ and $y$ is less than or equal to the distance between $x'$ and $y'$, i.e., $d(x, y) \leq d(x', y')$.