English
If S1 ⊆ S₂ are subspaces of V with S₂ finite-dimensional, and finrank_K S₂ ≤ finrank_K S₁, then S1 = S₂.
Русский
Пусть S1 ⊆ S2 — подпространства V; если S2 конечномерно и dim S2 ≤ dim S1, то S1 = S2.
LaTeX
$$$[\operatorname{FiniteDimensional}_K S_2] \Rightarrow (S_1 \le S_2 \Rightarrow \operatorname{finrank}_K S_2 \le \operatorname{finrank}_K S_1 \Rightarrow S_1 = S_2)$$$
Lean4
/-- If a submodule is contained in a finite-dimensional
submodule with the same or smaller dimension, they are equal. -/
theorem eq_of_le_of_finrank_le {S₁ S₂ : Submodule K V} [FiniteDimensional K S₂] (hle : S₁ ≤ S₂)
(hd : finrank K S₂ ≤ finrank K S₁) : S₁ = S₂ :=
by
rw [← LinearEquiv.finrank_eq (Submodule.comapSubtypeEquivOfLe hle)] at hd
exact
le_antisymm hle
(Submodule.comap_subtype_eq_top.1
(eq_top_of_finrank_eq (le_antisymm (comap (Submodule.subtype S₂) S₁).finrank_le hd)))
