English
If the restricted predicate holds for f at x, and g agrees with f near A, then the restricted predicate holds for g at x.
Русский
Если ограниченный предикат держится для f в точке x, и g совпадает с f близко к A, то предикат держится и для g в точке x.
LaTeX
$$$(hf : RestrictGermPredicate P A x f) \land (h : \forall^\infty z \in 𝓝^s A, g z = f z) \Rightarrow RestrictGermPredicate P A x g$$$
Lean4
theorem restrictGermPredicate_congr {P : ∀ x : X, Germ (𝓝 x) Y → Prop} (hf : RestrictGermPredicate P A x f)
(h : ∀ᶠ z in 𝓝ˢ A, g z = f z) : RestrictGermPredicate P A x g :=
by
intro hx
apply ((hf hx).and <| (eventually_nhdsSet_iff_forall.mp h x hx).eventually_nhds).mono
rintro y ⟨hy, h'y⟩
rwa [Germ.coe_eq.mpr h'y]
