English
If f is a family of functions defined on Icc(a,b), and each f_k varies continuously with a parameter, then the extended map is continuous.
Русский
Если f задаёт семейство функций на Icc(a,b) и каждая f_k непрерывна относительно параметра, то расширение непрерывно.
LaTeX
$$$\\forall \\text{family } f:\\gamma \\to (Icc\\ a\\ b)\\to \\beta,\\ \\text{Continuous } f\\Rightarrow \\text{Continuous } (\\IccExtend h f).$$$
Lean4
/-- See Note [continuity lemma statement]. -/
@[fun_prop]
protected theorem IccExtend {f : γ → Icc a b → β} {g : γ → α} (hf : Continuous ↿f) (hg : Continuous g) :
Continuous fun a => IccExtend h (f a) (g a) :=
show Continuous (↿f ∘ fun x => (x, projIcc a b h (g x))) from
hf.comp <| continuous_id.prodMk <| continuous_projIcc.comp hg
