isCountablyGenerated_nhdsWithin — Mathlib

English

If x has a countably generated neighborhood filter, then nhdsWithin x s is countably generated for any s.

Русский

Если окрестности точки x порождаются счётной базой, то окрестности внутри s тоже порождаются счётной базой.

LaTeX

$$$\\text{IsCountablyGenerated}(\\mathcal{N}_{x}^{\,s})$$$

Lean4

instance isCountablyGenerated_nhdsWithin (x : α) [IsCountablyGenerated (𝓝 x)] (s : Set α) :
    IsCountablyGenerated (𝓝[s] x) :=
  Inf.isCountablyGenerated _ _

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