nhds_le_nhdsSet_iff — Mathlib

English

For a point x and a set s in a T1 space, the neighborhood of the point is below the neighborhood filter of s exactly when x ∈ s.

Русский

Для точки x и множества s в T1-пространстве окрестности точки лежат ниже фильтра окрестностей s тогда, когда x ∈ s.

LaTeX

$$$\mathcal{N} x \le \mathcal{N}^{\mathrm{set}}(s) \iff x \in s$$$

Lean4

@[simp]
theorem nhds_le_nhdsSet_iff [T1Space X] {s : Set X} {x : X} : 𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s := by
  rw [← nhdsSet_singleton, nhdsSet_le_iff, singleton_subset_iff]

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