English
For i-th coordinate update, the image of the segment [x1 —[𝕜] x2] under the update map equals the segment between the updated endpoints.
Русский
Для обновления i-й координаты образ сегмента [x1 —[𝕜] x2] равен сегменту между обновленными точками.
LaTeX
$$$$\operatorname{update}(y,i)'' [x_1 -[\mathbb{k}] x_2] = [\operatorname{update}(y,i)\, x_1 -[\mathbb{k}] \operatorname{update}(y,i)\, x_2].$$$$
Lean4
theorem image_update_segment (i : ι) (x₁ x₂ : M i) (y : ∀ i, M i) :
update y i '' [x₁ -[𝕜] x₂] = [update y i x₁ -[𝕜] update y i x₂] :=
by
rw [segment_eq_image₂, segment_eq_image₂, image_image]
refine EqOn.image_eq fun a ha ↦ ?_
simp only [← update_smul, ← update_add, Convex.combo_self ha.2.2]
