congr_mono — Mathlib

English

If h has MF-derivative within s at x, and f1 equals f on t with hxt as a unique differentiability set, and t ⊆ s, then mfderivWithin equality holds.

Русский

Если h имеет MF-дериватив внутри s в x, и f1 совпадает с f на t, с условием уникальности точки, и t ⊆ s, тогда mfderivWithin совпадает.

LaTeX

$$$MDifferentiableWithinAt\ I I'\ f\ s\ x\ f' \Rightarrow (\forall x\in t, f_1 x = f x) \Rightarrow t\subseteq s \Rightarrow mfderivWithin\ I I'\ f\ t\ x = mfderivWithin\ I I'\ f\ s\ x$$$

Lean4

theorem congr_mono (h : MDifferentiableWithinAt I I' f s x) (ht : ∀ x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t ⊆ s) :
    MDifferentiableWithinAt I I' f₁ t x :=
  (HasMFDerivWithinAt.congr_mono h.hasMFDerivWithinAt ht hx h₁).mdifferentiableWithinAt

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