rank_span_le — Mathlib

English

For any subspace spanned by a set s, its rank does not exceed the cardinality of s.

Русский

Для подпространства, образованного множеством s, ранг не превосходит кардинал множества s.

LaTeX

$$$ \\operatorname{Module.rank} R (\\operatorname{span}_R s) \\leq \\#s. $$$

Lean4

theorem rank_span_le (s : Set M) : Module.rank R (span R s) ≤ #s :=
  by
  rw [Finsupp.span_eq_range_linearCombination, ← lift_strictMono.le_iff_le]
  refine (lift_rank_range_le _).trans ?_
  rw [rank_finsupp_self]
  simp only [lift_lift, le_refl]

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