image_mk_segment_left — Mathlib

English

The image of the left coordinate under the segment mapping equals the segment between (x1,y) and (x2,y).

Русский

Образ левого координатного компонента под отображением сегмента равен сегменту между (x1,y) и (x2,y).

LaTeX

$$$ (\lambda x).(x,y) '' [x_{1} -[\mathbb{k}] x_{2}] = [ (x_{1},y) -[\mathbb{k}] (x_{2},y) ] $$$

Lean4

theorem image_mk_segment_left (x₁ x₂ : E) (y : F) : (fun x => (x, y)) '' [x₁ -[𝕜] x₂] = [(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]

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