hasGenEigenvalue_of_hasGenEigenvalue_of_le

English

The iSup of genEigenspace across μ equals maxGenEigenspace; equivalently, sup over μ of genEigenspace μ k equals maxGenEigenspace μ.

Русский

Пусть iSup генерируемого семейства genEigenspace μ над μ совпадает с maxGenEigenspace; то есть супремум по μ равен максимальному эйгенпространству.

LaTeX

$$$\\displaystyle \\big\\lbrace f.genEigenspace(\\mu)\\;:\\; \\mu \\in R\\big\\rbrace _{\\mathrm{iSup}} = \\maxGenEigenspace(f, \\mu).$$$

Lean4

/-- A generalized eigenvalue for some exponent `k` is also
a generalized eigenvalue for exponents larger than `k`. -/
theorem hasGenEigenvalue_of_hasGenEigenvalue_of_le {f : End R M} {μ : R} {k : ℕ} {m : ℕ} (hm : k ≤ m)
    (hk : f.HasGenEigenvalue μ k) : f.HasGenEigenvalue μ m :=
  hk.le <| by simpa using hm

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