vectorSpan — Mathlib

English

The vectorSpan of a set s is the submodule generated by all differences of points in s, i.e., span of s − s.

Русский

VectorSpan множества s является подпростоянием, порожденным всеми разностями точек из s, то есть span{ s − s }.

LaTeX

$$$ \\operatorname{vectorSpan} \\ k\\ s = \\operatorname{Submodule}.span\\ k (s -\\!\\!\\! s) $$$

Lean4

/-- The submodule spanning the differences of a (possibly empty) set of points. -/
def vectorSpan (s : Set P) : Submodule k V :=
  Submodule.span k (s -ᵥ s)

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