genEigenspace_eq_iSup_genEigenspace_nat

English

The equality f.genEigenspace μ k equals the iSup over l≤k of f.genEigenspace μ l, seen as an equality of the corresponding order-hom images.

Русский

Равенство f.genEigenspace μ k и iSup по l≤k f.genEigenspace μ l выражено как равенство соответствующих образов порядок-гомологов.

LaTeX

$$$$ f.genEigenspace\\, μ\\, k = \\big\\langle f.genEigenspace\\, μ\\, l \\big\\rangle_{l: \\{l: \\mathbb{N} \\;|\\; l \\le k\\}}. $$$$

Lean4

theorem genEigenspace_eq_iSup_genEigenspace_nat (f : End R M) (μ : R) (k : ℕ∞) :
    f.genEigenspace μ k = ⨆ l : { l : ℕ // l ≤ k }, f.genEigenspace μ l := by
  simp_rw [genEigenspace_nat, genEigenspace, OrderHom.coe_mk, iSup_subtype]

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