injective_nhdsSet — Mathlib

English

The operation s ↦ 𝓝ˢ(s) is injective on sets when X is a T1 space: if 𝓝ˢ(s) = 𝓝ˢ(t) then s = t.

Русский

Операция s ↦ 𝓝ˢ(s) инъективна на множества при T1-пространстве: если 𝓝ˢ(s) = 𝓝ˢ(t), то s = t.

LaTeX

$$$\text{nhdsSet}$ is injective: if 𝓝ˢ(s) = 𝓝ˢ(t) then s = t$$

Lean4

theorem injective_nhdsSet [T1Space X] : Function.Injective (𝓝ˢ : Set X → Filter X) := fun _ _ hst =>
  nhdsSet_inj_iff.mp hst

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