comp_of_eq — Mathlib

English

If hh₂ is HasDerivAtFilter at h x with derivative h₂′ and hh is HasDerivAtFilter at x with derivative h′, then the iterated function h₂ ∘ h under the filter L has derivative h₂′ * h′.

Русский

Если hh₂ имеет HasDerivAtFilter в h x и имеет производную h₂′, а hh — HasDerivAtFilter в x с производной h′, то производная итерации по фильтру L есть.

LaTeX

$$$$\\forall x:\\ HasDerivAtFilter h₂ h₂' (h x) \\land\\ HasDerivAtFilter h h' x \\Rightarrow HasDerivAtFilter (h_2\\circ h) (h_2' * h') x. $$$$

Lean4

theorem comp_of_eq (hh₂ : HasStrictDerivAt h₂ h₂' y) (hh : HasStrictDerivAt h h' x) (hy : y = h x) :
    HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x := by rw [hy] at hh₂; exact hh₂.comp x hh

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