English
If h is ContMDiffWithinAt I I' n f s x and f1 agrees with f on s, and x ∈ s, then f1 is ContMDiffWithinAt I I' n f1 s x. The smoothness on s at x is preserved when replacing f by a function that matches f on s, provided x lies in s.
Русский
Если h: ContMDiffWithinAt I I' n f s x и f1 совпадает с f на s, и x ∈ s, тогда f1: ContMDiffWithinAt I I' n f1 s x. Гладкость на s в точке x сохраняется при замене f на функцию, которая совпадает с f на s, если x ∈ s.
LaTeX
$$$h : ContMDiffWithinAt I I' n f s x \;\text{ и }\; \forall y \in s, f_1 y = f y \;\land\; x \in s \Rightarrow ContMDiffWithinAt I I' n f_1 s x.$$$
Lean4
theorem congr_of_mem (h : ContMDiffWithinAt I I' n f s x) (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : x ∈ s) :
ContMDiffWithinAt I I' n f₁ s x :=
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_of_mem h h₁ hx
