spectrum_eq — Mathlib

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]

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