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 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)...
Main Author: | |
---|---|
Format: | Article |
Language: | English |
Published: |
Sciendo
2015-12-01
|
Series: | Formalized Mathematics |
Subjects: | |
Online Access: | https://doi.org/10.1515/forma-2015-0023 |
Summary: | 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. |
---|---|
ISSN: | 1426-2630 1898-9934 |