no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.219178
β : Type ?u.219181
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ MapsTo (↑(AffineMap.lineMap x y)) (Icc 0 1) s
simpa only [mapsTo', segment_eq_image_lineMap] using h.segment_subset hx hy