eventually_eventually_nhds — Mathlib

English

For any X with a topology and any f,g: X→α, if they are eventually equal in nhds x, then for y near x, f and g are eventually equal in nhds y.

Русский

Пусть X — топологическое пространство и f,g: X→α. Если они равны в окрестности x в смысле предела, то при ближайших y к x они равны в окрестностях y.

LaTeX

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

Lean4

@[simp]
theorem eventually_eventually_nhds {p : X → Prop} : (∀ᶠ y in 𝓝 x, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝 x, p x :=
  ⟨fun h => h.self_of_nhds, fun h => h.eventually_nhds⟩

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