specializes_iff_nhdsKer_subset — Mathlib

English

In a topological space, x specializes to y if and only if the kernel of the neighborhood filter at x is contained in the kernel at y.

Русский

В топологическом пространстве x специализируется на y тогда, когда пересечение всех окрестностей x содержится в пересечении всех окрестностей y.

LaTeX

$$$Specializes(x,y) \\iff nhdsKer(\\{x\\}) \\subseteq nhdsKer(\\{y\\})$$$

Lean4

theorem specializes_iff_nhdsKer_subset : x ⤳ y ↔ nhdsKer { x } ⊆ nhdsKer { y } := by simp [Specializes]

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