finrank_strictMono — Mathlib

English

The function s ↦ finrank K s on submodules s of a finite-dimensional K-vector space is strictly monotone.

Русский

Функция s ↦ finrank_K s по подпростра́нствам имеет строгую монотонность.

LaTeX

$$$ \\text{StrictMono} \\ f: s \\mapsto \\operatorname{finrank}_K(s) $$$

Lean4

theorem finrank_strictMono [FiniteDimensional K V] : StrictMono fun s : Submodule K V => finrank K s := fun _ _ =>
  finrank_lt_finrank_of_lt

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