English
nhdsAdjoint is left adjoint to the operation sending a topology to its neighborhood filter at a.
Русский
nhdsAdjoint является левой частной связью к операции перехода топологии к ее окрестностной фильтрации в точке a.
LaTeX
$$theorem gc_nhds (a : α) : GaloisConnection (nhdsAdjoint a) (fun t => @nhds α t a)$$
Lean4
theorem gc_nhds (a : α) : GaloisConnection (nhdsAdjoint a) fun t => @nhds α t a := fun f t =>
by
rw [le_nhds_iff]
exact ⟨fun H s hs has => H _ has hs, fun H s has hs => H _ hs has⟩