English
If a predicate p holds eventually in a neighborhood of x, then for y sufficiently close to x, p holds in a neighborhood of y.
Русский
Если предикат p выполняется в окрестности x неразрывно (скоромно) тогда, для близких к x y, p выполняется в окрестности y.
LaTeX
$$$(\\forall^* y \\in 𝓝 x,\\ p(y)) \\Rightarrow (\\forall^* y \\in 𝓝 x,\\ \\forall^* x \\in 𝓝 y,\\ p(x)).$$$
Lean4
/-- If a predicate is true in a neighbourhood of `x`, then for `y` sufficiently close
to `x` this predicate is true in a neighbourhood of `y`. -/
theorem eventually_nhds {p : X → Prop} (h : ∀ᶠ y in 𝓝 x, p y) : ∀ᶠ y in 𝓝 x, ∀ᶠ x in 𝓝 y, p x :=
let ⟨t, htp, hto, ha⟩ := eventually_nhds_iff.1 h
eventually_nhds_iff.2 ⟨t, fun _x hx => eventually_nhds_iff.2 ⟨t, htp, hto, hx⟩, hto, ha⟩
