segment_eq_image₂ — Mathlib

English

The segment from x to y is the image of the map θ ↦ (1−θ)x + θy with θ in [0,1].

Русский

Отрезок от x до y является образом отображения θ ↦ (1−θ)x + θy при θ ∈ [0,1].

LaTeX

$$$[x -[𝕜] y] = \\{ (1-\\theta) x + \\theta y : \\theta \\in [0,1] \\}$$$

Lean4

theorem segment_eq_image₂ (x y : E) :
    [x -[𝕜] y] = (fun p : 𝕜 × 𝕜 => p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} := by
  simp only [segment, image, Prod.exists, mem_setOf_eq, and_assoc]

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