instIsCountablyGeneratedNhds — Mathlib

English

Let l be a filter on α which is countably generated. Then its neighborhood filter 𝓝 l is also countably generated.

Русский

Пусть l — фильтр на α и l является счётно порождённым. Тогда окрестности 𝓝 l тоже счётно порожденны.

LaTeX

$$$\forall \{\alpha : Type\}, \forall l : \text{Filter}(\alpha),\; [ \text{IsCountablyGenerated}(l) ] \Rightarrow \text{IsCountablyGenerated}(\mathcal{N}l).$$$

Lean4

/-- Neighborhoods of a countably generated filter is a countably generated filter. -/
instance {l : Filter α} [IsCountablyGenerated l] : IsCountablyGenerated (𝓝 l) :=
  let ⟨_b, hb⟩ := l.exists_antitone_basis
  HasCountableBasis.isCountablyGenerated <| ⟨hb.nhds, Set.to_countable _⟩

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