English
From differentiability at x, the equality of f on t implies equality of differentiability on t provided t ⊆ s.
Русский
Из дифференцируемости в точке x следует равенство дифференцируемости на t при условии t ⊆ s.
LaTeX
$$$MDifferentiableWithinAt\ I I'\ f\ s\ x\ f' \land (t\subseteq s) \Rightarrow (\forall y\in t, f_1(y)=f(y)) \Rightarrow MDifferentiableWithinAt\ I I'\ f_1\ t\ x$$$
Lean4
/-- Version of `MDifferentiableWithinAt.congr` where `x` need not be contained in `s`,
but `f` and `f₁` are equal on a set containing both. -/
theorem congr' (h : MDifferentiableWithinAt I I' f s x) (ht : ∀ x ∈ t, f₁ x = f x) (hst : s ⊆ t) (hxt : x ∈ t) :
MDifferentiableWithinAt I I' f₁ s x :=
h.congr (fun _y hy ↦ ht _y (hst hy)) (ht x hxt)
