nhds_eq_comap — Mathlib

English

For a dense inducing i, the neighborhood filter at a is the pullback along i of the neighborhood filter at i(a).

Русский

Для плотного индуцирующего отображения i окрестности точки a совпадают с обратным спектром окрестностей i(a).

LaTeX

$$$\\forall a,\\ \\mathcal{N}(a) = \\operatorname{comap} i (\\mathcal{N}(i a))$$$

Lean4

theorem nhds_eq_comap (di : IsDenseInducing i) : ∀ a : α, 𝓝 a = comap i (𝓝 <| i a) :=
  di.isInducing.nhds_eq_comap

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