English
If a predicate P holds for the germ of f and g agrees with f on a neighborhood of A, then P holds for g on that neighborhood as well.
Русский
Если предикат P выполняется для гёрма f и g совпадает с f в окрестности A, то P выполняется и для g в этой окрестности.
LaTeX
$$$(\forall x \in A, P x f) \land (\forall^\infty z \in 𝓝^s A, g z = f z) \Rightarrow (\forall^\infty x \in 𝓝^s A, P x g)$$$
Lean4
theorem germ_congr_set {P : ∀ x : X, Germ (𝓝 x) Y → Prop} (hf : ∀ᶠ x in 𝓝ˢ A, P x f) (h : ∀ᶠ z in 𝓝ˢ A, g z = f z) :
∀ᶠ x in 𝓝ˢ A, P x g := by
rw [eventually_nhdsSet_iff_forall] at *
intro x hx
apply ((hf x hx).and (h x hx).eventually_nhds).mono
intro y hy
convert hy.1 using 1
exact Germ.coe_eq.mpr hy.2
