differentiableAt_iff_comp_neg — Mathlib

English

Differentiability of f at a is equivalent to differentiability of the negated argument: f ∈ DifferentiableAt a iff f ∘ (−id) is differentiable at −a.

Русский

Дифференцируемость f в a эквивалентна дифференцируемости f при замещении аргумента на −a.

LaTeX

$$$ \\text{DifferentiableAt}(f)(a) \\iff \\text{DifferentiableAt}(f \\circ (-\\mathrm{id}))( -a) $$$

Lean4

theorem differentiableAt_iff_comp_neg {a : 𝕜} : DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (-x)) (-a) := by
  simp_rw [← differentiableAt_comp_neg, neg_neg]

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