eventuallyEq_nhds — Mathlib

English

If f and g are equal in a neighborhood of x, then for y sufficiently close to x these functions are equal in a neighborhood of y.

Русский

Если f и g равны в окрестности x, то при достаточно близких к x y функции равны в окрестности y.

LaTeX

$$$(\\nhds x).EventuallyEq f g \\Rightarrow \\forall^* y \\in 𝓝 x,\\ (\\nhds y).EventuallyEq f g.$$$

Lean4

/-- If two functions are equal in a neighbourhood of `x`, then for `y` sufficiently close
to `x` these functions are equal in a neighbourhood of `y`. -/
theorem eventuallyEq_nhds {f g : X → α} (h : f =ᶠ[𝓝 x] g) : ∀ᶠ y in 𝓝 x, f =ᶠ[𝓝 y] g :=
  h.eventually_nhds

Похожие утверждения