English
The neighborhood filter at a point x in a UniformSpace.Core corresponds to the comap of the uniformity by the map x ↦ (x, -).
Русский
Окрёжностный фильтр в точке x в UniformSpace.Core равен обратному образу равномерности по отображению x ↦ (x, -).
LaTeX
$$$\\forall x,\\ \\mathrm{nhds}_{u.toTopologicalSpace}(x) = \\mathrm{comap}(\\mathrm{Prod.mk}\;x)\\,u.uniformity$$$
Lean4
theorem nhds_toTopologicalSpace {α : Type u} (u : Core α) (x : α) :
@nhds α u.toTopologicalSpace x = comap (Prod.mk x) u.uniformity :=
by
apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun _ ↦ (basis_sets _).comap _)
· exact fun a U hU ↦ u.refl hU rfl
· intro a U hU
rcases u.comp_mem_uniformity_sets hU with ⟨V, hV, hVU⟩
filter_upwards [preimage_mem_comap hV] with b hb
filter_upwards [preimage_mem_comap hV] with c hc
exact
hVU
⟨b, hb, hc⟩
-- the topological structure is embedded in the uniform structure
-- to avoid instance diamond issues. See Note [forgetful inheritance].
