English
For finite-dimensional K-vector spaces V and endomorphism f, f.genEigenspace(μ,k) ≤ f.genEigenspace(μ, finrank K V).
Русский
Для конечномерного пространства V над K и эндоморфизма f, подпространство f.genEigenspace(μ,k) содержится в f.genEigenspace(μ, finrank K V).
LaTeX
$$$f\text{.genEigenspace} \; \mu \; k \le f\text{.genEigenspace} \; \mu \; \operatorname{finrank} K V$$$
Lean4
/-- Every generalized eigenvector is a generalized eigenvector for exponent `finrank K V`.
(Lemma 8.11 of [axler2015]) -/
theorem genEigenspace_le_genEigenspace_finrank [FiniteDimensional K V] (f : End K V) (μ : K) (k : ℕ∞) :
f.genEigenspace μ k ≤ f.genEigenspace μ (finrank K V) := by
calc
f.genEigenspace μ k ≤ f.genEigenspace μ ⊤ := (f.genEigenspace _).monotone le_top
_ ≤ f.genEigenspace μ (finrank K V) :=
by
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
exact (f.genEigenspace _).monotone <| by simpa using maxUnifEigenspaceIndex_le_finrank f μ
