English
If s is compact, the map fa ↦ cfc(toFun{ s } fa.1) fa.2 is jointly continuous on the product of the continuous-on-set and the predicate set.
Русский
Если s компактно, отображение пары (f,a) ↦ cfc(toFun{ s } f) a непрерывно по всем компонентам на произведении соответствующих множеств.
LaTeX
$$$\\IsCompact(s) \\rightarrow \\ ContinuousOn (\\lambda fa: (cfc (toFun{ s } fa.1) fa.2))\\ (\\{f | ContinuousOn (toFun{ s } f) s\\} \\timesˢ {a | p a ∧ spectrum 𝕜 a ⊆ s})$$$
Lean4
/-- The function `f ↦ cfc f a` is Lipschitz with constant 1 with respect to
supremum metric (on `R →ᵤ[{s}] R`) on those functions which are continuous on a set `s` containing
the spectrum. -/
theorem lipschitzOnWith_cfc_fun_of_subset (a : A) {s : Set R} (hs : spectrum R a ⊆ s) :
LipschitzOnWith 1 (fun f ↦ cfc (toFun { s } f) a) {f | ContinuousOn (toFun { s } f) (s)} :=
by
have h₁ := lipschitzOnWith_cfc_fun R a
have h₂ := lipschitzWith_one_ofFun_toFun' (𝔖 := {spectrum R a}) (𝔗 := { s }) (β := R) (by simpa)
have h₃ := h₂.lipschitzOnWith (s := {f | ContinuousOn (toFun { s } f) (s)})
simpa using h₁.comp h₃ (fun f hf ↦ hf.mono hs)
