genEigenspace_directed — Mathlib

English

The family of generalized eigenspaces {f.genEigenspace μ l} over l ≤ k is directed by inclusion; i.e., along the natural order on l.

Русский

Семейство обобщённых собственных пространств {f.genEigenspace μ l} по l ≤ k образует направленное по включению семейство.

LaTeX

$$$$ Directed (\\le) (\\lambda l. f.genEigenspace\\, μ\\, l). $$$$

Lean4

theorem genEigenspace_directed {f : End R M} {μ : R} {k : ℕ∞} :
    Directed (· ≤ ·) (fun l : { l : ℕ // l ≤ k } ↦ f.genEigenspace μ l) :=
  by
  have aux : Monotone ((↑) : { l : ℕ // l ≤ k } → ℕ∞) := fun x y h ↦ by simpa using h
  exact ((genEigenspace f μ).monotone.comp aux).directed_le

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