comp — Mathlib

English

If g is differentiable in the model sense and f is differentiable, then g ∘ f is differentiable.

Русский

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

LaTeX

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

Lean4

theorem comp (hg : MDifferentiable I' I'' g) (hf : MDifferentiable I I' f) : MDifferentiable I I'' (g ∘ f) := fun x =>
  MDifferentiableAt.comp x (hg (f x)) (hf x)

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