subsingleton_of_no_eigenvalue_finiteDimensional

English

If a symmetric operator on a nontrivial finite-dimensional space has no eigenvalues for any scalar μ, then the space is a singleton.

Русский

Если симметричный оператор на ненулевом пространстве конечной размерности не имеет собственных значений для каких-либо скаляров, пространство ничтожно одномерно.

LaTeX

$$If (∀ μ, Module.End.eigenspace(T,μ) = ⊥), then Subsingleton E.$$

Lean4

theorem subsingleton_of_no_eigenvalue_finiteDimensional (hT : T.IsSymmetric)
    (hT' : ∀ μ : 𝕜, Module.End.eigenspace (T : E →ₗ[𝕜] E) μ = ⊥) : Subsingleton E :=
  (subsingleton_or_nontrivial E).resolve_right fun _h => absurd (hT' _) hT.hasEigenvalue_iSup_of_finiteDimensional

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