finrank_vectorSpan — Mathlib

English

For a finite affinely independent family, the vector span has dimension one less than its cardinality.

Русский

Для конечной аффинно независимой семьи размерность vectorSpan на единицу меньше ее мощности.

LaTeX

$$$\operatorname{finrank}_k\bigl(\operatorname{vectorSpan}_k(\operatorname{SetRange}(p))\bigr) + 1 = |\iota|$$$

Lean4

/-- The `vectorSpan` of a finite affinely independent family has
dimension one less than its cardinality. -/
theorem finrank_vectorSpan [Fintype ι] {p : ι → P} (hi : AffineIndependent k p) {n : ℕ} (hc : Fintype.card ι = n + 1) :
    finrank k (vectorSpan k (Set.range p)) = n := by
  classical
  rw [← Finset.card_univ] at hc
  rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
  exact hi.finrank_vectorSpan_image_finset hc

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