spec_cfcₙAux — Mathlib

English

The spectrum of cfcₙAux hp₁ a ha applied to f equals the range of f.

Русский

Спектр отображения cfcₙAux hp₁ a ha, применённого к f, равен образу f.

LaTeX

$$$$ \\operatorname{spec}(cfc\\_nAux hp\\_1 a ha f) = \\operatorname{range} f $$$$

Lean4

theorem spec_cfcₙAux (f : C(σₙ 𝕜 a, 𝕜)₀) : σ 𝕜 (cfcₙAux hp₁ a ha f) = Set.range f :=
  by
  rw [cfcₙAux, NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply]
  simp only [NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_coe]
  rw [cfcHom_map_spectrum (hp₁.mpr ha) (R := 𝕜) _]
  simp

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