closure_image_mem_nhds — Mathlib

English

If s is a subset of α near a, then closure of i''s is a neighborhood of i(a).

Русский

Если s близко к a в α, то closure(i''s) образует окрестность i(a) в β.

LaTeX

$$$ IsDenseInducing\\ i \\to \\forall s\\in 𝓝 a, closure(i''s) \\in 𝓝 (i a)$$$

Lean4

theorem closure_image_mem_nhds {s : Set α} {a : α} (di : IsDenseInducing i) (hs : s ∈ 𝓝 a) :
    closure (i '' s) ∈ 𝓝 (i a) :=
  by
  rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs
  rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩
  refine mem_of_superset (hUo.mem_nhds haU) ?_
  calc
    U ⊆ closure (i '' (i ⁻¹' U)) := di.dense.subset_closure_image_preimage_of_isOpen hUo
    _ ⊆ closure (i '' s) := closure_mono (image_mono sub)

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