English
If f is continuous in a parameter x in γ and g is continuous at x, then the map a ↦ IccExtend h (f a) (g a) is continuous at x.
Русский
Если f непрерывна по параметру в γ и g непрерывна в x, то a ↦ IccExtend h (f a) (g a) непрерывно в x.
LaTeX
$$$\\forall x,\\ (\\text{ContinuousAt } (f) x)\\land (\\text{ContinuousAt } g x)\\Rightarrow \\text{ContinuousAt } (a\\mapsto IccExtend h (f a) (g a)) x.$$$
Lean4
@[fun_prop]
theorem IccExtend {x : γ} (f : γ → Icc a b → β) {g : γ → α} (hf : ContinuousAt ↿f (x, projIcc a b h (g x)))
(hg : ContinuousAt g x) : ContinuousAt (fun a => IccExtend h (f a) (g a)) x :=
show ContinuousAt (↿f ∘ fun x => (x, projIcc a b h (g x))) x from
ContinuousAt.comp hf <| continuousAt_id.prodMk <| continuous_projIcc.continuousAt.comp hg
