affineSpan_nonempty — Mathlib

English

The affine span of a set is nonempty if and only if the set is nonempty.

Русский

Аффинная оболочка множества непусто тогда и только тогда, когда множество непусто.

LaTeX

$$$(\operatorname{affineSpan}(k, s)).\text{Nonempty} \iff s.\text{Nonempty}$$$

Lean4

/-- The affine span of a set is nonempty if and only if that set is. -/
theorem affineSpan_nonempty : (affineSpan k s : Set P).Nonempty ↔ s.Nonempty :=
  spanPoints_nonempty k s

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