English
Let p: ι → P be affinely independent. For any finite s ⊆ ι, the vector span of s.image p has dimension equal to card(s.image p) − 1.
Русский
Пусть p: ι → P аффинно независимо. Для любого конечного s ⊆ ι размерность vectorSpan(сomponent image) равна |image|−1.
LaTeX
$$$\text{For } hi: \text{AffineIndependent}_k p\ \text{ and } s: \text{Finset } ι,\ \#(s.image p) = n+1 \Rightarrow \operatorname{finrank}_k\bigl( \operatorname{vectorSpan}_k( s.image p )\bigr) = n$$$
Lean4
/-- The `vectorSpan` of a finite subset of an affinely independent
family has dimension one less than its cardinality. -/
theorem finrank_vectorSpan_image_finset [DecidableEq P] {p : ι → P} (hi : AffineIndependent k p) {s : Finset ι} {n : ℕ}
(hc : #s = n + 1) : finrank k (vectorSpan k (s.image p : Set P)) = n := by
classical
have hi' := hi.range.mono (Set.image_subset_range p ↑s)
have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.injective]
have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
rcases hn with ⟨p₁, hp₁⟩
have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton, ← Finset.coe_image, ←
Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image] at hi'
have hc : #(((s.image p).erase p₁).image (· -ᵥ p₁)) = n :=
by
rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
exact Nat.pred_eq_of_eq_succ hc'
rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]
