differentiableWithinAt_comp_sub — Mathlib

English

If f is differentiable within s at x after subtracting a, then f is differentiable within translated set at x − a.

Русский

Если после вычитания a функция f дифференцируема внутри s в точке x, то она дифференцируема внутри перенесённого множества в точке x − a.

LaTeX

$$$\text{DifferentiableWithinAt}(f(\cdot - a), s, x) \iff \text{DifferentiableWithinAt}(f, -a + s, x - a)$$$

Lean4

theorem differentiableWithinAt_comp_sub (a : E) :
    DifferentiableWithinAt 𝕜 (fun x ↦ f (x - a)) s x ↔ DifferentiableWithinAt 𝕜 f (-a +ᵥ s) (x - a) := by
  simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_sub]

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