English
For any a ≤ b and δ, the n-th point produced by addNSMul equals the projection of a + nδ into [a,b].
Русский
Для любых a ≤ b и δ, n‑ая точка, полученная как addNSMul, равна проекции a + nδ на отрезок [a,b].
LaTeX
$$addNSMul h δ n = projIcc a b h (a + n·δ)$$
Lean4
/-- `Set.projIcc` is a contraction. -/
theorem _root_.Set.abs_projIcc_sub_projIcc : (|projIcc a b h c - projIcc a b h d| : α) ≤ |c - d| :=
by
wlog hdc : d ≤ c generalizing c d
· rw [abs_sub_comm, abs_sub_comm c]; exact this (le_of_not_ge hdc)
rw [abs_eq_self.2 (sub_nonneg.2 hdc), abs_eq_self.2 (sub_nonneg.2 <| mod_cast monotone_projIcc h hdc)]
rw [← sub_nonneg] at hdc
refine (max_sub_max_le_max _ _ _ _).trans (max_le (by rwa [sub_self]) ?_)
refine ((le_abs_self _).trans <| abs_min_sub_min_le_max _ _ _ _).trans (max_le ?_ ?_)
· rwa [sub_self, abs_zero]
· exact (abs_eq_self.mpr hdc).le
