mem_genEigenspace_top — Mathlib

English

The top generalized eigenspace equals the supremum of the generalized eigenspaces over all natural exponents: f.genEigenspace μ ⊤ = ⨆ k:ℕ, f.genEigenspace μ k.

Русский

Верхнее обобщённое собственное пространство равно супремуму по всем натуральным степеням: f.genEigenspace μ ⊤ = ⨆ k, f.genEigenspace μ k.

LaTeX

$$$$ f.genEigenspace\\, μ\\, ⊤ = \\bigSup_{k \\in \\mathbb{N}} f.genEigenspace\\, μ\\, k. $$$$

Lean4

theorem mem_genEigenspace_top {f : End R M} {μ : R} {x : M} :
    x ∈ f.genEigenspace μ ⊤ ↔ ∃ k : ℕ, x ∈ LinearMap.ker ((f - μ • 1) ^ k) := by simp [mem_genEigenspace]

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