differentiableAt_comp_neg — Mathlib

English

For any a ∈ 𝕜, differentiability of f ∘ (−id) at a is equivalent to differentiability of f at −a.

Русский

Для любого a ∈ 𝕜 дифференцируемость f ∘ (−id) в a эквивалентна дифференцируемости f в −a.

LaTeX

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

Lean4

theorem differentiableAt_comp_neg {a : 𝕜} : DifferentiableAt 𝕜 (fun x ↦ f (-x)) a ↔ DifferentiableAt 𝕜 f (-a) :=
  by
  refine ⟨fun H ↦ ?_, fun H ↦ H.comp a differentiable_neg.differentiableAt⟩
  convert ((neg_neg a).symm ▸ H).comp (-a) differentiable_neg.differentiableAt
  ext
  simp only [Function.comp_apply, neg_neg]

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