derivWithin_congr — Mathlib

English

If f and f1 agree on s and x ∈ s, then their derivatives within s at x agree.

Русский

Если две функции одинаковы на s и x ∈ s, их производные внутри s в x совпадают.

LaTeX

$$$\\mathrm{EqOn}\; f_1 f s \\rightarrow Eq (f_1 x) (f x) \\rightarrow Eq (derivWithin f_1 s x) (derivWithin f s x)$$$

Lean4

theorem derivWithin_congr (hs : EqOn f₁ f s) (hx : f₁ x = f x) : derivWithin f₁ s x = derivWithin f s x :=
  by
  unfold derivWithin
  rw [fderivWithin_congr hs hx]

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