Theorems · Theorem · functional analysis

Subalgebra.frontier_spectrum

∀ {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [inst : NormedRing A] [CompleteSpace A] [inst_2 : SetLike SA A]
  [inst_3 : SubringClass SA A] [inst_4 : NormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A]
  (S : SA) [hS : IsClosed ↑S] (x : ↥S), frontier (spectrum 𝕜 x) ⊆ spectrum 𝕜 ↑x

If S : Subalgebra 𝕜 A is a closed subalgebra of a Banach algebra A, then for any x : S, the boundary of the spectrum of x relative to S is a subset of the spectrum of ↑x : A relative to A.

Defined in

Mathlib.Analysis.Normed.Algebra.Spectrum

Cited by

2 results in Mathlib

Foundations

Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedRingCompleteSpaceSetLikeSubringClassNormedFieldNormedAlgebraSMulMemClassIsClosed