direction — Mathlib

English

The direction of an affine subspace equals the vectorSpan of its point-set.

Русский

Направление аффинного подпространства равно vectorSpan его множества точек.

LaTeX

$$$s.direction = vectorSpan\\, k \\ (s : Set\\ P)$$$

Lean4

/-- The direction of an affine subspace is the submodule spanned by
the pairwise differences of points.  (Except in the case of an empty
affine subspace, where the direction is the zero submodule, every
vector in the direction is the difference of two points in the affine
subspace.) -/
def direction (s : AffineSubspace k P) : Submodule k V :=
  vectorSpan k (s : Set P)

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