English
If f is uniformly convergent to f x0 on spectra and each f x is continuous on spectrum, then the map x ↦ cfc(f x) a is continuous within the set s at x0.
Русский
Если f сходится равномерно к f x0 на спектре и каждый f x непрерывен на спектре, то x ↦ cfc(f x) a непрерывна внутри s в точке x0.
LaTeX
$$$\\text{TendstoUniformlyOn } f (f x_0) (nhdsWithin x_0 s) (\\text{spectrum } R a) \\rightarrow \\\\text{Eventual}(x, ContinuousOn(f x, \\text{spectrum } R a)) \\Rightarrow \\\\text{ContinuousWithinAt}(x \\mapsto cfc(f x) a) s x_0$$$
Lean4
/-- If `f : X → R → R` tends to `f x₀` uniformly (along `𝓝[s] x₀`) on the spectrum of `a`,
and eventually each `f x` is continuous on the spectrum of `a`, then `fun x ↦ cfc (f x) a` is
continuous at `x₀` within `s`. -/
theorem continuousWithinAt_cfc_fun [TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X} {s : Set X}
(h_tendsto : TendstoUniformlyOn f (f x₀) (𝓝[s] x₀) (spectrum R a))
(hf : ∀ᶠ x in 𝓝[s] x₀, ContinuousOn (f x) (spectrum R a)) : ContinuousWithinAt (fun x ↦ cfc (f x) a) s x₀ :=
tendsto_cfc_fun h_tendsto hf
