val_re_map_spectrum — Mathlib

English

The spectrum of a self-adjoint element a is the image of the real part map: spectrum(a) = { Re(z) : z ∈ spectrum(a) }.

Русский

Спектр сам-сопряженного элемента равен образу вещественной части: спектр(a) = { Re(z) : z ∈ спектр(a) }.

LaTeX

$$$$\operatorname{spectrum}_{\mathbb{C}}(a) = (\text{real})\,\operatorname{map}\, (\operatorname{re})''(\operatorname{spectrum}_{\mathbb{C}}(a)).$$$$

Lean4

/-- The spectrum of a selfadjoint is real -/
theorem val_re_map_spectrum {a : A} (ha : IsSelfAdjoint a) : spectrum ℂ a = ((↑) ∘ re '' spectrum ℂ a : Set ℂ) :=
  le_antisymm (fun z hz => ⟨z, hz, (ha.mem_spectrum_eq_re hz).symm⟩) fun z =>
    by
    rintro ⟨z, hz, rfl⟩
    simpa only [(ha.mem_spectrum_eq_re hz).symm, Function.comp_apply] using hz

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