image_mk_segment_right — Mathlib

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]

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