English
If f is continuous on its joint domain and α is continuous on s with α(s) ⊆ u, then t ↦ f(t, α(t)) is continuous on s.
Русский
Если функция $f$ непрерывна на объединённой области и $\\alpha$ непрерывна на $s$ с $\\alpha(s)\\subseteq u$, то $t\\mapsto f(t,\\alpha(t))$ непрерывна на $s$.
LaTeX
$$Если $f$ непрерывно на $\\operatorname{uncurry} f$ на $s\\times u$ и $α$ непрерывна на $s$ и $MapsTo(α,s,u)$, то $t\\mapsto f(t,α(t))$ непрерывна на $s$.$$
Lean4
/-- Given a continuous time-dependent vector field `f` and a continuous curve `α`, the composition
`f t (α t)` is continuous in `t`. -/
theorem continuousOn_comp (hf : ContinuousOn (uncurry f) (s ×ˢ u)) (hα : ContinuousOn α s) (hmem : MapsTo α s u) :
ContinuousOn (fun t ↦ f t (α t)) s :=
contDiffOn_zero.mp <| (contDiffOn_comp (contDiffOn_zero.mpr hf) (contDiffOn_zero.mpr hα) hmem)
