affineSpan_eq_sInf — Mathlib

English

The affine span of a set is the greatest lower bound (infimum) of all affine subspaces containing that set.

Русский

Аффинная оболочка множества является наименьшим сверху слабых ограничений? — точнее: наименьшим субпространством, содержащим данное множество.

LaTeX

$$$\\mathrm{affineSpan}(k,s) = \\inf\\{s' : \\text{AffineSubspace}(k,P) \\mid s \\subseteq s'\\}$$$

Lean4

/-- The affine span is the `sInf` of subspaces containing the given points. -/
theorem affineSpan_eq_sInf (s : Set P) : affineSpan k s = sInf {s' : AffineSubspace k P | s ⊆ s'} :=
  le_antisymm (affineSpan_le_of_subset_coe <| Set.subset_iInter₂ fun _ => id) (sInf_le (subset_spanPoints k _))

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