English
Under the hypotheses of tendsto_cfc_fun, the map x ↦ cfc(F x) a is continuous at x0.
Русский
При тех же предпосылках, что и tendsto_cfc_fun, отображение x ↦ cfc(F x) a непрерывно в точке x0.
LaTeX
$$$\\text{TendstoUniformlyOn } f (f x_0) (nhds x_0) (\\text{spectrum } R a) \\rightarrow \\\\text{Eventual}(x, ContinuousOn(Fx, \\text{spectrum } R a)) \\Rightarrow \\\\text{ContinuousAt}(x \\mapsto cfc(Fx) a) x_0$$$
Lean4
/-- If `f : X → R → R` tends to `f x₀` uniformly (along `𝓝 x₀`) on the spectrum of `a`,
and each `f x` is continuous on the spectrum of `a`, then `fun x ↦ cfc (f x) a` is
continuous at `x₀`. -/
theorem continuousAt_cfc_fun [TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X}
(h_tendsto : TendstoUniformlyOn f (f x₀) (𝓝 x₀) (spectrum R a))
(hf : ∀ᶠ x in 𝓝 x₀, ContinuousOn (f x) (spectrum R a)) : ContinuousAt (fun x ↦ cfc (f x) a) x₀ :=
tendsto_cfc_fun h_tendsto hf
