fderivWithin_congr' — Mathlib

English

If EqOn f1 f s and x ∈ s, then fderivWithin 𝕜 f1 s x = fderivWithin 𝕜 f s x.

Русский

Если EqOn f1 f s и x принадлежит s, тогда fderivWithin 𝕜 f1 s x = fderivWithin 𝕜 f s x.

LaTeX

$$$\text{If } (f_1=f)\text{ on } s\text{ and } x\in s,\; fderivWithin 𝕜 f_1 s x = fderivWithin 𝕜 f s x.$$$

Lean4

theorem fderivWithin_congr' (hs : EqOn f₁ f s) (hx : x ∈ s) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
  fderivWithin_congr hs (hs hx)

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