linearIndependent_le_span — Mathlib

English

In a module M, the size of any LI family is bounded by the size of any basis of M (under strong rank condition).

Русский

В модуле M размер любой линейно независимой семьи ограничен размером базиса M (при условии сильного ранга).

LaTeX

$$$\#\{\text{LI family}\} \le \#\text{basis}$ under SR condition.$$

Lean4

/-- If `R` satisfies the strong rank condition,
then for any linearly independent family `v : ι → M`
and any finite spanning set `w : Set M`,
the cardinality of `ι` is bounded by the cardinality of `w`.
-/
theorem linearIndependent_le_span {ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype w]
    (s : span R w = ⊤) : #ι ≤ Fintype.card w :=
  by
  apply linearIndependent_le_span' v i w
  rw [s]
  exact le_top

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