English
If two functions f and f1 agree on s and share the same value at the point x ∈ s, then ContMDiffWithinAt I I' n f1 s x is equivalent to ContMDiffWithinAt I I' n f s x. The smoothness property is unchanged when replacing f by f1 on s.
Русский
Если две функции f и f1 согласуются на множестве s и имеют одинаковое значение в точке x ∈ s, тогда ContMDiffWithinAt I I' n f1 s x эквивалентно ContMDiffWithinAt I I' n f s x. Гладкость не меняется при замене f на f1 на s.
LaTeX
$$$\forall h = ContMDiffWithinAt I I' n f s x,\; \forall h_1: \forall y \in s, f_1 y = f y \;\Rightarrow\; ContMDiffWithinAt I I' n f_1 s x \;\Leftrightarrow\; ContMDiffWithinAt I I' n f s x.$$$
Lean4
theorem contMDiffWithinAt_congr (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : f₁ x = f x) :
ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x :=
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff h₁ hx
