English
If hi is affine independent and s.image p lies in sp with finite dimension of sp.direction, and card s equals finrank sp.direction + 1, then affineSpan k (s.image p) equals sp.
Русский
Если Hi аффинно независим и образ s image p лежит в sp с конечной размерностью направления sp.direction, и |s| = finrank sp.direction + 1, тогда affineSpan k (s.image p) = sp.
LaTeX
$$$\text{AffineIndependent}_k(p) \Rightarrow (\operatorname{affineSpan}_k(\operatorname{image}(p,s)) \le sp) \Rightarrow \#s = \operatorname{finrank}_k(sp.direction) + 1 \Rightarrow \operatorname{affineSpan}_k(\operatorname{image}(p,s)) = sp$$$
Lean4
/-- If the `affineSpan` of a finite subset of an affinely independent
family lies in an affine subspace whose direction has dimension one
less than its cardinality, it equals that subspace. -/
theorem affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one [DecidableEq P] {p : ι → P}
(hi : AffineIndependent k p) {s : Finset ι} {sp : AffineSubspace k P} [FiniteDimensional k sp.direction]
(hle : affineSpan k (s.image p : Set P) ≤ sp) (hc : #s = finrank k sp.direction + 1) :
affineSpan k (s.image p : Set P) = sp :=
by
have hn : s.Nonempty := by
rw [← Finset.card_pos, hc]
apply Nat.succ_pos
refine eq_of_direction_eq_of_nonempty_of_le ?_ ((hn.image p).to_set.affineSpan k) hle
have hd := direction_le hle
rw [direction_affineSpan] at hd ⊢
exact hi.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hd hc
