English
This construction defines a topology on α from a fixed point a and a filter f: open sets are those containing a imply membership in f.
Русский
Это построение задаёт топологию на α из фиксированной точки a и фильтра f: открытые множества — те, для которых a ∈ s влечёт s ∈ f.
LaTeX
$$def nhdsAdjoint (a : α) (f : Filter α) : TopologicalSpace α where IsOpen s := a ∈ s → s ∈ f$$
Lean4
/-- This construction is left adjoint to the operation sending a topology on `α`
to its neighborhood filter at a fixed point `a : α`. -/
def nhdsAdjoint (a : α) (f : Filter α) : TopologicalSpace α
where
IsOpen s := a ∈ s → s ∈ f
isOpen_univ _ := univ_mem
isOpen_inter := fun _s _t hs ht ⟨has, hat⟩ => inter_mem (hs has) (ht hat)
isOpen_sUnion := fun _k hk ⟨u, hu, hau⟩ => mem_of_superset (hk u hu hau) (subset_sUnion_of_mem hu)
