linearIndependent_le_span_finset — Mathlib

English

A bound between LI-family size and the size of a spanning set holds in the general setting with strong rank condition.

Русский

Общее положение о размере LI-семейства и порождающего множества при SR.

LaTeX

$$$|\kappa| \le |w|$ under the given conditions.$$

Lean4

/-- A version of `linearIndependent_le_span` for `Finset`. -/
theorem linearIndependent_le_span_finset {ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Finset M)
    (s : span R (w : Set M) = ⊤) : #ι ≤ w.card := by
  simpa only [Finset.coe_sort_coe, Fintype.card_coe] using linearIndependent_le_span v i w s

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