segment_eq_image_lineMap — Mathlib

English

The segment between x and y is the image of the line map t ↦ (1−t)x + ty for t in [0,1].

Русский

Сегмент между x и y есть образ линейного отображения t ↦ (1−t)x + ty при t ∈ [0,1].

LaTeX

$$$$ [x -[\mathbb{K}] y] = \{ (1-t) x + t y : t \in [0,1] \}. $$$$

Lean4

theorem segment_eq_image_lineMap (x y : E) : [x -[𝕜] y] = AffineMap.lineMap x y '' Icc (0 : 𝕜) 1 :=
  by
  convert segment_eq_image 𝕜 x y using 2
  exact AffineMap.lineMap_apply_module _ _ _

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