genEigenspace_top — Mathlib

English

The top generalized eigenspace equals the supremum of all generalized eigenspaces over natural indices.

Русский

Верхнее обобщённое собственное пространство равно супремуму по всем обобщённым пространствам с натуральными индексами.

LaTeX

$$$$ f.genEigenspace\\, μ\\, ⊤ = \\big\\langle f.genEigenspace\\, μ\\, k \\Big\\rangle_{k \\in \\mathbb{N}}. $$$$

Lean4

theorem genEigenspace_top (f : End R M) (μ : R) : f.genEigenspace μ ⊤ = ⨆ k : ℕ, f.genEigenspace μ k :=
  by
  rw [genEigenspace_eq_iSup_genEigenspace_nat, iSup_subtype]
  simp only [le_top, iSup_pos]

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