finrank_lt_finrank_of_lt — Mathlib

English

Let s ⊂ t be submodules of a finite-dimensional vector space V over a division ring K. Then finrank_K(s) < finrank_K(t).

Русский

Пусть s ⊂ t — подпространые пространства над полем K в конечномерном векторном пространстве V. Тогда размерности удовлетворяют finrank_K(s) < finrank_K(t).

LaTeX

$$$s < t \\Rightarrow \\operatorname{finrank}_K s < \\operatorname{finrank}_K t$$$

Lean4

theorem finrank_lt_finrank_of_lt {s t : Submodule K V} [FiniteDimensional K t] (hst : s < t) :
    finrank K s < finrank K t :=
  (comapSubtypeEquivOfLe hst.le).finrank_eq.symm.trans_lt <| finrank_lt <| by simp [not_le_of_gt hst]

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