comp — Mathlib

English

If g is differentiable on a set u and f is differentiable on a set s, and s ⊆ f^{-1}(u), then g ∘ f is differentiable on s.

Русский

Если g дифференцируема на множество u, а f — на множество s, и s ⊆ f^{-1}(u), то g ∘ f дифференцируема на s.

LaTeX

$$(hg : MDifferentiableOn I' I'' g u) ∧ (hf : MDifferentiableOn I I' f s) ∧ (st : s ⊆ f^{-1} u) ⇒ MDifferentiableOn I I'' (g ∘ f) s$$

Lean4

theorem comp (hg : MDifferentiableOn I' I'' g u) (hf : MDifferentiableOn I I' f s) (st : s ⊆ f ⁻¹' u) :
    MDifferentiableOn I I'' (g ∘ f) s := fun x hx => MDifferentiableWithinAt.comp x (hg (f x) (st hx)) (hf x hx) st

Похожие утверждения