English
If m ≤ n and a C^m property holds, then there exists an open neighborhood U of x such that the restricted map is C^m on insert x s ∩ U.
Русский
Если m ≤ n и выполняется свойство C^m, то существует открытое окрестность U точки x такая, что ограниченная функция C^m на insert x s ∩ U.
LaTeX
$$$ \exists U \text{ open}, x ∈ U \land ContMDiffOn I I' m f (insert x s \cap U) $$$
Lean4
/-- Being `C^n` in a set only depends on the germ of the set. Version where one only requires
the two sets to coincide locally in the complement of a point `y`. -/
theorem contMDiffWithinAt_congr_set' (y : M) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x :=
by
have : T1Space M := I.t1Space M
rw [← contMDiffWithinAt_insert_self (s := s), ← contMDiffWithinAt_insert_self (s := t)]
exact contMDiffWithinAt_congr_set (eventuallyEq_insert h)
