mem_spectrum_eq_re — Mathlib

English

The spectrum of a self-adjoint element a is real: z ∈ spectrum(a) implies z = Re(z).

Русский

Спектр сам-сопряженного элемента является вещественным: если z ∈ spectrum(a), то z ∈ ℝ.

LaTeX

$$$$\text{IsSelfAdjoint}(a) \Rightarrow \text{ spectrum}_{\mathbb{C}}(a) \subseteq \mathbb{R}.$$$$

Lean4

/-- Any element of the spectrum of a selfadjoint is real. -/
theorem mem_spectrum_eq_re (a : selfAdjoint A) {z : ℂ} (hz : z ∈ spectrum ℂ (a : A)) : z = z.re :=
  a.prop.mem_spectrum_eq_re hz

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