spectrum_apply_subset

Mathlib.Algebra.Algebra.Spectrum.Basic

URI: https://scilib.ai/kg/mathlib#AlgHom.spectrum_apply_subset

English

If φ a ∈ σ(a), then the image under φ lies in the spectrum consistently with functoriality.

Русский

Образ под φ принадлежит спектру и согласуется с функториальностью.

LaTeX

$$$\sigma_R((\phi : A \to B) a) \subseteq \sigma_R(a)$$$

Lean4

theorem spectrum_apply_subset (φ : F) (a : A) : σ ((φ : A → B) a) ⊆ σ a := fun _ => mt (mem_resolventSet_apply φ)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru