openSegment_eq_image_lineMap — Mathlib

English

Similarly, openSegment equals the image of the line map restricted to Ioo(0,1).

Русский

Открытый сегмент равен образу линейного отображения ограниченного до Ioo(0,1).

LaTeX

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

Lean4

theorem openSegment_eq_image_lineMap (x y : E) : openSegment 𝕜 x y = AffineMap.lineMap x y '' Ioo (0 : 𝕜) 1 :=
  by
  convert openSegment_eq_image 𝕜 x y using 2
  exact AffineMap.lineMap_apply_module _ _ _

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