spectrum_real_eq_range_eigenvalues

English

The real-spectrum of a Hermitian matrix equals the range of its eigenvalues.

Русский

ℝ-спектр эрмитовой матрицы равен диапазону её собственных значений.

LaTeX

$$$\\\\operatorname{Spectrum}_{\\\\mathbb{R}}(A) = \\\\mathrm{range}(h_A\\\\,\\\\mathrm{eigenvalues})$$$

Lean4

/-- The `ℝ`-spectrum of a Hermitian matrix over `RCLike` field is the range of the eigenvalue
function. -/
theorem spectrum_real_eq_range_eigenvalues : spectrum ℝ A = Set.range hA.eigenvalues :=
  Set.ext fun x => by
    conv_lhs => rw [hA.spectral_theorem, ← spectrum.algebraMap_mem_iff 𝕜]
    simp

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