differentiableOn_congr — Mathlib

English

If f0 and f1 are differentiable at x and equal in a neighborhood of x, then the differentiability at x with the same derivative passes between them.

Русский

Если f0 и f1 дифференцируемы в x и совпадают в окрестности x, то дифференцируемость в x с тем же производным переходит между ними.

LaTeX

$$$ (\\forall f_0,f_1) \\bigl(\\mathrm{DifferentiableAt}(f_0,f',x) \\iff \\mathrm{DifferentiableAt}(f_1,f',x)\\bigr) $$$

Lean4

theorem differentiableOn_congr (h' : ∀ x ∈ s, f₁ x = f x) : DifferentiableOn 𝕜 f₁ s ↔ DifferentiableOn 𝕜 f s :=
  ⟨fun h => DifferentiableOn.congr h fun y hy => (h' y hy).symm, fun h => DifferentiableOn.congr h h'⟩

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