isOpen_resolventSet

Mathlib.Analysis.Normed.Algebra.Spectrum

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

English

The resolvent set ρ(a) is an open subset of the underlying algebra.

Русский

Множество резольвентности ρ(a) открыто в алгебраическом пространстве.

LaTeX

$$$IsOpen(\rho(a)).$$$

Lean4

theorem isOpen_resolventSet (a : A) : IsOpen (ρ a) :=
  Units.isOpen.preimage ((continuous_algebraMap 𝕜 A).sub continuous_const)

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

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

Разделы

Аффилиация

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