span_lt_of_subset_of_card_lt_finrank

English

If s is a finite subset of M contained in t, and the size of s is smaller than the dimension of t, then the span of s is strictly contained in t.

Русский

Если s — конечное подмножество M, содержащееся в t, и размер s меньше размерности t, то span(s) строго меньше t.

LaTeX

$$$(s \subseteq t) \land (|s| < \operatorname{finrank}_R(t)) \Rightarrow \operatorname{span}_R(s) < t$$$

Lean4

theorem span_lt_of_subset_of_card_lt_finrank {s : Set M} [Fintype s] {t : Submodule R M} (subset : s ⊆ t)
    (card_lt : s.toFinset.card < finrank R t) : span R s < t :=
  lt_of_le_of_finrank_lt_finrank (span_le.mpr subset) (lt_of_le_of_lt (finrank_span_le_card _) card_lt)

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