nhdsWithin_singleton — Mathlib

English

The neighborhood within a singleton equals the pure filter at that point.

Русский

Окрестность внутри множества, содержащего единственный элемент, равна чистому фильтру в этой точке.

LaTeX

$$$$ 𝓝[\\{a\\}] a = \\mathrm{pure}(a) $$$$

Lean4

@[simp]
theorem nhdsWithin_singleton (a : α) : 𝓝[{ a }] a = pure a := by
  rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]

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