Topology from Neighbourhoods

Abstract

Using Mizar [9], and the formal topological space structure (FMT_Space_Str) [19], we introduce the three U-FMT conditions (U-FMT filter, U-FMT with point and U-FMT local) similar to those VI, VII, VIII and VIV of the proposition 2 in [10]: If to each element x of a set X there corresponds a set B(x) of subsets of X such that the properties VI, VII, VIII and VIV are satisfied, then there is a unique topological structure on X such that, for each x ∈ X, B(x) is the set of neighborhoods of x in this topology.We present a correspondence between a topological space and a space defined with the formal topological space structure with the three U-FMT conditions called the topology from neighbourhoods. For the formalization, we were inspired by the works of Bourbaki [11] and Claude Wagschal [31].