English
If the neighborhood filter at x has a basis indexed by s with property p, and f is a dense-inducing map, then the neighborhood filter at f(x) has a basis indexed by closures of the images of s under f.
Русский
Если фильтр около точки x имеет базис, индексируемый множеством s, и f — плотностно-индуктивное отображение, то фильтр вокруг f(x) имеет базис, индексируемый замыканиями образов s под действием f.
LaTeX
$$$$\text{HasBasis}(\mathcal{N}_x, p, s) \Rightarrow \text{HasBasis}(\mathcal{N}_{f(x)}, p, \lambda i. \overline{f''s_i}).$$$$
Lean4
theorem hasBasis_of_isDenseInducing [TopologicalSpace α] [TopologicalSpace β] [RegularSpace β] {ι : Type*}
{s : ι → Set α} {p : ι → Prop} {x : α} (h : (𝓝 x).HasBasis p s) {f : α → β} (hf : IsDenseInducing f) :
(𝓝 (f x)).HasBasis p fun i => closure <| f '' s i :=
by
rw [Filter.hasBasis_iff] at h ⊢
intro T
refine ⟨fun hT => ?_, fun hT => ?_⟩
· obtain ⟨T', hT₁, hT₂, hT₃⟩ := exists_mem_nhds_isClosed_subset hT
have hT₄ : f ⁻¹' T' ∈ 𝓝 x := by
rw [hf.isInducing.nhds_eq_comap x]
exact ⟨T', hT₁, Subset.rfl⟩
obtain ⟨i, hi, hi'⟩ := (h _).mp hT₄
exact
⟨i, hi,
(closure_mono (image_mono hi')).trans (Subset.trans (closure_minimal (image_preimage_subset _ _) hT₂) hT₃)⟩
· obtain ⟨i, hi, hi'⟩ := hT
suffices closure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this] using hi'
replace h := (h (s i)).mpr ⟨i, hi, Subset.rfl⟩
exact hf.closure_image_mem_nhds h
