height_strictMono — Mathlib

English

The height function on submodules is strictly monotone: if N ⊊ P then height(N) < height(P).

Русский

Функция высоты на подмодулях строго монотонна: если N ⊊ P, тогда height(N) < height(P).

LaTeX

$$$\text{Height}: \text{Submodule}_R M \to \mathbb{N}_\infty$ is strictly monotone: \forall N \subsetneq P,\ height(N) < height(P).$$$

Lean4

theorem height_strictMono [IsArtinian R M] [IsNoetherian R M] : StrictMono (Order.height : Submodule R M → ℕ∞) :=
  fun N _ h ↦ Order.height_strictMono h N.height_lt_top

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