affineSpan — Mathlib

English

The affine span of a set s is the smallest affine subspace containing s.

Русский

Афинное span множества s есть наименьшее афинное подпространство, содержащее s.

LaTeX

$$$\\text{affineSpan}_k(s) \\,=\\, \\text{the smallest affine subspace containing } s$$$

Lean4

/-- The affine span of a set of points is the smallest affine subspace containing those points.
(Actually defined here in terms of spans in modules.) -/
def affineSpan (s : Set P) : AffineSubspace k P
    where
  carrier := spanPoints k s
  smul_vsub_vadd_mem c _ _ _ hp₁ hp₂
    hp₃ :=
    vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan k hp₃
      ((vectorSpan k s).smul_mem c (vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints k hp₁ hp₂))

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