mem_nhds_iff — Mathlib

English

For a filter l on α and a set S of filters, S belongs to the neighborhood filter 𝓝 l iff there exists t ∈ l such that Iic(𝓟 t) ⊆ S.

Русский

Для фильтра l на α и множества S фильтров: S ∈ 𝓝 l тогда и только тогда, когда существует t ∈ l such that Iic(𝓟 t) ⊆ S.

LaTeX

$$$\forall {\alpha}, {l : \text{Filter}(\alpha)}, {S : \text{Set}(\text{Filter}(\alpha))},\; S ∈ 𝓝 l \iff \exists t \in l, Iic (\mathcal{P} t) \subseteq S.$$$

Lean4

protected theorem mem_nhds_iff {l : Filter α} {S : Set (Filter α)} : S ∈ 𝓝 l ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ S :=
  l.basis_sets.nhds.mem_iff

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