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)