continuousOn_zpow₀_spectrum — Mathlib

English

A variant of the previous continuity lemma expressed via a simple subset-equivalence for spectrum and inv.

Русский

Вариант выражения непрерывности через простое равенство подмножеств спектра и обращение.

LaTeX

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

Lean4

@[fun_prop]
theorem continuousOn_zpow₀_spectrum [ContinuousMul R] (a : Aˣ) (n : ℤ) : ContinuousOn (· ^ n) (spectrum R (a : A)) :=
  (continuousOn_zpow₀ n).mono <| by simpa only [Set.subset_compl_singleton_iff] using spectrum.zero_notMem R a.isUnit

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