nhdsSet_inj_iff — Mathlib

English

In a T1 space, equality of neighborhood-set filters characterizes equality of the sets themselves: 𝓝ˢ(s) = 𝓝ˢ(t) if and only if s = t.

Русский

В T1-пространстве равенство фильтров окрестностей множества определяется равенством самих множеств: 𝓝ˢ(s) = 𝓝ˢ(t) эквивално s = t.

LaTeX

$$$\mathcal{N}_{\mathrm{nhds}}(s) = \mathcal{N}_{\mathrm{nhds}}(t) \iff s = t$$$

Lean4

@[simp]
theorem nhdsSet_inj_iff [T1Space X] {s t : Set X} : 𝓝ˢ s = 𝓝ˢ t ↔ s = t :=
  by
  simp_rw [le_antisymm_iff]
  exact and_congr nhdsSet_le_iff nhdsSet_le_iff

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