segment — Mathlib

English

The segment between points x and y in a vector space consists of all convex combinations a x + b y where a,b ≥ 0 and a + b = 1, i.e., all usual line segments between x and y.

Русский

Отрезок между точками x и y векторного пространства состоит из всех выпуклых комбинаций a x + b y, где a,b ≥ 0 и a + b = 1.

LaTeX

$$$[x -[𝕜] y] := \\{ z \\in E : \\exists a,b: 𝕜, 0 \\le a, 0 \\le b, a+b=1, a\\cdot x + b\\cdot y = z \\}$$$

Lean4

/-- Segments in a vector space. -/
def segment (x y : E) : Set E :=
  {z : E | ∃ a b : 𝕜, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a • x + b • y = z}

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