finrank_span_le_card — Mathlib

English

The finrank of the span of a Finset is bounded by the cardinality of the Finset.

Русский

Финразмер пространства span от Finset ограничен по размеру самого Finset.

LaTeX

$$$ (s : Finset M) : \\operatorname{Module.rank} R (\\operatorname{span}_R (s : Set M)) \\leq s.card. $$$

Lean4

theorem finrank_span_le_card (s : Set M) [Fintype s] : finrank R (span R s) ≤ s.toFinset.card :=
  finrank_le_of_rank_le (by simpa using rank_span_le (R := R) s)

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