Theorems · Theorem · functional analysis

Subalgebra.isUnit_of_isUnit_val_of_eventually

∀ {𝕜 : 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] {l : Filter ↥S} {a : ↥S},
  IsUnit ↑a → l ≤ nhds a → (∀ᶠ (x : ↥S) in l, IsUnit x) → l.NeBot → IsUnit a

Let S be a closed subalgebra of a Banach algebra A. If a : S is invertible in A, and for all x : S sufficiently close to a within some filter l, x is invertible in S, then a is invertible in S as well.

Defined in

Mathlib.Analysis.Normed.Algebra.Spectrum

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedRingCompleteSpaceSetLikeSubringClassNormedFieldNormedAlgebraSMulMemClassIsClosed