interior_setOf_eq — Mathlib

English

Let p be a predicate on X. The interior of the set {x | p(x)} equals the set of points x for which p holds eventually in the neighborhood of x.

Русский

Пусть p — предикат на X. Внутренность множества {x | p(x)} равна множеству точек x, для которых p выполняется вплоть до некоторой окрестности x.

LaTeX

$$$\\operatorname{int}(\\{x \\mid p(x)\\}) = \\{x \\mid (\\forall^\\mathrm{f} y \\in \\mathcal{N}(x), p(y))\\}$$$

Lean4

theorem interior_setOf_eq {p : X → Prop} : interior {x | p x} = {x | ∀ᶠ y in 𝓝 x, p y} :=
  interior_eq_nhds'

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