mfderivWithin_congr — Mathlib

English

If f and f1 agree pointwise on all of s, then their MF derivatives within s at x coincide.

Русский

Если функции f и f1 совпадают на всем множесте s по точкам, то их MF-дифференциалы внутри s в точке x совпадают.

LaTeX

$$$\\forall x\\in M,\\; (f = f_1\\text{ on }s) \\Rightarrow mfderivWithin I I' f\\,s\\,x = mfderivWithin I I' f_1\\,s\\,x$$$

Lean4

theorem mfderivWithin_congr (hL : ∀ x ∈ s, f₁ x = f x) (hx : f₁ x = f x) :
    mfderivWithin I I' f₁ s x = mfderivWithin I I' f s x :=
  Filter.EventuallyEq.mfderivWithin_eq (Filter.eventuallyEq_of_mem self_mem_nhdsWithin hL) hx

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