finrank_vectorSpan_range_le — Mathlib

English

For a finite index set, the vector span of the range has dimension card − 1, i.e., finrank + 1 = card.

Русский

Для конечного множества индексов размерность vectorSpan образа равна кардиналу минус единица.

LaTeX

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

Lean4

/-- The `vectorSpan` of an indexed family of `n + 1` points has
dimension at most `n`. -/
theorem finrank_vectorSpan_range_le [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 1) :
    finrank k (vectorSpan k (Set.range p)) ≤ n := by
  classical
  rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
  rw [← Finset.card_univ] at hc
  exact finrank_vectorSpan_image_finset_le _ _ _ hc

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