English
The distance between two next-curves starting at x and y is exactly the distance between the starting points, i.e., the next map is an isometry with respect to the base point.
Русский
Расстояние между двумя кривыми next, начинающимися в x и y, равно расстоянию между точками x и y; оператор next сохраняет расстояние (является изометрией).
LaTeX
$$$\\operatorname{dist}\\big(\\text{next } hf\\ hx\\ α,\\ \\text{next } hf\\ hy\\ α\\big) = \\operatorname{dist}(x,y).$$$
Lean4
/-- A key step in the base case of `exists_forall_closedBall_funSpace_dist_le_mul` -/
theorem dist_next_next (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ closedBall x₀ r) (hy : y ∈ closedBall x₀ r)
(α : FunSpace t₀ x₀ r L) : dist (next hf hx α) (next hf hy α) = dist x y :=
by
have : Nonempty (Icc tmin tmax) :=
⟨t₀⟩ -- needed for `ciSup_const`
rw [← MetricSpace.isometry_induced FunSpace.toContinuousMap FunSpace.toContinuousMap.injective |>.dist_eq,
dist_eq_norm, ContinuousMap.norm_eq_iSup_norm]
simp [add_sub_add_right_eq_sub, dist_eq_norm]
