eigenspace_restrict_le_eigenspace

English

The eigen space of the restriction f|_p maps into the eigen space of f: (eigenspace of f|_p) under map p is contained in eigenspace of f.

Русский

Эйгенпространство ограничения f на p отображается в эйгенпространство f и вложено в него.

LaTeX

$$$(\\mathrm{eigenspace}(f|_p)\\,\\mu).\\mathrm{map}\\ p.subtype \\le \\mathrm{eigenspace}(f)\\mu$$$

Lean4

/-- If `p` is an invariant submodule of an endomorphism `f`, then the `μ`-eigenspace of the
restriction of `f` to `p` is a submodule of the `μ`-eigenspace of `f`. -/
theorem eigenspace_restrict_le_eigenspace (f : End R M) {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p) (μ : R) :
    (eigenspace (f.restrict hfp) μ).map p.subtype ≤ f.eigenspace μ :=
  by
  rintro a ⟨x, hx, rfl⟩
  simp only [SetLike.mem_coe, mem_eigenspace_iff, LinearMap.restrict_apply] at hx ⊢
  exact congr_arg Subtype.val hx

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