congr_mono — Mathlib

English

For differentiability within sets, equality on a set implies transfer of differentiability under subset relations.

Русский

Для дифференцируемости внутри множеств равенство на множестве означает переносимость дифференцируемости при подмножествах.

LaTeX

$$$ \\mathrm{DifferentiableWithinAt}(f,s,x) \\to \\mathrm{Set.EqOn}(f_1,f,t) \\to \\mathrm{Subset}(t,s) \\to \\mathrm{DifferentiableWithinAt}(f_1,t,x) $$$

Lean4

theorem congr_mono (h : DifferentiableWithinAt 𝕜 f s x) (ht : EqOn f₁ f t) (hx : f₁ x = f x) (h₁ : t ⊆ s) :
    DifferentiableWithinAt 𝕜 f₁ t x :=
  (HasFDerivWithinAt.congr_mono h.hasFDerivWithinAt ht hx h₁).differentiableWithinAt

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