span — Mathlib

English

The span of a set of projective points is a subspace of V.

Русский

Обобщение множества точек в проективном пространстве образует подпространство V.

LaTeX

$$$\text{span}(S) \text{ является подпространством } V$$$

Lean4

/-- The span of a set of points in projective space is a subspace. -/
def span (S : Set (ℙ K V)) : Subspace K V where
  carrier := spanCarrier S
  mem_add' v w hv hw hvw := spanCarrier.mem_add v w hv hw hvw

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