nhdsWithin_diff_singleton — Mathlib

English

Let X be a T1 topological space. For any distinct points x ≠ y and any subset s ⊆ X, the neighborhoods of x within s \ {y} are the same as the neighborhoods of x within s.

Русский

Пусть X — топологическое пространство типа T1. Для любых x ≠ y и любого s ⊆ X множества окрестностей точки x внутри s \ {y} совпадают с окрестностями точки x внутри s.

LaTeX

$$$\\forall X [\\mathcal{T}_1(X)], \\forall x,y\\in X, x\\neq y, \\forall s\\subseteq X,\\nhdsWithin(x, s\\setminus\\{y\\}) = nhdsWithin(x, s).$$$

Lean4

theorem nhdsWithin_diff_singleton [T1Space X] {x y : X} (h : x ≠ y) (s : Set X) : 𝓝[s \ { y }] x = 𝓝[s] x :=
  by
  rw [diff_eq, inter_comm, nhdsWithin_inter_of_mem]
  exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)

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