English
If g is differentiable on t and f is differentiable on s and MapsTo f s t, then g ∘ f is differentiable on s.
Русский
Если g дифференцируема на t, а f дифференцируема на s, и отображение f отображает s в t, то композиция g ∘ f дифференцируема на s.
LaTeX
$$$$ (\\text{DifferentiableOn}_{\\mathbb{K}} g\, t) \\to (\\text{DifferentiableOn}_{\\mathbb{K}} f\, s) \\to (\\text{MapsTo } f s t) \\to \\text{DifferentiableOn}_{\\mathbb{K}} (g \\circ f) s. $$$$
Lean4
@[fun_prop]
theorem fun_comp {g : F → G} {t : Set F} (hg : DifferentiableOn 𝕜 g t) (hf : DifferentiableOn 𝕜 f s)
(st : MapsTo f s t) : DifferentiableOn 𝕜 (fun x ↦ g (f x)) s := fun x hx =>
DifferentiableWithinAt.comp x (hg (f x) (st hx)) (hf x hx) st
