:: Topology from Neighbourhoods
:: by Roland Coghetto
::
:: Received August 14, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


theorem :: FINTOPO7:1
for X being non empty set
for B, Y being Subset-Family of X st Y c= UniCl B holds
union Y in UniCl B
proof end;

theorem Th1: :: FINTOPO7:2
for X being non empty set
for B being empty Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
FinMeetCl B c= UniCl B
proof end;

theorem Th2: :: FINTOPO7:3
for X being non empty set
for B being non empty Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
FinMeetCl B c= UniCl B
proof end;

theorem Th3: :: FINTOPO7:4
for X being non empty set
for B being Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
( UniCl B = UniCl (FinMeetCl B) & TopStruct(# X,(UniCl B) #) is TopSpace-like )
proof end;

theorem :: FINTOPO7:5
for FMT being non empty FMT_Space_Str ex S being RelStr st
for x being Element of FMT holds U_FMT x is Subset of S
proof end;

registration
let T be non empty TopSpace;
cluster NeighSp T -> Fo_filled ;
coherence
NeighSp T is Fo_filled
proof end;
end;

definition
let ET be non empty strict FMT_Space_Str ;
let O be Subset of ET;
attr O is open means :Def1: :: FINTOPO7:def 1
for x being Element of ET st x in O holds
O in U_FMT x;
end;

:: deftheorem Def1 defines open FINTOPO7:def 1 :
for ET being non empty strict FMT_Space_Str
for O being Subset of ET holds
( O is open iff for x being Element of ET st x in O holds
O in U_FMT x );

definition
let ET be non empty strict FMT_Space_Str ;
attr ET is U_FMT_filter means :Def2: :: FINTOPO7:def 2
for x being Element of ET holds U_FMT x is Filter of the carrier of ET;
attr ET is U_FMT_with_point means :Def3: :: FINTOPO7:def 3
for x being Element of ET
for V being Element of U_FMT x holds x in V;
attr ET is U_FMT_local means :Def4: :: FINTOPO7:def 4
for x being Element of ET
for V being Element of U_FMT x ex W being Element of U_FMT x st
for y being Element of ET st y is Element of W holds
V is Element of U_FMT y;
end;

:: deftheorem Def2 defines U_FMT_filter FINTOPO7:def 2 :
for ET being non empty strict FMT_Space_Str holds
( ET is U_FMT_filter iff for x being Element of ET holds U_FMT x is Filter of the carrier of ET );

:: deftheorem Def3 defines U_FMT_with_point FINTOPO7:def 3 :
for ET being non empty strict FMT_Space_Str holds
( ET is U_FMT_with_point iff for x being Element of ET
for V being Element of U_FMT x holds x in V );

:: deftheorem Def4 defines U_FMT_local FINTOPO7:def 4 :
for ET being non empty strict FMT_Space_Str holds
( ET is U_FMT_local iff for x being Element of ET
for V being Element of U_FMT x ex W being Element of U_FMT x st
for y being Element of ET st y is Element of W holds
V is Element of U_FMT y );

theorem Th4: :: FINTOPO7:6
for ET being non empty strict FMT_Space_Str st ET is U_FMT_filter holds
for x being Element of ET holds not U_FMT x is empty ;

theorem :: FINTOPO7:7
for ET being non empty strict FMT_Space_Str st ET is U_FMT_with_point holds
ET is Fo_filled ;

theorem Th5: :: FINTOPO7:8
for ET being non empty strict FMT_Space_Str st ET is Fo_filled & ( for x being Element of ET holds not U_FMT x is empty ) holds
ET is U_FMT_with_point
proof end;

theorem :: FINTOPO7:9
for ET being non empty strict FMT_Space_Str st ET is Fo_filled & ET is U_FMT_filter holds
ET is U_FMT_with_point
proof end;

registration
cluster non empty strict U_FMT_filter U_FMT_with_point U_FMT_local for FMT_Space_Str ;
existence
ex b1 being non empty strict FMT_Space_Str st
( b1 is U_FMT_local & b1 is U_FMT_with_point & b1 is U_FMT_filter )
proof end;
end;

theorem Th6: :: FINTOPO7:10
for ET being non empty strict U_FMT_filter FMT_Space_Str
for x being Element of ET holds the carrier of ET in U_FMT x
proof end;

definition
let ET be non empty strict U_FMT_filter FMT_Space_Str ;
let x be Element of ET;
mode a_neighborhood of x -> Subset of ET means :Def5: :: FINTOPO7:def 5
it in U_FMT x;
existence
ex b1 being Subset of ET st b1 in U_FMT x
proof end;
end;

:: deftheorem Def5 defines a_neighborhood FINTOPO7:def 5 :
for ET being non empty strict U_FMT_filter FMT_Space_Str
for x being Element of ET
for b3 being Subset of ET holds
( b3 is a_neighborhood of x iff b3 in U_FMT x );

registration
let ET be non empty strict U_FMT_filter FMT_Space_Str ;
let x be Element of ET;
cluster open for a_neighborhood of x;
existence
ex b1 being a_neighborhood of x st b1 is open
proof end;
end;

definition
let ET be non empty strict U_FMT_filter FMT_Space_Str ;
let A be Subset of ET;
mode a_neighborhood of A -> Subset of ET means :Def6: :: FINTOPO7:def 6
for x being Element of ET st x in A holds
it in U_FMT x;
existence
ex b1 being Subset of ET st
for x being Element of ET st x in A holds
b1 in U_FMT x
proof end;
end;

:: deftheorem Def6 defines a_neighborhood FINTOPO7:def 6 :
for ET being non empty strict U_FMT_filter FMT_Space_Str
for A, b3 being Subset of ET holds
( b3 is a_neighborhood of A iff for x being Element of ET st x in A holds
b3 in U_FMT x );

registration
let ET be non empty strict U_FMT_filter FMT_Space_Str ;
let A be Subset of ET;
cluster open for a_neighborhood of A;
existence
ex b1 being a_neighborhood of A st b1 is open
proof end;
end;

theorem Th7: :: FINTOPO7:11
for ET being non empty strict U_FMT_filter FMT_Space_Str
for A being Subset of ET
for NA being a_neighborhood of A
for B being Subset of ET st NA c= B holds
B is a_neighborhood of A
proof end;

definition
let ET be non empty strict U_FMT_filter FMT_Space_Str ;
let A be Subset of ET;
func Neighborhood A -> Subset-Family of ET equals :: FINTOPO7:def 7
{ N where N is a_neighborhood of A : verum } ;
correctness
coherence
{ N where N is a_neighborhood of A : verum } is Subset-Family of ET
;
proof end;
end;

:: deftheorem defines Neighborhood FINTOPO7:def 7 :
for ET being non empty strict U_FMT_filter FMT_Space_Str
for A being Subset of ET holds Neighborhood A = { N where N is a_neighborhood of A : verum } ;

theorem Th7bis: :: FINTOPO7:12
for ET being non empty strict U_FMT_filter FMT_Space_Str
for A being non empty Subset of ET holds Neighborhood A is Filter of the carrier of ET
proof end;

definition
let ET be non empty strict FMT_Space_Str ;
attr ET is U_FMT_filter_base means :: FINTOPO7:def 8
for x being Element of the carrier of ET holds U_FMT x is filter_base of the carrier of ET;
end;

:: deftheorem defines U_FMT_filter_base FINTOPO7:def 8 :
for ET being non empty strict FMT_Space_Str holds
( ET is U_FMT_filter_base iff for x being Element of the carrier of ET holds U_FMT x is filter_base of the carrier of ET );

definition
let ET be non empty FMT_Space_Str ;
func <.ET.] -> Function of the carrier of ET,(bool (bool the carrier of ET)) means :Def7: :: FINTOPO7:def 9
for x being Element of the carrier of ET holds it . x = <.(U_FMT x).];
existence
ex b1 being Function of the carrier of ET,(bool (bool the carrier of ET)) st
for x being Element of the carrier of ET holds b1 . x = <.(U_FMT x).]
proof end;
uniqueness
for b1, b2 being Function of the carrier of ET,(bool (bool the carrier of ET)) st ( for x being Element of the carrier of ET holds b1 . x = <.(U_FMT x).] ) & ( for x being Element of the carrier of ET holds b2 . x = <.(U_FMT x).] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines <. FINTOPO7:def 9 :
for ET being non empty FMT_Space_Str
for b2 being Function of the carrier of ET,(bool (bool the carrier of ET)) holds
( b2 = <.ET.] iff for x being Element of the carrier of ET holds b2 . x = <.(U_FMT x).] );

definition
let ET be non empty strict FMT_Space_Str ;
func gen_filter ET -> non empty strict FMT_Space_Str equals :: FINTOPO7:def 10
FMT_Space_Str(# the carrier of ET,<.ET.] #);
correctness
coherence
FMT_Space_Str(# the carrier of ET,<.ET.] #) is non empty strict FMT_Space_Str
;
;
end;

:: deftheorem defines gen_filter FINTOPO7:def 10 :
for ET being non empty strict FMT_Space_Str holds gen_filter ET = FMT_Space_Str(# the carrier of ET,<.ET.] #);

theorem Th8: :: FINTOPO7:13
for ET being non empty strict FMT_Space_Str st ET is U_FMT_filter_base holds
gen_filter ET is U_FMT_filter
proof end;

definition
mode FMT_TopSpace is non empty strict U_FMT_filter U_FMT_with_point U_FMT_local FMT_Space_Str ;
end;

notation
let ET be FMT_TopSpace;
let x be Element of ET;
synonym NeighborhoodSystem x for U_FMT x;
end;

registration
let ET be FMT_TopSpace;
cluster open for Element of K24( the carrier of ET);
existence
ex b1 being Subset of ET st b1 is open
proof end;
end;

definition
let ET be FMT_TopSpace;
func Family_open_set ET -> non empty Subset-Family of the carrier of ET equals :: FINTOPO7:def 11
{ O where O is open Subset of ET : verum } ;
correctness
coherence
{ O where O is open Subset of ET : verum } is non empty Subset-Family of the carrier of ET
;
proof end;
end;

:: deftheorem defines Family_open_set FINTOPO7:def 11 :
for ET being FMT_TopSpace holds Family_open_set ET = { O where O is open Subset of ET : verum } ;

theorem Th9: :: FINTOPO7:14
for ET being FMT_TopSpace holds
( {} in Family_open_set ET & the carrier of ET in Family_open_set ET & ( for a being Subset-Family of ET st a c= Family_open_set ET holds
union a in Family_open_set ET ) & ( for a, b being Subset of ET st a in Family_open_set ET & b in Family_open_set ET holds
a /\ b in Family_open_set ET ) )
proof end;

theorem Th10: :: FINTOPO7:15
for ET being FMT_TopSpace
for a being Element of ET
for V being a_neighborhood of a ex O being open Subset of ET st
( a in O & O c= V )
proof end;

theorem Th11: :: FINTOPO7:16
for ET being FMT_TopSpace
for A being non empty Subset of ET
for V being Subset of ET holds
( V is a_neighborhood of A iff ex O being open Subset of ET st
( A c= O & O c= V ) )
proof end;

theorem :: FINTOPO7:17
for ET being FMT_TopSpace
for A being non empty Subset of ET holds Neighborhood A is Filter of the carrier of ET by Th7bis;

definition
let ET be FMT_TopSpace;
let A be non empty Subset of ET;
func OpenNeighborhoods A -> Subset-Family of the carrier of ET equals :: FINTOPO7:def 12
{ N where N is open a_neighborhood of A : verum } ;
correctness
coherence
{ N where N is open a_neighborhood of A : verum } is Subset-Family of the carrier of ET
;
proof end;
end;

:: deftheorem defines OpenNeighborhoods FINTOPO7:def 12 :
for ET being FMT_TopSpace
for A being non empty Subset of ET holds OpenNeighborhoods A = { N where N is open a_neighborhood of A : verum } ;

theorem :: FINTOPO7:18
for ET being FMT_TopSpace
for cF being Filter of the carrier of ET
for cS being non empty Subset of cF
for A being non empty Subset of ET st cF = Neighborhood A & cS = OpenNeighborhoods A holds
cS is filter_basis
proof end;

theorem Th12: :: FINTOPO7:19
for T being non empty TopSpace ex ET being FMT_TopSpace st
( the carrier of T = the carrier of ET & Family_open_set ET = the topology of T )
proof end;

theorem Th13: :: FINTOPO7:20
for T being non empty TopSpace
for ET being FMT_TopSpace st the carrier of T = the carrier of ET & Family_open_set ET = the topology of T holds
for x being Element of ET holds U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V )
}
proof end;

definition
let ET be FMT_TopSpace;
let F be Subset-Family of ET;
attr F is quasi_basis means :Def8: :: FINTOPO7:def 13
Family_open_set ET c= UniCl F;
end;

:: deftheorem Def8 defines quasi_basis FINTOPO7:def 13 :
for ET being FMT_TopSpace
for F being Subset-Family of ET holds
( F is quasi_basis iff Family_open_set ET c= UniCl F );

registration
let ET be FMT_TopSpace;
cluster Family_open_set ET -> non empty quasi_basis ;
coherence
Family_open_set ET is quasi_basis
proof end;
end;

registration
let ET be FMT_TopSpace;
cluster quasi_basis for Element of K24(K24( the carrier of ET));
existence
ex b1 being Subset-Family of ET st b1 is quasi_basis
proof end;
end;

definition
let ET be FMT_TopSpace;
let S be Subset-Family of ET;
attr S is open means :: FINTOPO7:def 14
S c= Family_open_set ET;
end;

:: deftheorem defines open FINTOPO7:def 14 :
for ET being FMT_TopSpace
for S being Subset-Family of ET holds
( S is open iff S c= Family_open_set ET );

registration
let ET be FMT_TopSpace;
cluster open for Element of K24(K24( the carrier of ET));
existence
ex b1 being Subset-Family of ET st b1 is open
proof end;
end;

registration
let ET be FMT_TopSpace;
cluster quasi_basis open for Element of K24(K24( the carrier of ET));
existence
ex b1 being Subset-Family of ET st
( b1 is open & b1 is quasi_basis )
proof end;
end;

definition
let ET be FMT_TopSpace;
mode Basis of ET is quasi_basis open Subset-Family of ET;
end;

theorem :: FINTOPO7:21
for ET being FMT_TopSpace
for B being Basis of ET holds Family_open_set ET = UniCl B
proof end;

theorem :: FINTOPO7:22
for X being non empty set
for B being non empty Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
ex ET being FMT_TopSpace st
( the carrier of ET = X & B is Basis of ET )
proof end;

theorem :: FINTOPO7:23
for ET being FMT_TopSpace
for B being Basis of ET holds
( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & the carrier of ET = union B )
proof end;

definition
let T be non empty TopSpace;
func TopSpace2FMT T -> FMT_TopSpace means :Def9: :: FINTOPO7:def 15
( the carrier of it = the carrier of T & Family_open_set it = the topology of T );
existence
ex b1 being FMT_TopSpace st
( the carrier of b1 = the carrier of T & Family_open_set b1 = the topology of T )
by Th12;
uniqueness
for b1, b2 being FMT_TopSpace st the carrier of b1 = the carrier of T & Family_open_set b1 = the topology of T & the carrier of b2 = the carrier of T & Family_open_set b2 = the topology of T holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines TopSpace2FMT FINTOPO7:def 15 :
for T being non empty TopSpace
for b2 being FMT_TopSpace holds
( b2 = TopSpace2FMT T iff ( the carrier of b2 = the carrier of T & Family_open_set b2 = the topology of T ) );

definition
let ET be FMT_TopSpace;
func FMT2TopSpace ET -> strict TopSpace means :Def10: :: FINTOPO7:def 16
( the carrier of it = the carrier of ET & Family_open_set ET = the topology of it );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = the carrier of ET & Family_open_set ET = the topology of b1 )
proof end;
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = the carrier of ET & Family_open_set ET = the topology of b1 & the carrier of b2 = the carrier of ET & Family_open_set ET = the topology of b2 holds
b1 = b2
;
end;

:: deftheorem Def10 defines FMT2TopSpace FINTOPO7:def 16 :
for ET being FMT_TopSpace
for b2 being strict TopSpace holds
( b2 = FMT2TopSpace ET iff ( the carrier of b2 = the carrier of ET & Family_open_set ET = the topology of b2 ) );

registration
let ET be FMT_TopSpace;
cluster FMT2TopSpace ET -> non empty strict ;
coherence
not FMT2TopSpace ET is empty
by Def10;
end;

theorem :: FINTOPO7:24
for T being non empty strict TopSpace holds T = FMT2TopSpace (TopSpace2FMT T)
proof end;

theorem :: FINTOPO7:25
for ET being FMT_TopSpace holds ET = TopSpace2FMT (FMT2TopSpace ET)
proof end;