span_lt_top_of_card_lt_finrank — Mathlib

English

If s is finite and its elements live in a module of rank greater than its size, then span(s) is a proper submodule of the top.

Русский

Если s — конечное множество и элементы образуют подпространство меньшей размерности, чем пространство, то span(s) является правильной подподмодулем верхнего.

LaTeX

$$$|s| <\operatorname{finrank}_R(M) \Rightarrow \operatorname{span}_R(s) < \top$$$

Lean4

theorem span_lt_top_of_card_lt_finrank {s : Set M} [Fintype s] (card_lt : s.toFinset.card < finrank R M) :
    span R s < ⊤ :=
  lt_top_of_finrank_lt_finrank (lt_of_le_of_lt (finrank_span_le_card _) card_lt)

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