eq_iSup_inf_genEigenspace — Mathlib

English

If p is an invariant subspace under f, and the genEigenspace sup is top in V, then the restricted endomorphism has genEigenspace top as well; i.e., the generalized eigenspaces of the restriction span the whole p.

Русский

Если p инвариантно относительно f и верхняя грань по знаку генEigenspace достигает топа, то ограничение отображения на p сохраняет это свойство.

LaTeX

$$$\\text{If } h:\\forall x\\in p, f x\\in p, \\text{ and } ⨆_{\\mu} f.genEigenspace(μ, k) = ⊤, \\; ⨆_{\\mu} (Module.End.genEigenspace (LinearMap.restrict f h)) (μ, k) = ⊤.$$$

Lean4

theorem eq_iSup_inf_genEigenspace [FiniteDimensional K V] (k : ℕ∞) (h : ∀ x ∈ p, f x ∈ p)
    (h' : ⨆ μ, f.genEigenspace μ k = ⊤) : p = ⨆ μ, p ⊓ f.genEigenspace μ k := by
  rw [← inf_iSup_genEigenspace h, h', inf_top_eq]

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