congr — Mathlib

English

If f and f1 agree on a set, then differentiability on that set is equivalent.

Русский

Если f и f1 совпадают на множестве, то дифференцируемость на этом множестве эквивалентна.

LaTeX

$$$ \\mathrm{DifferentiableOn}(f,s) \\to (\\forall x\\in s,\; f_1(x)=f(x)) \\to \\mathrm{DifferentiableOn}(f_1,s) $$$

Lean4

theorem congr (h : DifferentiableOn 𝕜 f s) (h' : ∀ x ∈ s, f₁ x = f x) : DifferentiableOn 𝕜 f₁ s := fun x hx =>
  (h x hx).congr h' (h' x hx)

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