English
For a continuous map f: X → R (R a normed division ring), the spectrum of f over 𝕜 is the preimage under the algebra map: spectrum 𝕜 f = algebraMap 𝕜 R)⁻¹(Set.range f).
Русский
Для непрерывного отображения f: X → R спектр f над 𝕜 равен предобразу диапазона под алгебраическим отображением.
LaTeX
$$$\mathrm{spectrum}_{\mathbb{K}}(f) = (\mathrm{algebraMap}_{\mathbb{K}, R})^{-1}(\mathrm{range}(f)).$$$
Lean4
theorem continuous_isUnit_unit {f : C(X, R)} (h : ∀ x, IsUnit (f x)) : Continuous fun x => (h x).unit :=
by
refine
continuous_induced_rng.2
(Continuous.prodMk f.continuous (MulOpposite.continuous_op.comp (continuous_iff_continuousAt.mpr fun x => ?_)))
have := NormedRing.inverse_continuousAt (h x).unit
simp only
simp only [← Ring.inverse_unit, IsUnit.unit_spec] at this ⊢
exact this.comp (f.continuousAt x)
