Topology from Neighbourhoods

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 V_I, V_II, V_III and V_IV 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 V_I, V_II, V_III and V_IV 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].