isInducing_nhds — Mathlib

English

The map x ↦ 𝓝 x is an inducing map from X into the space of filters on X; i.e., the topology on X is the initial topology induced by nhds.

Русский

Отображение x ↦ 𝓝 x является индуктивным отображением из X в пространство фильтров на X; топология X есть начальная топология от nhds.

LaTeX

$$$\text{IsInducing}(\, x \mapsto 𝓝 x\:).$$$

Lean4

theorem isInducing_nhds : IsInducing (𝓝 : X → Filter X) :=
  isInducing_iff_nhds.2 fun x =>
    (nhds_def' _).trans <| by
      simp +contextual only [nhds_nhds, comap_iInf, comap_principal, Iic_principal, preimage_setOf_eq,
        ← mem_interior_iff_mem_nhds, setOf_mem_eq, IsOpen.interior_eq]

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