Theorems · Theorem · functional analysis

Subalgebra.spectrum_eq_of_isPreconnected_compl

∀ {𝕜 : 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 : NontriviallyNormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A]
  [inst_6 : SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] (x : ↥S),
  IsPreconnected (spectrum 𝕜 ↑x)ᶜ → spectrum 𝕜 x = spectrum 𝕜 ↑x

Let S be a closed subalgebra of a Banach algebra A. If for x : S the complement of the spectrum of ↑x : A is connected, then spectrum 𝕜 x = spectrum 𝕜 (x : A).

Defined in

Mathlib.Analysis.Normed.Algebra.Spectrum

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedRingCompleteSpaceSetLikeSubringClassNontriviallyNormedFieldNormedAlgebraSMulMemClassIsClosed