English
Let f be a linear endomorphism and μ ∈ R. If μ is a generalized eigenvalue of f with exponent k and k ≤ m (for ENat), then μ is a generalized eigenvalue of f with exponent m.
Русский
Пусть f — линейный эндоморфизм, μ ∈ R. Если μ является обобщённым собственным значением f с порядком k и k ≤ m, то μ является обобщённым собственным значением f с порядком m.
LaTeX
$$$\forall f: \mathrm{End}_R M,\; \mu \in R,\; k,m \in \mathbb{N}_\infty,\; k \le m \Rightarrow \text{HasUnifEigenvalue } f\, \mu\, k \Rightarrow \text{HasUnifEigenvalue } f\, \mu\, m$$$
Lean4
/-- A generalized eigenvalue for some exponent `k` is also
a generalized eigenvalue for exponents larger than `k`. -/
theorem le {f : End R M} {μ : R} {k m : ℕ∞} (hm : k ≤ m) (hk : f.HasUnifEigenvalue μ k) : f.HasUnifEigenvalue μ m :=
by
unfold HasUnifEigenvalue at *
contrapose! hk
rw [← le_bot_iff, ← hk]
exact (f.genEigenspace _).monotone hm
