English
Let f, f1: M → M' be two maps between manifolds, and let s ⊆ t be two sets of M with x ∈ t. If f and f1 agree on the set t (i.e., f1 y = f y for all y ∈ t) and f is ContMDiffWithinAt I I' n f on s at x, then f1 is ContMDiffWithinAt on s at x as well. In particular, replacing f by a function that agrees with f on a neighborhood containing s does not affect the smoothness property at x.
Русский
Пусть f, f1 : M → M' две отображения между многообразиями, пусть s ⊆ t и x ∈ t. Если f и f1 совпадают на всех точках множества t (то есть f1 y = f y для всех y ∈ t), и если f является ContMDiffWithinAt I I' n f на s в точке x, тогда и f1 является ContMDiffWithinAt на s в точке x. Другими словами, замена f на функцию, совпадающую с f на окрестности, не меняет гладкость в точке x.
LaTeX
$$$\;\;\; \forall \; h: ContMDiffWithinAt I I' n f s x, \; \forall y \in t, f_1(y) = f(y), \; s \subseteq t, \; x \in t \Rightarrow ContMDiffWithinAt I I' n f_1 s x.$$$
Lean4
/-- Version of `ContMDiffWithinAt.congr` where `x` need not be contained in `s`,
but `f` and `f₁` are equal on a set containing both. -/
theorem congr' (h : ContMDiffWithinAt I I' n f s x) (h₁ : ∀ y ∈ t, f₁ y = f y) (hst : s ⊆ t) (hxt : x ∈ t) :
ContMDiffWithinAt I I' n f₁ s x :=
h.congr (fun _y hy ↦ h₁ _ (hst hy)) (h₁ x hxt)
