English
Construct a topology on α from a neighborhood filter function n: α → Filter α by declaring a set open iff it is stable under neighborhood membership across all points in the set.
Русский
Сконструировать топологию на α из семейства фильтров окрестностей; множество считается открытым, если для каждого элемента множества он принадлежит его окрестности.
LaTeX
$$$\\mathrm{TopologicalSpace.mkOfNhds}(n)$ defined by $\\text{IsOpen}(s) \\iff ∀ a ∈ s, s ∈ n(a)$.$$
Lean4
/-- Construct a topology on α given the filter of neighborhoods of each point of α. -/
protected def mkOfNhds (n : α → Filter α) : TopologicalSpace α
where
IsOpen s := ∀ a ∈ s, s ∈ n a
isOpen_univ _ _ := univ_mem
isOpen_inter := fun _s _t hs ht x ⟨hxs, hxt⟩ => inter_mem (hs x hxs) (ht x hxt)
isOpen_sUnion := fun _s hs _a ⟨x, hx, hxa⟩ => mem_of_superset (hs x hx _ hxa) (subset_sUnion_of_mem hx)
