iSup_genEigenspace_eq — Mathlib

English

The iSup (supremum) of genEigenspace over k equals the maximal generalized eigenspace.

Русский

Обобщённое эйгенпространство по всем k равно максимальному обобщённому эйгенпространству.

LaTeX

$$$\\big\\lbrace f.genEigenspace(\\mu)\\;:\\; k \\mapsto \\operatorname{submodule} \\;\\,\\,\\_\\ \\big\\rbrace_{k\\in\\mathbb{N}} = \\maxGenEigenspace(f,\\mu).$$$

Lean4

theorem iSup_genEigenspace_eq (f : End R M) (μ : R) : ⨆ k : ℕ, (f.genEigenspace μ) k = f.maxGenEigenspace μ := by
  simp_rw [maxGenEigenspace, genEigenspace_top]

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