isClosed — Mathlib

English

Let 𝕜 be a normed field and A a normed algebra over 𝕜 with A complete. For every a ∈ A, the spectrum σ𝕜(a) is a closed subset of 𝕜.

Русский

Пусть 𝕜 — нормированное поле, A — нормированная алгебра над 𝕜, пространство A полно. Для любого a ∈ A спектр σ𝕜(a) является замкнутым подмножеством 𝕜.

LaTeX

$$$\\mathrm{IsClosed}\\bigl(\\sigma_{\\mathbb{K}}(a)\\bigr)$$$

Lean4

@[simp]
protected theorem isClosed (a : A) : IsClosed (σ a) :=
  (isOpen_resolventSet a).isClosed_compl

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