finrank_vectorSpan_range_add_one_le

English

For any indexed family, the vector span of the range has dimension at most card(ι)−1 when ι is finite.

Русский

Для любой индексированной семьи размерность vectorSpan(Set.range p) не превосходит card(ι)−1.

LaTeX

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

Lean4

/-- The `vectorSpan` of an indexed family of `n + 1` points has dimension at most `n`. -/
theorem finrank_vectorSpan_range_add_one_le [Fintype ι] [Nonempty ι] (p : ι → P) :
    finrank k (vectorSpan k (Set.range p)) + 1 ≤ Fintype.card ι :=
  (le_tsub_iff_right <| Nat.succ_le_iff.2 Fintype.card_pos).1 <|
    finrank_vectorSpan_range_le _ _ (tsub_add_cancel_of_le <| Nat.succ_le_iff.2 Fintype.card_pos).symm

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