eigenspace_le_maxGenEigenspace — Mathlib

English

For any f, μ, the eigenspace with eigenvalue μ is contained in the maximal generalized eigenspace for μ.

Русский

Для всякого f, μ соответствующее эйгенпространство содержится в максимальном обобщённом эйгенпространстве для μ.

LaTeX

$$$f.eigenspace(\\mu) \\le f.maxGenEigenspace(\\mu).$$$

Lean4

theorem eigenspace_le_maxGenEigenspace {f : End R M} {μ : R} : f.eigenspace μ ≤ f.maxGenEigenspace μ :=
  (f.genEigenspace _).monotone <| OrderTop.le_top _

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