isOpen_setOf_eventually_nhds — Mathlib

English

For any predicate p on X, the set of points x for which p holds eventually in the neighborhood of x is open.

Русский

Для любого предиката p на X множество точек x, для которых p выполняется вплоть до окрестности x, является открытым.

LaTeX

$$$\\operatorname{IsOpen}\\left(\\{x \\mid \\mathrm{Eventually}(p, \\mathcal{N}(x))\\}\\right)$$$

Lean4

theorem isOpen_setOf_eventually_nhds {p : X → Prop} : IsOpen {x | ∀ᶠ y in 𝓝 x, p y} := by
  simp only [← interior_setOf_eq, isOpen_interior]

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