English
If f is continuous on s in the topology of UniformOnFun and each f x is continuous on the spectrum and maps zero to zero, then x ↦ cfcₙ (f x) a is continuous on s.
Русский
Если f непрерывна на s в топологии UniformOnFun и для каждого x f x непрерывна на спектре и подает ноль в ноль, то x ↦ cfcₙ (f x) a непрерывна на s.
LaTeX
$$$\\text{ContinuousOn } (\\lambda x. \\operatorname{ofFun} \\{\\text{quasispectrum } R a\\} (f x))\n s \\rightarrow (\\forall x \\in s, ContinuousOn (f x) (\\text{quasispectrum } R a)) \\rightarrow (\\forall x \\in s, f x 0 = 0) \\rightarrow \\text{ContinuousOn } (\\lambda x. cfcₙ (f x) a) s$$$
Lean4
/-- If `f : X → R → R` is continuous on `s : Set X` in the topology on
`X → R →ᵤ[{spectrum R a}] → R`, and for each `x ∈ s`, `f x` is continuous on the spectrum and
maps zero to itself, then `x ↦ cfcₙ (f x) a` is continuous on `s` also. -/
theorem cfcₙ_fun [TopologicalSpace X] {f : X → R → R} {a : A} {s : Set X}
(h_cont : ContinuousOn (fun x ↦ ofFun {quasispectrum R a} (f x)) s)
(hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)) (hf0 : ∀ x ∈ s, f x 0 = 0) :
ContinuousOn (fun x ↦ cfcₙ (f x) a) s := by
rw [ContinuousOn] at h_cont ⊢
simp only [ContinuousWithinAt, UniformOnFun.tendsto_iff_tendstoUniformlyOn, Set.mem_singleton_iff, Function.comp_def,
toFun_ofFun, forall_eq] at h_cont
refine fun x hx ↦ continuousWithinAt_cfcₙ_fun (h_cont x hx) ?_ ?_
all_goals filter_upwards [self_mem_nhdsWithin] with x hx
exacts [hf x hx, hf0 x hx]
