eq_of_le_of_finrank_eq — Mathlib

English

If S1 ⊆ S2 and finrank_K S1 = finrank_K S₂, then S1 = S2.

Русский

Если S1 ⊆ S2 и dim_K S1 = dim_K S2, тогда S1 = S2.

LaTeX

$$$S_1 \le S_2 \land \operatorname{finrank}_K S_1 = \operatorname{finrank}_K S_2 \Rightarrow S_1 = S_2$$$

Lean4

/-- If a submodule is contained in a finite-dimensional
submodule with the same dimension, they are equal. -/
theorem eq_of_le_of_finrank_eq {S₁ S₂ : Submodule K V} [FiniteDimensional K S₂] (hle : S₁ ≤ S₂)
    (hd : finrank K S₁ = finrank K S₂) : S₁ = S₂ :=
  eq_of_le_of_finrank_le hle hd.ge

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