comap_nhds_neBot — Mathlib

English

For a dense inducing i, the comap of nhds b along i is nontrivial.

Русский

Для плотного индуциирующего отображения i обратное образ окрестностей относительно b не тривиально.

LaTeX

$$$ \\text{comap } i (\\mathcal{N} b) \\text{ is NeBot}$$$

Lean4

theorem comap_nhds_neBot (di : IsDenseInducing i) (b : β) : NeBot (comap i (𝓝 b)) :=
  comap_neBot fun s hs =>
    by
    rcases mem_closure_iff_nhds.1 (di.dense b) s hs with ⟨_, ⟨ha, a, rfl⟩⟩
    exact ⟨a, ha⟩

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