English
Updating the i-th coordinate maps the open segment between x1 and x2 to the open segment between the updated endpoints.
Русский
Обновление i-й координаты отображает открытый сегмент между x1 и x2 в открытый сегмент между обновленными точками.
LaTeX
$$$$\operatorname{update}(y,i)'' \operatorname{openSegment}_{\mathbb{k}}(x_1,x_2) = \operatorname{openSegment}_{\mathbb{k}}(\operatorname{update}(y,i)x_1, \operatorname{update}(y,i)x_2).$$$$
Lean4
theorem image_update_openSegment (i : ι) (x₁ x₂ : M i) (y : ∀ i, M i) :
update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (update y i x₁) (update y i x₂) :=
by
rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]
refine EqOn.image_eq fun a ha ↦ ?_
simp only [← update_smul, ← update_add, Convex.combo_self ha.2.2]
