finrank_le — Mathlib

English

If t is a finite submodule of M, then finrank_R s ≤ finrank_R t whenever s ≤ t.

Русский

Пусть t — конечное подпространство в M. Тогда, если s ≤ t, то finrank_R s ≤ finrank_R t.

LaTeX

$$$ s \\le t \\Rightarrow \\operatorname{finrank} R s \\le \\operatorname{finrank} R t \quad\\text{(with } [Module.Finite R t]). $$$

Lean4

/-- The dimension of a submodule is bounded by the dimension of the ambient space. -/
theorem finrank_le [Module.Finite R M] (s : Submodule R M) : finrank R s ≤ finrank R M :=
  toNat_le_toNat (Submodule.rank_le s) (rank_lt_aleph0 _ _)

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