English
Let k be a division ring, V a finite-dimensional k-vector space, P an affine space over V, and ι a finite index set. If p : ι → P is affinely independent and sp ⊂ P is an affine subspace whose direction has dimension dim sp.direction, and affineSpan k (range p) lies inside sp with card(ι) = finrank k sp.direction + 1, then affineSpan k (range p) = sp.
Русский
Пусть k — делимый кольцевой, V — конечномерное векторное пространство над k, P — аффинное пространство над V, и ι — конечное множество индексов. Пусть p : ι → P ортогонально независимо распределено; sp — аффинное подпространство P, направление которого имеет размерность dim sp.direction. Если афинное пространство, порождаемое p, вложено в sp и card(ι) = finrank k sp.direction + 1, то афинное развёртывание affineSpan k (range p) совпадает с sp.
LaTeX
$$$\Bigl(\text{AffineIndependent}_k(p) \wedge \ affineSpan_k(\{p(i) : i \in \iota\}) \le sp \wedge |\iota| = \operatorname{finrank} k\; sp.direction + 1\Bigr) \\Rightarrow \ affineSpan_k(\{p(i) : i \in \iota\}) = sp.$$$
Lean4
/-- If the `affineSpan` of a finite affinely independent family lies
in an affine subspace whose direction has dimension one less than its
cardinality, it equals that subspace. -/
theorem affineSpan_eq_of_le_of_card_eq_finrank_add_one [Fintype ι] {p : ι → P} (hi : AffineIndependent k p)
{sp : AffineSubspace k P} [FiniteDimensional k sp.direction] (hle : affineSpan k (Set.range p) ≤ sp)
(hc : Fintype.card ι = finrank k sp.direction + 1) : affineSpan k (Set.range p) = sp := by
classical
rw [← Finset.card_univ] at hc
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image] at hle ⊢
exact hi.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc
