comp' — Mathlib

English

Variant for the derivative within a composition without using ∘ notation.

Русский

Вариант формулировки для внутри-производной композиции без использования обозначения ∘.

LaTeX

$$$fderivWithin 𝕜 (y \mapsto g(f(y))) s x = fderivWithin 𝕜 g t (f(x)) \circ f' + \cdot$$$

Lean4

@[fun_prop]
theorem comp' {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : DifferentiableWithinAt 𝕜 f s x) :
    DifferentiableWithinAt 𝕜 (g ∘ f) (s ∩ f ⁻¹' t) x :=
  hg.comp x (hf.mono inter_subset_left) inter_subset_right

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