fderivWithin_congr_mono — Mathlib

English

If nhdsWithin x s sees f1 equal to f, then fderivWithin f1 s x = fderivWithin f s x when x ∈ s.

Русский

Если nhdsWithin x s фиксирует равенство f1 и f, то fderivWithin f1 s x = fderivWithin f s x при x ∈ s.

LaTeX

$$$ (nhdsWithin x s).\\text{EventuallyEq}(f_1,f) \\to x\\in s \\to \\mathrm{fderivWithin}(f_1,s,x) = \\mathrm{fderivWithin}(f,s,x) $$$

Lean4

theorem fderivWithin_congr_mono (h : DifferentiableWithinAt 𝕜 f s x) (hs : EqOn f₁ f t) (hx : f₁ x = f x)
    (hxt : UniqueDiffWithinAt 𝕜 t x) (h₁ : t ⊆ s) : fderivWithin 𝕜 f₁ t x = fderivWithin 𝕜 f s x :=
  (HasFDerivWithinAt.congr_mono h.hasFDerivWithinAt hs hx h₁).fderivWithin hxt

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