gc_nhds — Mathlib

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⟩

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