segment_eq_image' — Mathlib

English

The closed segment between x and y is the set of all points x + θ(y − x) with θ in [0,1].

Русский

Замкнутый сегмент между x и y состоит из всех точек x + θ(y − x) при θ ∈ [0,1].

LaTeX

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

Lean4

theorem segment_eq_image' (x y : E) : [x -[𝕜] y] = (fun θ : 𝕜 => x + θ • (y - x)) '' Icc (0 : 𝕜) 1 :=
  by
  convert segment_eq_image 𝕜 x y using 2
  simp only [smul_sub, sub_smul, one_smul]
  abel

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