nhds_subtype — Mathlib

English

In the subspace topology on a subset s ⊆ X, the neighborhood of x ∈ {x ∈ s} is the comap of the inclusion map with 𝓝(x).

Русский

В подпобочной топологии на подмножестве s ⊆ X окрестности x ∈ {x ∈ s} равны вычислению обратного образа через включение с 𝓝(x).

LaTeX

$$$ \\mathcal{N}_{\\text{Subtype}}(x) = \\operatorname{comap}(\\iota)(\\mathcal{N}_{X}(x)) $, where $\\iota$ is the inclusion.$$

Lean4

theorem nhds_subtype (s : Set X) (x : { x // x ∈ s }) : 𝓝 x = comap (↑) (𝓝 (x : X)) :=
  nhds_induced _ x

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