nhdsWithin_of_mem_discrete — Mathlib

English

If s is a discrete subset and x ∈ s, then the neighborhood filter within s at x equals the pure filter at x: 𝓝[s] x = pure x.

Русский

Если s — дискретное подмножество и x ∈ s, то 𝓝[s] x = pure x.

LaTeX

$$$ \\forall X [TopologicalSpace X], \\forall s \\subseteq X [DiscreteTopology s], \\forall x \\in s, 𝓝[s] x = \\mathrm{pure}(x). $$$

Lean4

/-- The neighbourhoods filter of `x` within `s`, under the discrete topology, is equal to
the pure `x` filter (which is the principal filter at the singleton `{x}`.) -/
theorem nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) : 𝓝[s] x = pure x :=
  le_antisymm (le_pure_iff.2 <| singleton_mem_nhdsWithin_of_mem_discrete hx) (pure_le_nhdsWithin hx)

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