English
The projection onto [a,b] is 1-Lipschitz: |projIcc a b h c − projIcc a b h d| ≤ |c − d|.
Русский
Проекция на [a,b] не увеличивает расстояния: расстояние между проекциями не превосходит расстояния между исходными точками.
LaTeX
$$|projIcc a b h c - projIcc a b h d| ≤ |c - d|$$
Lean4
theorem abs_sub_addNSMul_le (hδ : 0 ≤ δ) {t : Icc a b} (n : ℕ) (ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))) :
(|t - addNSMul h δ n| : α) ≤ δ :=
calc
(|t - addNSMul h δ n| : α) = t - addNSMul h δ n := abs_eq_self.2 <| sub_nonneg.2 ht.1
_ ≤ projIcc a b h (a + (n + 1) • δ) - addNSMul h δ n := by apply sub_le_sub_right; exact ht.2
_ ≤ (|projIcc a b h (a + (n + 1) • δ) - addNSMul h δ n| : α) := (le_abs_self _)
_ ≤ |a + (n + 1) • δ - (a + n • δ)| := (abs_projIcc_sub_projIcc h)
_ ≤ δ := by
rw [add_sub_add_comm, sub_self, zero_add, succ_nsmul', add_sub_cancel_right]
exact (abs_eq_self.mpr hδ).le
