segment_eq_image — Mathlib

English

The segment from x to y equals the image of θ ↦ (1−θ)x + θy for θ ∈ Icc(0,1).

Русский

Отрезок от x до y равен образу θ ↦ (1−θ)x + θy для θ ∈ Icc(0,1).

LaTeX

$$$[x -[𝕜] y] = (\\theta \\mapsto (1-\\theta) x + \\theta y) '' Icc(0,1)$$$

Lean4

theorem segment_eq_image (x y : E) : [x -[𝕜] y] = (fun θ : 𝕜 => (1 - θ) • x + θ • y) '' Icc (0 : 𝕜) 1 :=
  Set.ext fun _ =>
    ⟨fun ⟨a, b, ha, hb, hab, hz⟩ =>
      ⟨b, ⟨hb, hab ▸ le_add_of_nonneg_left ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel_right]⟩,
      fun ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩ => ⟨1 - θ, θ, sub_nonneg.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩

Похожие утверждения