of_subsingleton

Mathlib.Algebra.Algebra.Spectrum.Basic

URI: https://scilib.ai/kg/mathlib#spectrum.of_subsingleton

English

If A is a subsingleton, then the spectrum of any a ∈ A is empty: spectrum R a = ∅.

Русский

Если A является одноэлементным множеством, спектр любого элемента a ∈ A пуст: спектр R a = ∅.

LaTeX

$$$\operatorname{spectrum}(R,a) = \emptyset$$$

Lean4

@[simp]
theorem of_subsingleton [Subsingleton A] (a : A) : spectrum R a = ∅ := by
  rw [spectrum, resolventSet_of_subsingleton, Set.compl_univ]

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

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

Разделы

Аффилиация

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