English
Let a be a family of elements a_i in each κ_i indexed by i ∈ ι. Then the R-quasispectrum of the family a equals the union, over all indices i, of the R-quasispectra of the individual components a_i.
Русский
Пусть a = (a_i) — семейство элементов a_i из κ_i по индексу i ∈ ι. Тогда R-квазиспектрум последовательности a совпадает с объединением по all i квазиспектров отдельных компонентов a_i.
LaTeX
$$$$ \operatorname{quasispectrum}(R,a) = \bigcup_i \operatorname{quasispectrum}(R, a_i) $$$$
Lean4
theorem quasispectrum_eq [Nonempty ι] [CommSemiring R] [∀ i, NonUnitalRing (κ i)] [∀ i, Module R (κ i)] (a : ∀ i, κ i) :
quasispectrum R a = ⋃ i, quasispectrum R (a i) := by
ext r
simp only [quasispectrum, Set.mem_setOf_eq, Set.mem_iUnion]
by_cases hr : IsUnit r
· lift r to Rˣ using hr with r' hr'
simp [isQuasiregular_pi_iff]
· simp [hr]
