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