continuous_nhds — Mathlib

English

Let X be a topological space. The map x ↦ 𝓝 x from X to the space of filters on X is continuous.

Русский

Пусть X — топологическое пространство. Отображение x ↦ 𝓝(x) из X в пространство фильтров на X непрерывно.

LaTeX

$$$nhds:\\;X\\to\\mathcal{F}(X)\\ \\text{is continuous}$$$

Lean4

@[continuity]
theorem continuous_nhds : Continuous (𝓝 : X → Filter X) :=
  isInducing_nhds.continuous

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