continuousOn_inv₀_spectrum — Mathlib

English

For any unit a in A, the map x ↦ x⁻¹ is continuous on the spectrum of a.

Русский

Пусть a — модуль единицы в A; отображение x ↦ x⁻¹ непрерывно на спектре a.

LaTeX

$$ContinuousOn (\x => x^{-1}) (spectrum R (a : A))$$

Lean4

@[fun_prop]
theorem continuousOn_inv₀_spectrum (a : Aˣ) : ContinuousOn (·⁻¹) (spectrum R (a : A)) :=
  continuousOn_inv₀.mono <| by simpa only [Set.subset_compl_singleton_iff] using spectrum.zero_notMem R a.isUnit

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