genEigenspace_eq_genEigenspace_finrank_of_le

English

If finrank K V ≤ k then f.genEigenspace μ k = f.genEigenspace μ (finrank K V).

Русский

Если размерность пространства не больше k, то все обобщённые эйгенпространства с экспонентами k и finrank_K V совпадают.

LaTeX

$$$\text{If } \operatorname{finrank} K V \le k,\; f.\text{genEigenspace } \mu k = f.\text{genEigenspace } \mu (\operatorname{finrank} K V)$$$

Lean4

/-- Generalized eigenspaces for exponents at least `finrank K V` are equal to each other. -/
theorem genEigenspace_eq_genEigenspace_finrank_of_le [FiniteDimensional K V] (f : End K V) (μ : K) {k : ℕ}
    (hk : finrank K V ≤ k) : f.genEigenspace μ k = f.genEigenspace μ (finrank K V) :=
  le_antisymm (genEigenspace_le_genEigenspace_finrank _ _ _) ((f.genEigenspace μ).monotone <| by simpa using hk)

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