le_nhds_iff — Mathlib

English

A filter lies below the neighborhood filter at x iff it contains every open set around x.

Русский

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

LaTeX

$$$f \\le\\mathcal N_x \\iff \\forall s: Set X, x\\in s \\land IsOpen s \\Rightarrow s \\in f$$$

Lean4

/-- A filter lies below the neighborhood filter at `x` iff it contains every open set around `x`. -/
theorem le_nhds_iff {f} : f ≤ 𝓝 x ↔ ∀ s : Set X, x ∈ s → IsOpen s → s ∈ f := by simp [nhds_def]

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