English
Let f be an endomorphism of a finite-dimensional vector space over a field K. If the supremum over μ of genEigenspace μ k equals the entire space, then f possesses an eigenvalue μ for some μ ∈ K.
Русский
Пусть f — отображение на конечномерном векторном пространстве над полем K. Если верхняя грань по μ из сумм genEigenspace μ k равна всему пространству, то существует μ такое, что f имеет собственное значение μ.
LaTeX
$$$\\langle \\text{hf}, k \\rangle:$ if $\\bigvee_{\\mu} \\; f.{\\text{genEigenspace}}(\\mu, k) = ⊤$, then $\\exists \\mu, f.HasEigenvalue(\\mu)$.$$
Lean4
theorem exists_hasEigenvalue_of_genEigenspace_eq_top [Nontrivial M] {f : End R M} (k : ℕ∞)
(hf : ⨆ μ, f.genEigenspace μ k = ⊤) : ∃ μ, f.HasEigenvalue μ :=
by
suffices ∃ μ, f.HasUnifEigenvalue μ k by
peel this with μ hμ
exact HasUnifEigenvalue.lt zero_lt_one hμ
simp [HasUnifEigenvalue, ← not_forall, ← iSup_eq_bot, hf]
-- This is Lemma 5.21 of [axler2015], although we are no longer following that proof.
