card_le_finrank_succ — Mathlib

English

For an affinely independent family p, the cardinality of ι is at most finrank k (vectorSpan k (Set.range p)) + 1.

Русский

Для аффинно независимой семьи p кардинал множества индексов не превосходит размерности vectorSpan плюс единица.

LaTeX

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

Lean4

theorem card_le_finrank_succ [Fintype ι] {p : ι → P} (hp : AffineIndependent k p) :
    Fintype.card ι ≤ Module.finrank k (vectorSpan k (Set.range p)) + 1 :=
  by
  cases isEmpty_or_nonempty ι
  · simp [Fintype.card_eq_zero]
  rw [← tsub_le_iff_right]
  exact
    (affineIndependent_iff_le_finrank_vectorSpan _ _
          (tsub_add_cancel_of_le <| Nat.one_le_iff_ne_zero.2 Fintype.card_ne_zero).symm).1
      hp

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