English
If f is C^n on s × u and α is C^n on s with α(t) ∈ u for all t ∈ s, then t ↦ f(t, α(t)) is C^n on s.
Русский
Если f на области s × u обладает гладкостью C^n, а α на s имеет гладкость C^n и α(t) ∈ u для всех t ∈ s, то t ↦ f(t, α(t)) имеет гладкость C^n на s.
LaTeX
$$Если $f$ является $C^n$ на $s\\times u$, $\\alpha$ является $C^n$ на $s$ и $\\alpha(t)\\in u$ для всех $t\\in s$, то $t\\mapsto f(t,\\alpha(t))$ является $C^n$ на $s$.$$
Lean4
/-- Given a $C^n$ time-dependent vector field `f` and a $C^n$ curve `α`, the composition `f t (α t)`
is $C^n$ in `t`. -/
theorem contDiffOn_comp {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n (uncurry f) (s ×ˢ u)) (hα : ContDiffOn ℝ n α s)
(hmem : ∀ t ∈ s, α t ∈ u) : ContDiffOn ℝ n (fun t ↦ f t (α t)) s :=
by
have : (fun t ↦ f t (α t)) = (uncurry f) ∘ fun t ↦ (t, α t) := rfl
rw [this]
apply hf.comp (by fun_prop)
intro _ ht
rw [mem_prod]
exact ⟨ht, hmem _ ht⟩
