case h.e'_3.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.93217
G : Type ?u.93220
ι : Type ?u.93223
π : ι → Type ?u.93228
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ ↑(AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.93217
G : Type ?u.93220
ι : Type ?u.93223
π : ι → Type ?u.93228
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
⊢ openSegment 𝕜 x y = ↑(AffineMap.lineMap x y) '' Ioo 0 1
convert openSegment_eq_image 𝕜 x y using 2
no goals
case h.e'_3.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.93217
G : Type ?u.93220
ι : Type ?u.93223
π : ι → Type ?u.93228
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ ↑(AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y
exact AffineMap.lineMap_apply_module _ _ _