congr_mono — Mathlib

English

If a derivative exists for f at x inside s, and f1 agrees with f on t ⊆ s with f1 x = f x and f1 ≡ f on t, then HasFDerivWithinAt f1 f' t x holds.

Русский

Если существует производная внутри области для f, и f1 совпадает с f на t ⊆ s при f1 x = f x и f1 ≡ f на t, тогда имеет место HasFDerivWithinAt f1 f' t x.

LaTeX

$$$ \\mathrm{HasFDerivWithinAt}(f,f',s,x) \\to \\mathrm{Set.EqOn}(f_1,f,t) \\Rightarrow \\mathrm{Eq}(f_1(x),f(x)) \\to \\mathrm{HasFDerivWithinAt}(f_1,f',t,x) $$$

Lean4

theorem congr_mono (h : HasFDerivWithinAt f f' s x) (ht : EqOn f₁ f t) (hx : f₁ x = f x) (h₁ : t ⊆ s) :
    HasFDerivWithinAt f₁ f' t x :=
  HasFDerivAtFilter.congr_of_eventuallyEq (h.mono h₁) (Filter.mem_inf_of_right ht) hx

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