comp_mdifferentiableOn — Mathlib

English

If g is differentiable in the model sense and f is differentiable on a set s, then g ∘ f is differentiable on s.

Русский

Если g дифференцируема в модели, а f дифференцируема на множестве s, то g ∘ f дифференцируема на s.

LaTeX

$$(hg : MDifferentiable I' I'' g) ∧ (hf : MDifferentiableOn I I' f s) ⇒ MDifferentiableOn I I'' (g ∘ f) s$$

Lean4

theorem comp_mdifferentiableOn (hg : MDifferentiable I' I'' g) (hf : MDifferentiableOn I I' f s) :
    MDifferentiableOn I I'' (g ∘ f) s := by
  rw [← mdifferentiableOn_univ] at hg
  exact hg.comp hf (by simp)

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