fun_comp — Mathlib

English

If g is differentiable and f is differentiable, then the composition g ∘ f is differentiable.

Русский

Если g и f дифференцируемы, то композиция g ∘ f дифференцируема.

LaTeX

$$$$ \text{Differentiable}_{\mathbb{K}} g \to \text{Differentiable}_{\mathbb{K}} f \to \text{Differentiable}_{\mathbb{K}} (\lambda x. g(f(x))). $$$$

Lean4

@[fun_prop]
theorem fun_comp {g : F → G} (hg : Differentiable 𝕜 g) (hf : Differentiable 𝕜 f) : Differentiable 𝕜 (fun x ↦ g (f x)) :=
  fun x => DifferentiableAt.comp x (hg (f x)) (hf x)

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