no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.12738
G : Type ?u.12741
ι : Type ?u.12744
π : ι → Type ?u.12749
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
x✝ y✝ x y : E
⊢ [x-[𝕜]y] = (fun p => p.fst • x + p.snd • y) '' {p | 0 ≤ p.fst ∧ 0 ≤ p.snd ∧ p.fst + p.snd = 1}
simp only [segment, image, Prod.exists, mem_setOf_eq, exists_prop, and_assoc]