English
The image of the right coordinate under the segment mapping equals the segment between (x1,y) and (x2,y).
Русский
Образ правой координаты под отображением сегмента равен сегменту между (x1,y) и (x2,y).
LaTeX
$$$ (\lambda y).(x,y) '' [x_{1} -[\mathbb{k}] x_{2}] = [ (x_{1},y) -[\mathbb{k}] (x_{2},y) ] $$$
Lean4
theorem image_mk_segment_right (x : E) (y₁ y₂ : F) : (fun y => (x, y)) '' [y₁ -[𝕜] y₂] = [(x, y₁) -[𝕜] (x, y₂)] :=
by
rw [segment_eq_image₂, segment_eq_image₂, image_image]
refine EqOn.image_eq fun a ha ↦ ?_
simp [Convex.combo_self ha.2.2]