eventually_eventuallyEq_nhds — Mathlib

English

If nhds x and f,g: X→α are eventually equal, then for all y near x, nhds y also makes f and g eventually equal.

Русский

Если nhds x и функции f,g: X→α равны хронологически (в окрестности x), то для всех y близких к x nhds y также делает f и g равными в окрестности y.

LaTeX

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

Lean4

@[simp]
theorem eventually_eventuallyEq_nhds {f g : X → α} : (∀ᶠ y in 𝓝 x, f =ᶠ[𝓝 y] g) ↔ f =ᶠ[𝓝 x] g :=
  eventually_eventually_nhds

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