finrank_mono — Mathlib

English

If s ⊆ t are subsets of V, then the finrank of the span of s is less than or equal to the finrank of the span of t.

Русский

Если s содержится в t и обе подмножества, то размерности спана элементов s не превосходят размерности спана элементов t.

LaTeX

$$$s \subseteq t \implies \operatorname{finrank}_K(\operatorname{Span}(s)) \le \operatorname{finrank}_K(\operatorname{Span}(t))$$$

Lean4

theorem finrank_mono [FiniteDimensional K V] {s t : Set V} (h : s ⊆ t) : s.finrank K ≤ t.finrank K :=
  Submodule.finrank_mono (span_mono h)

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