English
For a function a : ∀ i, κ_i, spectrum_R(a) equals the union of spectra of its coordinates: spectrum_R(a) = ⋃ i spectrum_R(a_i).
Русский
Для функции a : ∀ i κ_i спектр равен объединению спектров координат: spectrum_R(a) = ⋃ i spectrum_R(a_i).
LaTeX
$$$\operatorname{spectrum}_R(a) = \bigcup_{i} \operatorname{spectrum}_R(a(i))$$$
Lean4
theorem spectrum_eq [CommSemiring R] [∀ i, Ring (κ i)] [∀ i, Algebra R (κ i)] (a : ∀ i, κ i) :
spectrum R a = ⋃ i, spectrum R (a i) := by
apply compl_injective
simp_rw [spectrum, Set.compl_iUnion, compl_compl, resolventSet, Set.iInter_setOf, Pi.isUnit_iff, sub_apply,
algebraMap_apply]