𝕜 : Type u_1
E : Type u_2
F : Type ?u.158410
G : Type ?u.158413
ι : Type ?u.158416
π : ι → Type ?u.158421
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ midpoint 𝕜 x y ∈ ↑(AffineMap.lineMap x y) '' Icc 0 1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.158410
G : Type ?u.158413
ι : Type ?u.158416
π : ι → Type ?u.158421
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ midpoint 𝕜 x y ∈ [x-[𝕜]y]
rw [segment_eq_image_lineMap]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.158410
G : Type ?u.158413
ι : Type ?u.158416
π : ι → Type ?u.158421
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ midpoint 𝕜 x y ∈ ↑(AffineMap.lineMap x y) '' Icc 0 1
exact ⟨⅟ 2, ⟨invOf_nonneg.mpr zero_le_two, invOf_le_one one_le_two⟩, rfl⟩