English
For an affinely independent family p and a finite subset s of indices, the dimension of the vector span of s.image p equals card(s) minus 1.
Русский
Для аффинно независимой семьи p и конечного множества индексов s размерность vectorSpan( s.image p ) равна card(s)−1.
LaTeX
$$$\operatorname{finrank}_k\bigl(\operatorname{vectorSpan}_k(\operatorname{image}(p,s))\bigr) = |s| - 1$$$
Lean4
/-- The `vectorSpan` of `n + 1` points in an indexed family has
dimension at most `n`. -/
theorem finrank_vectorSpan_image_finset_le [DecidableEq P] (p : ι → P) (s : Finset ι) {n : ℕ} (hc : #s = n + 1) :
finrank k (vectorSpan k (s.image p : Set P)) ≤ n := by
classical
have hn : (s.image p).Nonempty := by
rw [Finset.image_nonempty, ← Finset.card_pos, hc]
apply Nat.succ_pos
rcases hn with ⟨p₁, hp₁⟩
rw [vectorSpan_eq_span_vsub_finset_right_ne k hp₁]
refine le_trans (finrank_span_finset_le_card (((s.image p).erase p₁).image fun p => p -ᵥ p₁)) ?_
rw [Finset.card_image_of_injective _ (vsub_left_injective p₁), Finset.card_erase_of_mem hp₁, tsub_le_iff_right, ← hc]
apply Finset.card_image_le
