spanPoints — Mathlib

English

The spanPoints of a set s consists exactly of all points that can be written as a point from s translated by a vector in the vectorSpan of s.

Русский

Область spanPoints множества s состоит ровно из всех точек, которые можно получить как точку из s, сдвинутую на вектор из vectorSpan k s.

LaTeX

$$$spanPoints(k,s)=\\{p\\in P : ∃ p_1\\in s, ∃ v\\in vectorSpan\\, k\, s,\\ p = v +_{\\mathrm{v}} p_1\\}$$$

Lean4

/-- The points in the affine span of a (possibly empty) set of points. Use `affineSpan` instead to
get an `AffineSubspace k P`. -/
def spanPoints (s : Set P) : Set P :=
  {p | ∃ p₁ ∈ s, ∃ v ∈ vectorSpan k s, p = v +ᵥ p₁}

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