image_mk_openSegment_left — Mathlib

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]

Похожие утверждения