mapsTo_lineMap — Mathlib

English

The segment between two points in a convex set remains in the set under the line map.

Русский

Отрезок между двумя точками выпуклого множества отображается линейной картой внутри множества.

LaTeX

$$$$ \\text{MapsTo}((\\text{AffineMap.lineMap } x y), Icc(0,1), s) $$$$

Lean4

theorem mapsTo_lineMap (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
    MapsTo (AffineMap.lineMap x y) (Icc (0 : 𝕜) 1) s := by
  simpa only [mapsTo_iff_image_subset, segment_eq_image_lineMap] using h.segment_subset hx hy

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