English
Let E be a vector space over a ring 𝕜 with the usual convex combination structure. The open segment between x and y consists exactly of all convex combinations (1−θ)x + θy with θ in (0,1).
Русский
Пусть E — векторное пространство над кольцом 𝕜. Открытый сегмент между x и y состоит из всех выпуклых комбинаций (1−θ)x + θy при θ ∈ (0,1).
LaTeX
$$$$\operatorname{openSegment}_{\mathbb{K}}(x,y) = \{ (1-\theta) x + \theta y : \theta \in (0,1) \}.$$$$
Lean4
theorem openSegment_eq_image (x y : E) : openSegment 𝕜 x y = (fun θ : 𝕜 => (1 - θ) • x + θ • y) '' Ioo (0 : 𝕜) 1 :=
Set.ext fun _ =>
⟨fun ⟨a, b, ha, hb, hab, hz⟩ =>
⟨b, ⟨hb, hab ▸ lt_add_of_pos_left _ ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel_right]⟩,
fun ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩ => ⟨1 - θ, θ, sub_pos.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩
