image_mk_openSegment_right — Mathlib

English

The image of the right coordinate under the openSegment mapping equals the openSegment between (x,y1) and (x,y2).

Русский

Образ правой координаты под отображением открытого сегмента равен открытому сегменту между (x,y1) и (x,y2).

LaTeX

$$$ (\lambda y).(x,y) '' openSegment_{\mathbb{k}}(y_{1},y_{2}) = openSegment_{\mathbb{k}}((x,y_{1}),(x,y_{2})) $$$

Lean4

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

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