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 |