openSegment_eq_image₂ — Mathlib

English

The open segment between x and y is the image of the map p ↦ p1 x + p2 y with p ranging over {p : 𝕜 × 𝕜 | p1 > 0, p2 > 0, p1 + p2 = 1}.

Русский

Открытый сегмент между x и y является образом отображения p1 x + p2 y, где p1>0, p2>0 и p1+p2=1.

LaTeX

$$$openSegment \\; 𝕜\\; x\\; y = \\{ p_1 x + p_2 y : (p_1,p_2) \\in 𝕜\\times 𝕜,\\ p_1>0,\\ p_2>0,\\ p_1+p_2=1 \\}$$$

Lean4

theorem openSegment_eq_image₂ (x y : E) :
    openSegment 𝕜 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 [openSegment, image, Prod.exists, mem_setOf_eq, and_assoc]

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