English
If F tends uniformly to f on the quasispectrum and each F x is continuous and maps zero to zero, then x ↦ cfcₙ (F x) a is continuous at x0.
Русский
Если F равномерно сходится к f на квази-спектре и каждый F x непрерывна и отображает ноль в ноль, то x ↦ cfcₙ (F x) a непрерывна в x0.
LaTeX
$$$\\text{TendstoUniformlyOn } F f (nhds x_0) (\\text{quasispectrum } R a) \\land (\\forall x, ContinuousOn (F x) (\\text{quasispectrum } R a)) \\land (\\forall x, F x 0 = 0) \\Rightarrow \\ Cont\\n\\ tinuousAt (\\lambda x. cfcₙ (F x) 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` and maps zero to itself, 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₀) (quasispectrum R a))
(hf : ∀ᶠ x in 𝓝 x₀, ContinuousOn (f x) (quasispectrum R a)) (hf0 : ∀ᶠ x in 𝓝 x₀, f x 0 = 0) :
ContinuousAt (fun x ↦ cfcₙ (f x) a) x₀ :=
tendsto_cfcₙ_fun h_tendsto hf hf0
