lt_top_of_finrank_lt_finrank — Mathlib

English

If a submodule s has strictly smaller finrank than M, then s is a proper submodule, i.e., s < ⊤.

Русский

Если подпространство s имеет существенно меньшую размерность, чем M, то s является proper-subspace: s < ⊤.

LaTeX

$$$ \\operatorname{finrank} R\,s < \\operatorname{finrank} R\,M \\Rightarrow s < \\top. $$$

Lean4

theorem lt_top_of_finrank_lt_finrank {s : Submodule R M} (lt : finrank R s < finrank R M) : s < ⊤ :=
  by
  rw [← finrank_top R M] at lt
  exact lt_of_le_of_finrank_lt_finrank le_top lt

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