English
The segment from x to y equals the image of p = (p1,p2) with p1,p2 ≥ 0 and p1+p2 = 1 under the map p ↦ p1 x + p2 y.
Русский
Отрезок от x до y равен образу пары p1,p2 с p1,p2 ≥ 0 и p1+p2=1 под отображением p ↦ p1 x + p2 y.
LaTeX
$$$[x -[𝕜] y] = (p \\mapsto p_1 x + p_2 y) '' \\{ p \\mid p_1, p_2 \\ge 0, p_1 + p_2 = 1 \\}$$$
Lean4
@[simp]
theorem openSegment_same (x : E) : openSegment 𝕜 x x = { x } :=
Set.ext fun z =>
⟨fun ⟨a, b, _, _, hab, hz⟩ => by simpa only [← add_smul, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
fun h : z = x => by
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
refine ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, ?_⟩
rw [← add_smul, add_sub_cancel, one_smul, h]⟩
