Theorems · Theorem · functional analysis

upperHemicontinuous_quasispectrum

∀ (𝕜 : Type u_1) (A : Type u_2) [inst : NontriviallyNormedField 𝕜] [ProperSpace 𝕜] [inst_2 : NonUnitalNormedRing A]
  [inst_3 : NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [CompleteSpace A],
  UpperHemicontinuous (quasispectrum 𝕜)

The map a ↦ quasispectrum 𝕜 a is upper hemicontinuous.

Defined in

Mathlib.Analysis.Normed.Algebra.Spectrum

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldProperSpaceNonUnitalNormedRingNormedSpaceSMulCommClassIsScalarTowerCompleteSpace