:: PRE_TOPC semantic presentation
begin
definition
attrc1 is strict ;
struct TopStruct -> 1-sorted ;
aggrTopStruct(# carrier, topology #) -> TopStruct ;
sel topology c1 -> Subset-Family of the carrier of c1;
end;
definition
let IT be TopStruct ;
attrIT is TopSpace-like means :Def1: :: PRE_TOPC:def 1
( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds
union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds
a /\ b in the topology of IT ) );
end;
:: deftheorem Def1 defines TopSpace-like PRE_TOPC:def_1_:_
for IT being TopStruct holds
( IT is TopSpace-like iff ( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds
union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds
a /\ b in the topology of IT ) ) );
registration
cluster non empty strict TopSpace-like for TopStruct ;
existence
ex b1 being TopStruct st
( not b1 is empty & b1 is strict & b1 is TopSpace-like )
proof
now__::_thesis:_ex_X_being_set_ex_T_being_Subset-Family_of_X_st_
(_the_carrier_of_TopStruct(#_X,T_#)_in_the_topology_of_TopStruct(#_X,T_#)_&_(_for_a_being_Subset-Family_of_TopStruct(#_X,T_#)_st_a_c=_the_topology_of_TopStruct(#_X,T_#)_holds_
union_a_in_the_topology_of_TopStruct(#_X,T_#)_)_&_(_for_a,_b_being_Subset_of_TopStruct(#_X,T_#)_st_a_in_the_topology_of_TopStruct(#_X,T_#)_&_b_in_the_topology_of_TopStruct(#_X,T_#)_holds_
a_/\_b_in_the_topology_of_TopStruct(#_X,T_#)_)_)
take X = {{}}; ::_thesis: ex T being Subset-Family of X st
( the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) & ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) )
set T = {{},X};
{{},X} c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{},X} or x in bool X )
assume x in {{},X} ; ::_thesis: x in bool X
then ( x = {} or x = X ) by TARSKI:def_2;
then x c= X by XBOOLE_1:2;
hence x in bool X ; ::_thesis: verum
end;
then reconsider T = {{},X} as Subset-Family of X ;
take T = T; ::_thesis: ( the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) & ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) )
set Y = TopStruct(# X,T #);
thus the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) by TARSKI:def_2; ::_thesis: ( ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) )
thus for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ::_thesis: for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #)
proof
let a be Subset-Family of TopStruct(# X,T #); ::_thesis: ( a c= the topology of TopStruct(# X,T #) implies union a in the topology of TopStruct(# X,T #) )
assume a c= the topology of TopStruct(# X,T #) ; ::_thesis: union a in the topology of TopStruct(# X,T #)
then ( a = {} or a = {{}} or a = {X} or a = {{},X} ) by ZFMISC_1:36;
then ( union a = {} or union a = X or union a = {} \/ X ) by ZFMISC_1:2, ZFMISC_1:25, ZFMISC_1:75;
hence union a in the topology of TopStruct(# X,T #) by TARSKI:def_2; ::_thesis: verum
end;
let a, b be Subset of TopStruct(# X,T #); ::_thesis: ( a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) implies a /\ b in the topology of TopStruct(# X,T #) )
assume that
A1: a in the topology of TopStruct(# X,T #) and
A2: b in the topology of TopStruct(# X,T #) ; ::_thesis: a /\ b in the topology of TopStruct(# X,T #)
A3: ( b = {} or b = X ) by A2, TARSKI:def_2;
( a = {} or a = X ) by A1, TARSKI:def_2;
hence a /\ b in the topology of TopStruct(# X,T #) by A3, TARSKI:def_2; ::_thesis: verum
end;
then consider X being non empty set , T being Subset-Family of X such that
A4: ( the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) & ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) ) ;
take TopStruct(# X,T #) ; ::_thesis: ( not TopStruct(# X,T #) is empty & TopStruct(# X,T #) is strict & TopStruct(# X,T #) is TopSpace-like )
thus not TopStruct(# X,T #) is empty ; ::_thesis: ( TopStruct(# X,T #) is strict & TopStruct(# X,T #) is TopSpace-like )
thus ( TopStruct(# X,T #) is strict & TopStruct(# X,T #) is TopSpace-like ) by A4, Def1; ::_thesis: verum
end;
end;
definition
mode TopSpace is TopSpace-like TopStruct ;
end;
definition
let S be 1-sorted ;
mode Point of S is Element of S;
end;
registration
let T be TopSpace;
cluster the topology of T -> non empty ;
coherence
not the topology of T is empty by Def1;
end;
theorem Th1: :: PRE_TOPC:1
for GX being TopSpace holds {} in the topology of GX
proof
let GX be TopSpace; ::_thesis: {} in the topology of GX
reconsider A = {} as Subset-Family of GX by XBOOLE_1:2;
A c= the topology of GX by XBOOLE_1:2;
hence {} in the topology of GX by Def1, ZFMISC_1:2; ::_thesis: verum
end;
theorem :: PRE_TOPC:2
for T being 1-sorted
for P being Subset of T holds P \/ (P `) = [#] T
proof
let T be 1-sorted ; ::_thesis: for P being Subset of T holds P \/ (P `) = [#] T
let P be Subset of T; ::_thesis: P \/ (P `) = [#] T
P \/ (P `) = [#] the carrier of T by SUBSET_1:10
.= the carrier of T ;
hence P \/ (P `) = [#] T ; ::_thesis: verum
end;
theorem Th3: :: PRE_TOPC:3
for T being 1-sorted
for P being Subset of T holds ([#] T) \ (([#] T) \ P) = P
proof
let T be 1-sorted ; ::_thesis: for P being Subset of T holds ([#] T) \ (([#] T) \ P) = P
let P be Subset of T; ::_thesis: ([#] T) \ (([#] T) \ P) = P
([#] T) \ (([#] T) \ P) = P /\ ([#] T) by XBOOLE_1:48;
hence ([#] T) \ (([#] T) \ P) = P by XBOOLE_1:28; ::_thesis: verum
end;
theorem Th4: :: PRE_TOPC:4
for T being 1-sorted
for P being Subset of T holds
( P <> [#] T iff ([#] T) \ P <> {} )
proof
let T be 1-sorted ; ::_thesis: for P being Subset of T holds
( P <> [#] T iff ([#] T) \ P <> {} )
let P be Subset of T; ::_thesis: ( P <> [#] T iff ([#] T) \ P <> {} )
now__::_thesis:_(_P_<>_[#]_T_implies_not_([#]_T)_\_P_=_{}_)
assume that
A1: P <> [#] T and
A2: ([#] T) \ P = {} ; ::_thesis: contradiction
[#] T c= P by A2, XBOOLE_1:37;
hence contradiction by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
hence ( P <> [#] T iff ([#] T) \ P <> {} ) by XBOOLE_1:37; ::_thesis: verum
end;
theorem :: PRE_TOPC:5
for T being 1-sorted
for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds
Q = ([#] T) \ P
proof
let T be 1-sorted ; ::_thesis: for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds
Q = ([#] T) \ P
let P, Q be Subset of T; ::_thesis: ( [#] T = P \/ Q & P misses Q implies Q = ([#] T) \ P )
assume that
A1: [#] T = P \/ Q and
A2: P misses Q ; ::_thesis: Q = ([#] T) \ P
([#] T) \ P = Q \ P by A1, XBOOLE_1:40
.= Q by A2, XBOOLE_1:83 ;
hence Q = ([#] T) \ P ; ::_thesis: verum
end;
theorem :: PRE_TOPC:6
for T being 1-sorted holds [#] T = ({} T) ` ;
definition
let T be TopStruct ;
let P be Subset of T;
attrP is open means :Def2: :: PRE_TOPC:def 2
P in the topology of T;
end;
:: deftheorem Def2 defines open PRE_TOPC:def_2_:_
for T being TopStruct
for P being Subset of T holds
( P is open iff P in the topology of T );
definition
let T be TopStruct ;
let P be Subset of T;
attrP is closed means :Def3: :: PRE_TOPC:def 3
([#] T) \ P is open ;
end;
:: deftheorem Def3 defines closed PRE_TOPC:def_3_:_
for T being TopStruct
for P being Subset of T holds
( P is closed iff ([#] T) \ P is open );
definition
let T be TopStruct ;
mode SubSpace of T -> TopStruct means :Def4: :: PRE_TOPC:def 4
( [#] it c= [#] T & ( for P being Subset of it holds
( P in the topology of it iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] it) ) ) ) );
existence
ex b1 being TopStruct st
( [#] b1 c= [#] T & ( for P being Subset of b1 holds
( P in the topology of b1 iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] b1) ) ) ) )
proof
take T ; ::_thesis: ( [#] T c= [#] T & ( for P being Subset of T holds
( P in the topology of T iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) ) ) )
thus [#] T c= [#] T ; ::_thesis: for P being Subset of T holds
( P in the topology of T iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) )
let P be Subset of T; ::_thesis: ( P in the topology of T iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) )
hereby ::_thesis: ( ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) implies P in the topology of T )
assume A1: P in the topology of T ; ::_thesis: ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) )
take Q = P; ::_thesis: ( Q in the topology of T & P = Q /\ ([#] T) )
thus Q in the topology of T by A1; ::_thesis: P = Q /\ ([#] T)
thus P = Q /\ ([#] T) by XBOOLE_1:28; ::_thesis: verum
end;
given Q being Subset of T such that A2: ( Q in the topology of T & P = Q /\ ([#] T) ) ; ::_thesis: P in the topology of T
thus P in the topology of T by A2, XBOOLE_1:28; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines SubSpace PRE_TOPC:def_4_:_
for T, b2 being TopStruct holds
( b2 is SubSpace of T iff ( [#] b2 c= [#] T & ( for P being Subset of b2 holds
( P in the topology of b2 iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] b2) ) ) ) ) );
Lm1: for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
proof
let T be TopStruct ; ::_thesis: TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
set S = TopStruct(# the carrier of T, the topology of T #);
thus [#] TopStruct(# the carrier of T, the topology of T #) c= [#] T ; :: according to PRE_TOPC:def_4 ::_thesis: for P being Subset of TopStruct(# the carrier of T, the topology of T #) holds
( P in the topology of TopStruct(# the carrier of T, the topology of T #) iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) )
let P be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( P in the topology of TopStruct(# the carrier of T, the topology of T #) iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) )
hereby ::_thesis: ( ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) implies P in the topology of TopStruct(# the carrier of T, the topology of T #) )
reconsider Q = P as Subset of T ;
assume A1: P in the topology of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) )
take Q = Q; ::_thesis: ( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) )
thus Q in the topology of T by A1; ::_thesis: P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #))
thus P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) by XBOOLE_1:28; ::_thesis: verum
end;
given Q being Subset of T such that A2: ( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ; ::_thesis: P in the topology of TopStruct(# the carrier of T, the topology of T #)
thus P in the topology of TopStruct(# the carrier of T, the topology of T #) by A2, XBOOLE_1:28; ::_thesis: verum
end;
registration
let T be TopStruct ;
cluster strict for SubSpace of T;
existence
ex b1 being SubSpace of T st b1 is strict
proof
TopStruct(# the carrier of T, the topology of T #) is SubSpace of T by Lm1;
hence ex b1 being SubSpace of T st b1 is strict ; ::_thesis: verum
end;
end;
registration
let T be non empty TopStruct ;
cluster non empty strict for SubSpace of T;
existence
ex b1 being SubSpace of T st
( b1 is strict & not b1 is empty )
proof
( TopStruct(# the carrier of T, the topology of T #) is SubSpace of T & not TopStruct(# the carrier of T, the topology of T #) is empty ) by Lm1;
hence ex b1 being SubSpace of T st
( b1 is strict & not b1 is empty ) ; ::_thesis: verum
end;
end;
registration
let T be TopSpace;
cluster -> TopSpace-like for SubSpace of T;
coherence
for b1 being SubSpace of T holds b1 is TopSpace-like
proof
let S be SubSpace of T; ::_thesis: S is TopSpace-like
S is TopSpace-like
proof
set P = the carrier of S;
A1: [#] T in the topology of T by Def1;
A2: the carrier of S = [#] S ;
then the carrier of S c= [#] T by Def4;
then ([#] T) /\ the carrier of S = the carrier of S by XBOOLE_1:28;
hence the carrier of S in the topology of S by A2, A1, Def4; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for a being Subset-Family of S st a c= the topology of S holds
union a in the topology of S ) & ( for a, b being Subset of S st a in the topology of S & b in the topology of S holds
a /\ b in the topology of S ) )
thus for a being Subset-Family of S st a c= the topology of S holds
union a in the topology of S ::_thesis: for a, b being Subset of S st a in the topology of S & b in the topology of S holds
a /\ b in the topology of S
proof
let a be Subset-Family of S; ::_thesis: ( a c= the topology of S implies union a in the topology of S )
assume A3: a c= the topology of S ; ::_thesis: union a in the topology of S
defpred S1[ set ] means ( T /\ the carrier of S in a & T in the topology of T );
consider b being Subset-Family of T such that
A4: for Z being Subset of T holds
( Z in b iff S1[Z] ) from SUBSET_1:sch_3();
A5: (union b) /\ the carrier of S c= union a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union b) /\ the carrier of S or x in union a )
assume A6: x in (union b) /\ the carrier of S ; ::_thesis: x in union a
then x in union b by XBOOLE_0:def_4;
then consider Z being set such that
A7: x in Z and
A8: Z in b by TARSKI:def_4;
x in the carrier of S by A6, XBOOLE_0:def_4;
then A9: x in Z /\ the carrier of S by A7, XBOOLE_0:def_4;
Z /\ the carrier of S in a by A4, A8;
hence x in union a by A9, TARSKI:def_4; ::_thesis: verum
end;
b c= the topology of T
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in b or y in the topology of T )
assume y in b ; ::_thesis: y in the topology of T
hence y in the topology of T by A4; ::_thesis: verum
end;
then A10: union b in the topology of T by Def1;
union a c= (union b) /\ the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union a or x in (union b) /\ the carrier of S )
assume A11: x in union a ; ::_thesis: x in (union b) /\ the carrier of S
then consider Z1 being set such that
A12: x in Z1 and
A13: Z1 in a by TARSKI:def_4;
consider Z3 being Subset of T such that
A14: ( Z3 in the topology of T & Z1 = Z3 /\ the carrier of S ) by A2, A3, A13, Def4;
( Z3 in b & x in Z3 ) by A4, A12, A13, A14, XBOOLE_0:def_4;
then x in union b by TARSKI:def_4;
hence x in (union b) /\ the carrier of S by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
then union a = (union b) /\ the carrier of S by A5, XBOOLE_0:def_10;
hence union a in the topology of S by A2, A10, Def4; ::_thesis: verum
end;
thus for V, Q being Subset of S st V in the topology of S & Q in the topology of S holds
V /\ Q in the topology of S ::_thesis: verum
proof
let V, Q be Subset of S; ::_thesis: ( V in the topology of S & Q in the topology of S implies V /\ Q in the topology of S )
assume that
A15: V in the topology of S and
A16: Q in the topology of S ; ::_thesis: V /\ Q in the topology of S
consider P1 being Subset of T such that
A17: P1 in the topology of T and
A18: V = P1 /\ the carrier of S by A2, A15, Def4;
consider Q1 being Subset of T such that
A19: Q1 in the topology of T and
A20: Q = Q1 /\ the carrier of S by A2, A16, Def4;
A21: V /\ Q = P1 /\ ((Q1 /\ the carrier of S) /\ the carrier of S) by A18, A20, XBOOLE_1:16
.= P1 /\ (Q1 /\ ( the carrier of S /\ the carrier of S)) by XBOOLE_1:16
.= (P1 /\ Q1) /\ the carrier of S by XBOOLE_1:16 ;
P1 /\ Q1 in the topology of T by A17, A19, Def1;
hence V /\ Q in the topology of S by A2, A21, Def4; ::_thesis: verum
end;
end;
hence S is TopSpace-like ; ::_thesis: verum
end;
end;
definition
let T be TopStruct ;
let P be Subset of T;
funcT | P -> strict SubSpace of T means :Def5: :: PRE_TOPC:def 5
[#] it = P;
existence
ex b1 being strict SubSpace of T st [#] b1 = P
proof
defpred S1[ set ] means ex Q being Subset of T st
( Q in the topology of T & $1 = Q /\ P );
consider top1 being Subset-Family of P such that
A1: for Z being Subset of P holds
( Z in top1 iff S1[Z] ) from SUBSET_1:sch_3();
reconsider top1 = top1 as Subset-Family of P ;
set Y = TopStruct(# P,top1 #);
A2: for Z being Subset of TopStruct(# P,top1 #) holds
( Z in top1 iff ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) )
proof
let Z be Subset of TopStruct(# P,top1 #); ::_thesis: ( Z in top1 iff ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) )
thus ( Z in top1 implies ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) ) ::_thesis: ( ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) implies Z in top1 )
proof
assume Z in top1 ; ::_thesis: ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) )
then S1[Z] by A1;
hence ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) ; ::_thesis: verum
end;
thus ( ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) implies Z in top1 ) by A1; ::_thesis: verum
end;
[#] TopStruct(# P,top1 #) c= [#] T ;
then reconsider Y = TopStruct(# P,top1 #) as strict SubSpace of T by A2, Def4;
take Y ; ::_thesis: [#] Y = P
thus [#] Y = P ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict SubSpace of T st [#] b1 = P & [#] b2 = P holds
b1 = b2
proof
let Z1, Z2 be strict SubSpace of T; ::_thesis: ( [#] Z1 = P & [#] Z2 = P implies Z1 = Z2 )
assume A3: ( [#] Z1 = P & [#] Z2 = P ) ; ::_thesis: Z1 = Z2
A4: the topology of Z2 c= the topology of Z1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of Z2 or x in the topology of Z1 )
assume x in the topology of Z2 ; ::_thesis: x in the topology of Z1
then ex Q being Subset of T st
( Q in the topology of T & x = Q /\ ([#] Z1) ) by A3, Def4;
hence x in the topology of Z1 by Def4; ::_thesis: verum
end;
the topology of Z1 c= the topology of Z2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of Z1 or x in the topology of Z2 )
assume x in the topology of Z1 ; ::_thesis: x in the topology of Z2
then ex Q being Subset of T st
( Q in the topology of T & x = Q /\ ([#] Z2) ) by A3, Def4;
hence x in the topology of Z2 by Def4; ::_thesis: verum
end;
hence Z1 = Z2 by A3, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines | PRE_TOPC:def_5_:_
for T being TopStruct
for P being Subset of T
for b3 being strict SubSpace of T holds
( b3 = T | P iff [#] b3 = P );
registration
let T be non empty TopStruct ;
let P be non empty Subset of T;
clusterT | P -> non empty strict ;
coherence
not T | P is empty
proof
[#] (T | P) = P by Def5;
hence not the carrier of (T | P) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
registration
let T be TopSpace;
cluster strict TopSpace-like for SubSpace of T;
existence
ex b1 being SubSpace of T st
( b1 is TopSpace-like & b1 is strict )
proof
set X = the strict SubSpace of T;
take the strict SubSpace of T ; ::_thesis: ( the strict SubSpace of T is TopSpace-like & the strict SubSpace of T is strict )
thus ( the strict SubSpace of T is TopSpace-like & the strict SubSpace of T is strict ) ; ::_thesis: verum
end;
end;
registration
let T be TopSpace;
let P be Subset of T;
clusterT | P -> strict TopSpace-like ;
coherence
T | P is TopSpace-like ;
end;
theorem :: PRE_TOPC:7
for S being TopSpace
for P1, P2 being Subset of S
for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds
S | P1 = (S | P2) | P19
proof
let S be TopSpace; ::_thesis: for P1, P2 being Subset of S
for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds
S | P1 = (S | P2) | P19
let P1, P2 be Subset of S; ::_thesis: for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds
S | P1 = (S | P2) | P19
let P19 be Subset of (S | P2); ::_thesis: ( P1 = P19 & P1 c= P2 implies S | P1 = (S | P2) | P19 )
assume that
A1: P1 = P19 and
A2: P1 c= P2 ; ::_thesis: S | P1 = (S | P2) | P19
A3: [#] ((S | P2) | P19) = P1 by A1, Def5;
A4: [#] (S | P2) = P2 by Def5;
A5: for R being Subset of ((S | P2) | P19) holds
( R in the topology of ((S | P2) | P19) iff ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) ) )
proof
let R be Subset of ((S | P2) | P19); ::_thesis: ( R in the topology of ((S | P2) | P19) iff ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) ) )
A6: now__::_thesis:_(_ex_Q_being_Subset_of_S_st_
(_Q_in_the_topology_of_S_&_R_=_Q_/\_([#]_((S_|_P2)_|_P19))_)_implies_R_in_the_topology_of_((S_|_P2)_|_P19)_)
given Q being Subset of S such that A7: Q in the topology of S and
A8: R = Q /\ ([#] ((S | P2) | P19)) ; ::_thesis: R in the topology of ((S | P2) | P19)
reconsider R9 = Q /\ ([#] (S | P2)) as Subset of (S | P2) ;
A9: R9 in the topology of (S | P2) by A7, Def4;
R9 /\ ([#] ((S | P2) | P19)) = Q /\ (P2 /\ P1) by A4, A3, XBOOLE_1:16
.= R by A2, A3, A8, XBOOLE_1:28 ;
hence R in the topology of ((S | P2) | P19) by A9, Def4; ::_thesis: verum
end;
now__::_thesis:_(_R_in_the_topology_of_((S_|_P2)_|_P19)_implies_ex_Q_being_Subset_of_S_st_
(_Q_in_the_topology_of_S_&_R_=_Q_/\_([#]_((S_|_P2)_|_P19))_)_)
assume R in the topology of ((S | P2) | P19) ; ::_thesis: ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) )
then consider Q0 being Subset of (S | P2) such that
A10: Q0 in the topology of (S | P2) and
A11: R = Q0 /\ ([#] ((S | P2) | P19)) by Def4;
consider Q1 being Subset of S such that
A12: Q1 in the topology of S and
A13: Q0 = Q1 /\ ([#] (S | P2)) by A10, Def4;
R = Q1 /\ (P2 /\ P1) by A4, A3, A11, A13, XBOOLE_1:16
.= Q1 /\ ([#] ((S | P2) | P19)) by A2, A3, XBOOLE_1:28 ;
hence ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) ) by A12; ::_thesis: verum
end;
hence ( R in the topology of ((S | P2) | P19) iff ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) ) ) by A6; ::_thesis: verum
end;
[#] ((S | P2) | P19) c= [#] S by A3;
then (S | P2) | P19 is SubSpace of S by A5, Def4;
hence S | P1 = (S | P2) | P19 by A3, Def5; ::_thesis: verum
end;
theorem Th8: :: PRE_TOPC:8
for GX being TopStruct
for A being Subset of GX holds the carrier of (GX | A) = A
proof
let GX be TopStruct ; ::_thesis: for A being Subset of GX holds the carrier of (GX | A) = A
let A be Subset of GX; ::_thesis: the carrier of (GX | A) = A
A = [#] (GX | A) by Def5;
hence the carrier of (GX | A) = A ; ::_thesis: verum
end;
theorem :: PRE_TOPC:9
for X being TopStruct
for Y being non empty TopStruct
for f being Function of X,Y
for P being Subset of X holds f | P is Function of (X | P),Y
proof
let X be TopStruct ; ::_thesis: for Y being non empty TopStruct
for f being Function of X,Y
for P being Subset of X holds f | P is Function of (X | P),Y
let Y be non empty TopStruct ; ::_thesis: for f being Function of X,Y
for P being Subset of X holds f | P is Function of (X | P),Y
let f be Function of X,Y; ::_thesis: for P being Subset of X holds f | P is Function of (X | P),Y
let P be Subset of X; ::_thesis: f | P is Function of (X | P),Y
P = the carrier of (X | P) by Th8;
hence f | P is Function of (X | P),Y by FUNCT_2:32; ::_thesis: verum
end;
definition
let S, T be TopStruct ;
let f be Function of S,T;
attrf is continuous means :Def6: :: PRE_TOPC:def 6
for P1 being Subset of T st P1 is closed holds
f " P1 is closed ;
end;
:: deftheorem Def6 defines continuous PRE_TOPC:def_6_:_
for S, T being TopStruct
for f being Function of S,T holds
( f is continuous iff for P1 being Subset of T st P1 is closed holds
f " P1 is closed );
theorem :: PRE_TOPC:10
for T1, T2, S1, S2 being TopStruct st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & S1 is SubSpace of T1 holds
S2 is SubSpace of T2
proof
let T1, T2, S1, S2 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & S1 is SubSpace of T1 implies S2 is SubSpace of T2 )
assume A1: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) ) ; ::_thesis: ( not S1 is SubSpace of T1 or S2 is SubSpace of T2 )
assume that
A2: [#] S1 c= [#] T1 and
A3: for P being Subset of S1 holds
( P in the topology of S1 iff ex Q being Subset of T1 st
( Q in the topology of T1 & P = Q /\ ([#] S1) ) ) ; :: according to PRE_TOPC:def_4 ::_thesis: S2 is SubSpace of T2
thus [#] S2 c= [#] T2 by A1, A2; :: according to PRE_TOPC:def_4 ::_thesis: for P being Subset of S2 holds
( P in the topology of S2 iff ex Q being Subset of T2 st
( Q in the topology of T2 & P = Q /\ ([#] S2) ) )
thus for P being Subset of S2 holds
( P in the topology of S2 iff ex Q being Subset of T2 st
( Q in the topology of T2 & P = Q /\ ([#] S2) ) ) by A1, A3; ::_thesis: verum
end;
theorem Th11: :: PRE_TOPC:11
for T being TopStruct
for X9 being SubSpace of T
for A being Subset of X9 holds A is Subset of T
proof
let T be TopStruct ; ::_thesis: for X9 being SubSpace of T
for A being Subset of X9 holds A is Subset of T
let X9 be SubSpace of T; ::_thesis: for A being Subset of X9 holds A is Subset of T
let A be Subset of X9; ::_thesis: A is Subset of T
[#] X9 c= [#] T by Def4;
hence A is Subset of T by XBOOLE_1:1; ::_thesis: verum
end;
theorem :: PRE_TOPC:12
for T being TopStruct
for A being Subset of T st A <> {} T holds
ex x being Point of T st x in A
proof
let T be TopStruct ; ::_thesis: for A being Subset of T st A <> {} T holds
ex x being Point of T st x in A
let A be Subset of T; ::_thesis: ( A <> {} T implies ex x being Point of T st x in A )
set x = the Element of A;
assume A1: A <> {} T ; ::_thesis: ex x being Point of T st x in A
then the Element of A is Point of T by TARSKI:def_3;
hence ex x being Point of T st x in A by A1; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster [#] T -> closed ;
coherence
[#] T is closed
proof
{} T in the topology of T by Th1;
then A1: {} T is open by Def2;
([#] T) \ ([#] T) = {} T by Th4;
hence [#] T is closed by A1, Def3; ::_thesis: verum
end;
end;
registration
let T be TopSpace;
cluster closed for Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is closed
proof
take [#] T ; ::_thesis: [#] T is closed
thus [#] T is closed ; ::_thesis: verum
end;
end;
registration
let T be non empty TopSpace;
cluster non empty closed for Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( not b1 is empty & b1 is closed )
proof
take [#] T ; ::_thesis: ( not [#] T is empty & [#] T is closed )
thus ( not [#] T is empty & [#] T is closed ) ; ::_thesis: verum
end;
end;
theorem Th13: :: PRE_TOPC:13
for T being TopStruct
for X9 being SubSpace of T
for B being Subset of X9 holds
( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
proof
let T be TopStruct ; ::_thesis: for X9 being SubSpace of T
for B being Subset of X9 holds
( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
let X9 be SubSpace of T; ::_thesis: for B being Subset of X9 holds
( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
let B be Subset of X9; ::_thesis: ( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
A1: [#] X9 is Subset of T by Th11;
A2: now__::_thesis:_(_B_is_closed_implies_ex_C_being_Subset_of_T_st_
(_C_is_closed_&_C_/\_([#]_X9)_=_B_)_)
assume B is closed ; ::_thesis: ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B )
then ([#] X9) \ B is open by Def3;
then ([#] X9) \ B in the topology of X9 by Def2;
then consider V being Subset of T such that
A3: V in the topology of T and
A4: ([#] X9) \ B = V /\ ([#] X9) by Def4;
A5: (([#] T) \ V) /\ ([#] X9) = ([#] X9) /\ (V `)
.= ([#] X9) \ V by A1, SUBSET_1:13
.= ([#] X9) \ (([#] X9) /\ V) by XBOOLE_1:47
.= B by A4, Th3 ;
reconsider V1 = V as Subset of T ;
A6: ([#] T) \ (([#] T) \ V) = V by Th3;
V1 is open by A3, Def2;
then ([#] T) \ V is closed by A6, Def3;
hence ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) by A5; ::_thesis: verum
end;
now__::_thesis:_(_ex_C_being_Subset_of_T_st_
(_C_is_closed_&_C_/\_([#]_X9)_=_B_)_implies_B_is_closed_)
given C being Subset of T such that A7: C is closed and
A8: C /\ ([#] X9) = B ; ::_thesis: B is closed
([#] T) \ C is open by A7, Def3;
then ([#] T) \ C in the topology of T by Def2;
then A9: (([#] T) \ C) /\ ([#] X9) in the topology of X9 by Def4;
([#] X9) \ B = ([#] X9) \ C by A8, XBOOLE_1:47
.= ([#] X9) /\ (C `) by A1, SUBSET_1:13
.= (([#] T) \ C) /\ ([#] X9) ;
then ([#] X9) \ B is open by A9, Def2;
hence B is closed by Def3; ::_thesis: verum
end;
hence ( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) ) by A2; ::_thesis: verum
end;
theorem Th14: :: PRE_TOPC:14
for GX being TopSpace
for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is closed ) holds
meet F is closed
proof
let GX be TopSpace; ::_thesis: for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is closed ) holds
meet F is closed
let F be Subset-Family of GX; ::_thesis: ( ( for A being Subset of GX st A in F holds
A is closed ) implies meet F is closed )
assume A1: for A being Subset of GX st A in F holds
A is closed ; ::_thesis: meet F is closed
percases ( F <> {} or F = {} ) ;
supposeA2: F <> {} ; ::_thesis: meet F is closed
defpred S1[ set ] means ([#] GX) \ $1 in F;
consider R1 being Subset-Family of GX such that
A3: for B being Subset of GX holds
( B in R1 iff S1[B] ) from SUBSET_1:sch_3();
A4: for x being set st x in the carrier of GX holds
( ( for A being Subset of GX st A in F holds
x in A ) iff for Z being Subset of GX st Z in R1 holds
not x in Z )
proof
let x be set ; ::_thesis: ( x in the carrier of GX implies ( ( for A being Subset of GX st A in F holds
x in A ) iff for Z being Subset of GX st Z in R1 holds
not x in Z ) )
assume A5: x in the carrier of GX ; ::_thesis: ( ( for A being Subset of GX st A in F holds
x in A ) iff for Z being Subset of GX st Z in R1 holds
not x in Z )
thus ( ( for A being Subset of GX st A in F holds
x in A ) implies for Z being Subset of GX st Z in R1 holds
not x in Z ) ::_thesis: ( ( for Z being Subset of GX st Z in R1 holds
not x in Z ) implies for A being Subset of GX st A in F holds
x in A )
proof
assume A6: for A being Subset of GX st A in F holds
x in A ; ::_thesis: for Z being Subset of GX st Z in R1 holds
not x in Z
let Z be Subset of GX; ::_thesis: ( Z in R1 implies not x in Z )
assume Z in R1 ; ::_thesis: not x in Z
then ([#] GX) \ Z in F by A3;
then x in ([#] GX) \ Z by A6;
hence not x in Z by XBOOLE_0:def_5; ::_thesis: verum
end;
assume A7: for Z being Subset of GX st Z in R1 holds
not x in Z ; ::_thesis: for A being Subset of GX st A in F holds
x in A
let A be Subset of GX; ::_thesis: ( A in F implies x in A )
assume A8: A in F ; ::_thesis: x in A
([#] GX) \ (([#] GX) \ A) = A by Th3;
then ([#] GX) \ A in R1 by A3, A8;
then not x in ([#] GX) \ A by A7;
hence x in A by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
A9: for x being set holds
( x in ([#] GX) \ (union R1) iff x in meet F )
proof
let x be set ; ::_thesis: ( x in ([#] GX) \ (union R1) iff x in meet F )
thus ( x in ([#] GX) \ (union R1) implies x in meet F ) ::_thesis: ( x in meet F implies x in ([#] GX) \ (union R1) )
proof
assume A10: x in ([#] GX) \ (union R1) ; ::_thesis: x in meet F
then not x in union R1 by XBOOLE_0:def_5;
then for Z being Subset of GX st Z in R1 holds
not x in Z by TARSKI:def_4;
then for A being set st A in F holds
x in A by A4, A10;
hence x in meet F by A2, SETFAM_1:def_1; ::_thesis: verum
end;
assume A11: x in meet F ; ::_thesis: x in ([#] GX) \ (union R1)
then for A being Subset of GX st A in F holds
x in A by SETFAM_1:def_1;
then for Z being set st x in Z holds
not Z in R1 by A4;
then not x in union R1 by TARSKI:def_4;
hence x in ([#] GX) \ (union R1) by A11, XBOOLE_0:def_5; ::_thesis: verum
end;
now__::_thesis:_for_B_being_set_st_B_in_R1_holds_
B_in_the_topology_of_GX
let B be set ; ::_thesis: ( B in R1 implies B in the topology of GX )
assume A12: B in R1 ; ::_thesis: B in the topology of GX
then reconsider B1 = B as Subset of GX ;
( B1 in R1 iff ([#] GX) \ B1 in F ) by A3;
then A13: ([#] GX) \ B1 is closed by A1, A12;
([#] GX) \ (([#] GX) \ B1) = B1 by Th3;
then B1 is open by A13, Def3;
hence B in the topology of GX by Def2; ::_thesis: verum
end;
then R1 c= the topology of GX by TARSKI:def_3;
then union R1 in the topology of GX by Def1;
then A14: union R1 is open by Def2;
([#] GX) \ (([#] GX) \ (union R1)) = union R1 by Th3;
then ([#] GX) \ (union R1) is closed by A14, Def3;
hence meet F is closed by A9, TARSKI:1; ::_thesis: verum
end;
supposeA15: F = {} ; ::_thesis: meet F is closed
the carrier of GX in the topology of GX by Def1;
then A16: [#] GX is open by Def2;
[#] GX = ([#] GX) \ ({} GX) ;
then {} GX is closed by A16, Def3;
hence meet F is closed by A15, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
definition
let GX be TopStruct ;
let A be Subset of GX;
func Cl A -> Subset of GX means :Def7: :: PRE_TOPC:def 7
for p being set st p in the carrier of GX holds
( p in it iff for G being Subset of GX st G is open & p in G holds
A meets G );
existence
ex b1 being Subset of GX st
for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
A meets G )
proof
defpred S1[ set ] means for G being Subset of GX st G is open & $1 in G holds
A meets G;
consider P being Subset of GX such that
A1: for x being set holds
( x in P iff ( x in the carrier of GX & S1[x] ) ) from SUBSET_1:sch_1();
take P ; ::_thesis: for p being set st p in the carrier of GX holds
( p in P iff for G being Subset of GX st G is open & p in G holds
A meets G )
thus for p being set st p in the carrier of GX holds
( p in P iff for G being Subset of GX st G is open & p in G holds
A meets G ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of GX st ( for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) & ( for p being set st p in the carrier of GX holds
( p in b2 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) holds
b1 = b2
proof
let C1, C2 be Subset of GX; ::_thesis: ( ( for p being set st p in the carrier of GX holds
( p in C1 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) & ( for p being set st p in the carrier of GX holds
( p in C2 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) implies C1 = C2 )
assume that
A2: for p being set st p in the carrier of GX holds
( p in C1 iff for G being Subset of GX st G is open & p in G holds
A meets G ) and
A3: for p being set st p in the carrier of GX holds
( p in C2 iff for V being Subset of GX st V is open & p in V holds
A meets V ) ; ::_thesis: C1 = C2
for x being set holds
( x in C1 iff x in C2 )
proof
let x be set ; ::_thesis: ( x in C1 iff x in C2 )
thus ( x in C1 implies x in C2 ) ::_thesis: ( x in C2 implies x in C1 )
proof
assume A4: x in C1 ; ::_thesis: x in C2
then for G being Subset of GX st G is open & x in G holds
A meets G by A2;
hence x in C2 by A3, A4; ::_thesis: verum
end;
assume A5: x in C2 ; ::_thesis: x in C1
then for V being Subset of GX st V is open & x in V holds
A meets V by A3;
hence x in C1 by A2, A5; ::_thesis: verum
end;
hence C1 = C2 by TARSKI:1; ::_thesis: verum
end;
projectivity
for b1, b2 being Subset of GX st ( for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
b2 meets G ) ) holds
for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
b1 meets G )
proof
let r, A be Subset of GX; ::_thesis: ( ( for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) implies for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G ) )
assume A6: for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
A meets G ) ; ::_thesis: for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G )
let p be set ; ::_thesis: ( p in the carrier of GX implies ( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G ) )
assume A7: p in the carrier of GX ; ::_thesis: ( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G )
thus ( p in r implies for G being Subset of GX st G is open & p in G holds
r meets G ) by XBOOLE_0:3; ::_thesis: ( ( for G being Subset of GX st G is open & p in G holds
r meets G ) implies p in r )
assume A8: for G being Subset of GX st G is open & p in G holds
r meets G ; ::_thesis: p in r
A9: now__::_thesis:_for_C_being_Subset_of_GX_st_C_is_closed_&_A_c=_C_holds_
p_in_C
let C be Subset of GX; ::_thesis: ( C is closed & A c= C implies p in C )
assume C is closed ; ::_thesis: ( A c= C implies p in C )
then A10: ([#] GX) \ C is open by Def3;
now__::_thesis:_(_p_in_([#]_GX)_\_C_implies_A_meets_([#]_GX)_\_C_)
assume p in ([#] GX) \ C ; ::_thesis: A meets ([#] GX) \ C
then r meets ([#] GX) \ C by A8, A10;
then ex x being set st
( x in r & x in ([#] GX) \ C ) by XBOOLE_0:3;
hence A meets ([#] GX) \ C by A6, A10; ::_thesis: verum
end;
then ( not A c= (([#] GX) \ C) ` or p in C or not p in [#] GX ) by SUBSET_1:23, XBOOLE_0:def_5;
hence ( A c= C implies p in C ) by A7, Th3; ::_thesis: verum
end;
for G being Subset of GX st G is open & p in G holds
A meets G
proof
let G be Subset of GX; ::_thesis: ( G is open & p in G implies A meets G )
assume A11: G is open ; ::_thesis: ( not p in G or A meets G )
([#] GX) \ (([#] GX) \ G) = G by Th3;
then ([#] GX) \ G is closed by A11, Def3;
then ( A c= G ` implies p in ([#] GX) \ G ) by A9;
hence ( not p in G or A meets G ) by SUBSET_1:23, XBOOLE_0:def_5; ::_thesis: verum
end;
hence p in r by A6, A7; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines Cl PRE_TOPC:def_7_:_
for GX being TopStruct
for A, b3 being Subset of GX holds
( b3 = Cl A iff for p being set st p in the carrier of GX holds
( p in b3 iff for G being Subset of GX st G is open & p in G holds
A meets G ) );
theorem Th15: :: PRE_TOPC:15
for T being TopStruct
for A being Subset of T
for p being set st p in the carrier of T holds
( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
proof
let T be TopStruct ; ::_thesis: for A being Subset of T
for p being set st p in the carrier of T holds
( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
let A be Subset of T; ::_thesis: for p being set st p in the carrier of T holds
( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
let p be set ; ::_thesis: ( p in the carrier of T implies ( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C ) )
assume A1: p in the carrier of T ; ::_thesis: ( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
A2: now__::_thesis:_(_(_for_C_being_Subset_of_T_st_C_is_closed_&_A_c=_C_holds_
p_in_C_)_implies_p_in_Cl_A_)
assume A3: for C being Subset of T st C is closed & A c= C holds
p in C ; ::_thesis: p in Cl A
for G being Subset of T st G is open & p in G holds
A meets G
proof
let G be Subset of T; ::_thesis: ( G is open & p in G implies A meets G )
assume A4: G is open ; ::_thesis: ( not p in G or A meets G )
([#] T) \ (([#] T) \ G) = G by Th3;
then ([#] T) \ G is closed by A4, Def3;
then ( A c= G ` implies p in ([#] T) \ G ) by A3;
hence ( not p in G or A meets G ) by SUBSET_1:23, XBOOLE_0:def_5; ::_thesis: verum
end;
hence p in Cl A by A1, Def7; ::_thesis: verum
end;
now__::_thesis:_(_p_in_Cl_A_implies_for_C_being_Subset_of_T_st_C_is_closed_&_A_c=_C_holds_
p_in_C_)
assume A5: p in Cl A ; ::_thesis: for C being Subset of T st C is closed & A c= C holds
p in C
let C be Subset of T; ::_thesis: ( C is closed & A c= C implies p in C )
assume C is closed ; ::_thesis: ( A c= C implies p in C )
then ([#] T) \ C is open by Def3;
then ( p in ([#] T) \ C implies A meets ([#] T) \ C ) by A5, Def7;
then ( not A c= (([#] T) \ C) ` or p in C or not p in [#] T ) by SUBSET_1:23, XBOOLE_0:def_5;
hence ( A c= C implies p in C ) by A1, Th3; ::_thesis: verum
end;
hence ( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C ) by A2; ::_thesis: verum
end;
theorem Th16: :: PRE_TOPC:16
for GX being TopSpace
for A being Subset of GX ex F being Subset-Family of GX st
( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
proof
let GX be TopSpace; ::_thesis: for A being Subset of GX ex F being Subset-Family of GX st
( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
let A be Subset of GX; ::_thesis: ex F being Subset-Family of GX st
( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
defpred S1[ set ] means ex C1 being Subset of GX st
( C1 = $1 & C1 is closed & A c= $1 );
consider F9 being Subset-Family of GX such that
A1: for C being Subset of GX holds
( C in F9 iff S1[C] ) from SUBSET_1:sch_3();
take F = F9; ::_thesis: ( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
thus for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ::_thesis: Cl A = meet F
proof
let C be Subset of GX; ::_thesis: ( C in F iff ( C is closed & A c= C ) )
thus ( C in F implies ( C is closed & A c= C ) ) ::_thesis: ( C is closed & A c= C implies C in F )
proof
assume C in F ; ::_thesis: ( C is closed & A c= C )
then ex C1 being Subset of GX st
( C1 = C & C1 is closed & A c= C ) by A1;
hence ( C is closed & A c= C ) ; ::_thesis: verum
end;
thus ( C is closed & A c= C implies C in F ) by A1; ::_thesis: verum
end;
A c= [#] GX ;
then A2: F <> {} by A1;
for p being set holds
( p in Cl A iff p in meet F )
proof
let p be set ; ::_thesis: ( p in Cl A iff p in meet F )
A3: now__::_thesis:_(_p_in_meet_F_implies_p_in_Cl_A_)
assume A4: p in meet F ; ::_thesis: p in Cl A
now__::_thesis:_for_C_being_Subset_of_GX_st_C_is_closed_&_A_c=_C_holds_
p_in_C
let C be Subset of GX; ::_thesis: ( C is closed & A c= C implies p in C )
assume ( C is closed & A c= C ) ; ::_thesis: p in C
then C in F by A1;
hence p in C by A4, SETFAM_1:def_1; ::_thesis: verum
end;
hence p in Cl A by A4, Th15; ::_thesis: verum
end;
now__::_thesis:_(_p_in_Cl_A_implies_p_in_meet_F_)
assume A5: p in Cl A ; ::_thesis: p in meet F
now__::_thesis:_for_C_being_set_st_C_in_F_holds_
p_in_C
let C be set ; ::_thesis: ( C in F implies p in C )
assume C in F ; ::_thesis: p in C
then ex C1 being Subset of GX st
( C1 = C & C1 is closed & A c= C ) by A1;
hence p in C by A5, Th15; ::_thesis: verum
end;
hence p in meet F by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence ( p in Cl A iff p in meet F ) by A3; ::_thesis: verum
end;
hence Cl A = meet F by TARSKI:1; ::_thesis: verum
end;
theorem :: PRE_TOPC:17
for T being TopStruct
for X9 being SubSpace of T
for A being Subset of T
for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
proof
let T be TopStruct ; ::_thesis: for X9 being SubSpace of T
for A being Subset of T
for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
let X9 be SubSpace of T; ::_thesis: for A being Subset of T
for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
let A be Subset of T; ::_thesis: for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
let A1 be Subset of X9; ::_thesis: ( A = A1 implies Cl A1 = (Cl A) /\ ([#] X9) )
assume A1: A = A1 ; ::_thesis: Cl A1 = (Cl A) /\ ([#] X9)
for p being set holds
( p in Cl A1 iff p in (Cl A) /\ ([#] X9) )
proof
let p be set ; ::_thesis: ( p in Cl A1 iff p in (Cl A) /\ ([#] X9) )
thus ( p in Cl A1 implies p in (Cl A) /\ ([#] X9) ) ::_thesis: ( p in (Cl A) /\ ([#] X9) implies p in Cl A1 )
proof
reconsider DD = Cl A1 as Subset of T by Th11;
assume A2: p in Cl A1 ; ::_thesis: p in (Cl A) /\ ([#] X9)
A3: for D1 being Subset of T st D1 is closed & A c= D1 holds
p in D1
proof
let D1 be Subset of T; ::_thesis: ( D1 is closed & A c= D1 implies p in D1 )
assume A4: D1 is closed ; ::_thesis: ( not A c= D1 or p in D1 )
set D3 = D1 /\ ([#] X9);
assume A c= D1 ; ::_thesis: p in D1
then A5: A1 c= D1 /\ ([#] X9) by A1, XBOOLE_1:19;
D1 /\ ([#] X9) is closed by A4, Th13;
then p in D1 /\ ([#] X9) by A2, A5, Th15;
hence p in D1 by XBOOLE_0:def_4; ::_thesis: verum
end;
p in DD by A2;
then p in Cl A by A3, Th15;
hence p in (Cl A) /\ ([#] X9) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A6: p in (Cl A) /\ ([#] X9) ; ::_thesis: p in Cl A1
then A7: p in Cl A by XBOOLE_0:def_4;
now__::_thesis:_for_D1_being_Subset_of_X9_st_D1_is_closed_&_A1_c=_D1_holds_
p_in_D1
let D1 be Subset of X9; ::_thesis: ( D1 is closed & A1 c= D1 implies p in D1 )
assume D1 is closed ; ::_thesis: ( A1 c= D1 implies p in D1 )
then consider D2 being Subset of T such that
A8: D2 is closed and
A9: D1 = D2 /\ ([#] X9) by Th13;
A10: D2 /\ ([#] X9) c= D2 by XBOOLE_1:17;
assume A1 c= D1 ; ::_thesis: p in D1
then A c= D2 by A1, A9, A10, XBOOLE_1:1;
then p in D2 by A7, A8, Th15;
hence p in D1 by A6, A9, XBOOLE_0:def_4; ::_thesis: verum
end;
hence p in Cl A1 by A6, Th15; ::_thesis: verum
end;
hence Cl A1 = (Cl A) /\ ([#] X9) by TARSKI:1; ::_thesis: verum
end;
theorem Th18: :: PRE_TOPC:18
for T being TopStruct
for A being Subset of T holds A c= Cl A
proof
let T be TopStruct ; ::_thesis: for A being Subset of T holds A c= Cl A
let A be Subset of T; ::_thesis: A c= Cl A
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_in_Cl_A
let x be set ; ::_thesis: ( x in A implies x in Cl A )
assume A1: x in A ; ::_thesis: x in Cl A
assume not x in Cl A ; ::_thesis: contradiction
then ex C being Subset of T st
( C is closed & A c= C & not x in C ) by A1, Th15;
hence contradiction by A1; ::_thesis: verum
end;
hence A c= Cl A by TARSKI:def_3; ::_thesis: verum
end;
theorem Th19: :: PRE_TOPC:19
for T being TopStruct
for A, B being Subset of T st A c= B holds
Cl A c= Cl B
proof
let T be TopStruct ; ::_thesis: for A, B being Subset of T st A c= B holds
Cl A c= Cl B
let A, B be Subset of T; ::_thesis: ( A c= B implies Cl A c= Cl B )
assume A1: A c= B ; ::_thesis: Cl A c= Cl B
now__::_thesis:_for_x_being_set_st_x_in_Cl_A_holds_
x_in_Cl_B
let x be set ; ::_thesis: ( x in Cl A implies x in Cl B )
assume A2: x in Cl A ; ::_thesis: x in Cl B
now__::_thesis:_for_D1_being_Subset_of_T_st_D1_is_closed_&_B_c=_D1_holds_
x_in_D1
let D1 be Subset of T; ::_thesis: ( D1 is closed & B c= D1 implies x in D1 )
assume A3: D1 is closed ; ::_thesis: ( B c= D1 implies x in D1 )
assume B c= D1 ; ::_thesis: x in D1
then A c= D1 by A1, XBOOLE_1:1;
hence x in D1 by A2, A3, Th15; ::_thesis: verum
end;
hence x in Cl B by A2, Th15; ::_thesis: verum
end;
hence Cl A c= Cl B by TARSKI:def_3; ::_thesis: verum
end;
theorem :: PRE_TOPC:20
for GX being TopSpace
for A, B being Subset of GX holds Cl (A \/ B) = (Cl A) \/ (Cl B)
proof
let GX be TopSpace; ::_thesis: for A, B being Subset of GX holds Cl (A \/ B) = (Cl A) \/ (Cl B)
let A, B be Subset of GX; ::_thesis: Cl (A \/ B) = (Cl A) \/ (Cl B)
now__::_thesis:_for_x_being_set_st_x_in_Cl_(A_\/_B)_holds_
x_in_(Cl_A)_\/_(Cl_B)
let x be set ; ::_thesis: ( x in Cl (A \/ B) implies x in (Cl A) \/ (Cl B) )
assume A1: x in Cl (A \/ B) ; ::_thesis: x in (Cl A) \/ (Cl B)
assume A2: not x in (Cl A) \/ (Cl B) ; ::_thesis: contradiction
then not x in Cl A by XBOOLE_0:def_3;
then consider G1 being Subset of GX such that
A3: G1 is open and
A4: x in G1 and
A5: A misses G1 by A1, Def7;
A6: A /\ G1 = {} by A5, XBOOLE_0:def_7;
not x in Cl B by A2, XBOOLE_0:def_3;
then consider G2 being Subset of GX such that
A7: G2 is open and
A8: x in G2 and
A9: B misses G2 by A1, Def7;
A10: G2 in the topology of GX by A7, Def2;
A11: B /\ G2 = {} by A9, XBOOLE_0:def_7;
(A \/ B) /\ (G1 /\ G2) = (A /\ (G1 /\ G2)) \/ (B /\ (G2 /\ G1)) by XBOOLE_1:23
.= ((A /\ G1) /\ G2) \/ (B /\ (G2 /\ G1)) by XBOOLE_1:16
.= {} \/ ({} /\ G1) by A6, A11, XBOOLE_1:16
.= {} GX ;
then A12: A \/ B misses G1 /\ G2 by XBOOLE_0:def_7;
G1 in the topology of GX by A3, Def2;
then G1 /\ G2 in the topology of GX by A10, Def1;
then A13: G1 /\ G2 is open by Def2;
x in G1 /\ G2 by A4, A8, XBOOLE_0:def_4;
hence contradiction by A1, A13, A12, Def7; ::_thesis: verum
end;
then A14: Cl (A \/ B) c= (Cl A) \/ (Cl B) by TARSKI:def_3;
( Cl A c= Cl (A \/ B) & Cl B c= Cl (A \/ B) ) by Th19, XBOOLE_1:7;
then (Cl A) \/ (Cl B) c= Cl (A \/ B) by XBOOLE_1:8;
hence Cl (A \/ B) = (Cl A) \/ (Cl B) by A14, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: PRE_TOPC:21
for T being TopStruct
for A, B being Subset of T holds Cl (A /\ B) c= (Cl A) /\ (Cl B)
proof
let T be TopStruct ; ::_thesis: for A, B being Subset of T holds Cl (A /\ B) c= (Cl A) /\ (Cl B)
let A, B be Subset of T; ::_thesis: Cl (A /\ B) c= (Cl A) /\ (Cl B)
( Cl (A /\ B) c= Cl A & Cl (A /\ B) c= Cl B ) by Th19, XBOOLE_1:17;
hence Cl (A /\ B) c= (Cl A) /\ (Cl B) by XBOOLE_1:19; ::_thesis: verum
end;
theorem Th22: :: PRE_TOPC:22
for T being TopStruct
for A being Subset of T holds
( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )
proof
let T be TopStruct ; ::_thesis: for A being Subset of T holds
( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )
let A be Subset of T; ::_thesis: ( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )
thus ( A is closed implies Cl A = A ) ::_thesis: ( T is TopSpace-like & Cl A = A implies A is closed )
proof
assume A is closed ; ::_thesis: Cl A = A
then for x being set st x in Cl A holds
x in A by Th15;
then A1: Cl A c= A by TARSKI:def_3;
A c= Cl A by Th18;
hence Cl A = A by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
assume A2: T is TopSpace-like ; ::_thesis: ( not Cl A = A or A is closed )
then consider F being Subset-Family of T such that
A3: for C being Subset of T holds
( C in F iff ( C is closed & A c= C ) ) and
A4: Cl A = meet F by Th16;
assume A5: Cl A = A ; ::_thesis: A is closed
for C being Subset of T st C in F holds
C is closed by A3;
hence A is closed by A2, A5, A4, Th14; ::_thesis: verum
end;
theorem :: PRE_TOPC:23
for T being TopStruct
for A being Subset of T holds
( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )
proof
let T be TopStruct ; ::_thesis: for A being Subset of T holds
( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )
let A be Subset of T; ::_thesis: ( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )
([#] T) \ (([#] T) \ A) = A by Th3;
then A1: ( A is open iff ([#] T) \ A is closed ) by Def3;
hence ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) by Th22; ::_thesis: ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open )
assume ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A ) ; ::_thesis: A is open
hence A is open by A1, Th22; ::_thesis: verum
end;
theorem :: PRE_TOPC:24
for T being TopStruct
for A being Subset of T
for p being Point of T holds
( p in Cl A iff ( not T is empty & ( for G being Subset of T st G is open & p in G holds
A meets G ) ) ) by Def7;
begin
theorem :: PRE_TOPC:25
for T being non empty TopStruct
for A being non empty SubSpace of T
for p being Point of A holds p is Point of T
proof
let T be non empty TopStruct ; ::_thesis: for A being non empty SubSpace of T
for p being Point of A holds p is Point of T
let A be non empty SubSpace of T; ::_thesis: for p being Point of A holds p is Point of T
[#] A c= [#] T by Def4;
hence for p being Point of A holds p is Point of T by TARSKI:def_3; ::_thesis: verum
end;
theorem :: PRE_TOPC:26
for A, B, C being TopSpace
for f being Function of A,C st f is continuous & C is SubSpace of B holds
for h being Function of A,B st h = f holds
h is continuous
proof
let A, B, C be TopSpace; ::_thesis: for f being Function of A,C st f is continuous & C is SubSpace of B holds
for h being Function of A,B st h = f holds
h is continuous
let f be Function of A,C; ::_thesis: ( f is continuous & C is SubSpace of B implies for h being Function of A,B st h = f holds
h is continuous )
assume that
A1: f is continuous and
A2: C is SubSpace of B ; ::_thesis: for h being Function of A,B st h = f holds
h is continuous
let h be Function of A,B; ::_thesis: ( h = f implies h is continuous )
assume A3: h = f ; ::_thesis: h is continuous
for P being Subset of B st P is closed holds
h " P is closed
proof
let P be Subset of B; ::_thesis: ( P is closed implies h " P is closed )
assume A4: P is closed ; ::_thesis: h " P is closed
A5: rng h c= the carrier of C by A3, RELAT_1:def_19;
A6: h " P = h " ((rng h) /\ P) by RELAT_1:133
.= h " (((rng h) /\ ([#] C)) /\ P) by A5, XBOOLE_1:28
.= h " ((rng h) /\ (([#] C) /\ P)) by XBOOLE_1:16
.= h " (P /\ ([#] C)) by RELAT_1:133 ;
reconsider C = C as SubSpace of B by A2;
reconsider Q = P /\ ([#] C) as Subset of C ;
Q is closed by A4, Th13;
hence h " P is closed by A1, A3, A6, Def6; ::_thesis: verum
end;
hence h is continuous by Def6; ::_thesis: verum
end;
theorem :: PRE_TOPC:27
for A being TopSpace
for B being non empty TopSpace
for f being Function of A,B
for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
proof
let A be TopSpace; ::_thesis: for B being non empty TopSpace
for f being Function of A,B
for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
let B be non empty TopSpace; ::_thesis: for f being Function of A,B
for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
let f be Function of A,B; ::_thesis: for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
let C be SubSpace of B; ::_thesis: ( f is continuous implies for h being Function of A,C st h = f holds
h is continuous )
assume A1: f is continuous ; ::_thesis: for h being Function of A,C st h = f holds
h is continuous
let h be Function of A,C; ::_thesis: ( h = f implies h is continuous )
assume A2: h = f ; ::_thesis: h is continuous
A3: rng f c= the carrier of C by A2, RELAT_1:def_19;
for P being Subset of C st P is closed holds
h " P is closed
proof
let P be Subset of C; ::_thesis: ( P is closed implies h " P is closed )
assume P is closed ; ::_thesis: h " P is closed
then consider Q being Subset of B such that
A4: Q is closed and
A5: Q /\ ([#] C) = P by Th13;
h " P = (f " Q) /\ (f " ([#] C)) by A2, A5, FUNCT_1:68
.= (f " Q) /\ (f " ((rng f) /\ ([#] C))) by RELAT_1:133
.= (f " Q) /\ (f " (rng f)) by A3, XBOOLE_1:28
.= (f " Q) /\ (dom f) by RELAT_1:134
.= f " Q by RELAT_1:132, XBOOLE_1:28 ;
hence h " P is closed by A1, A4, Def6; ::_thesis: verum
end;
hence h is continuous by Def6; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster empty -> closed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is empty holds
b1 is closed
proof
let S be Subset of T; ::_thesis: ( S is empty implies S is closed )
assume S is empty ; ::_thesis: S is closed
then A1: S = {} T ;
the carrier of T in the topology of T by Def1;
hence ([#] T) \ S is open by Def2, A1; :: according to PRE_TOPC:def_3 ::_thesis: verum
end;
end;
registration
let X be TopSpace;
let Y be non empty TopStruct ;
let y be Point of Y;
clusterX --> y -> continuous ;
coherence
X --> y is continuous
proof
let P1 be Subset of Y; :: according to PRE_TOPC:def_6 ::_thesis: ( P1 is closed implies (X --> y) " P1 is closed )
assume P1 is closed ; ::_thesis: (X --> y) " P1 is closed
set F = X --> y;
set H = [#] X;
percases ( y in P1 or not y in P1 ) ;
suppose y in P1 ; ::_thesis: (X --> y) " P1 is closed
then (X --> y) " P1 = [#] X by FUNCOP_1:14;
hence (X --> y) " P1 is closed ; ::_thesis: verum
end;
suppose not y in P1 ; ::_thesis: (X --> y) " P1 is closed
then (X --> y) " P1 = {} X by FUNCOP_1:16;
hence (X --> y) " P1 is closed ; ::_thesis: verum
end;
end;
end;
end;
registration
let S be TopSpace;
let T be non empty TopSpace;
clusterV7() V10( the carrier of S) V11( the carrier of T) V12() V21( the carrier of S, the carrier of T) continuous for Element of bool [: the carrier of S, the carrier of T:];
existence
ex b1 being Function of S,T st b1 is continuous
proof
set a = the Point of T;
S --> the Point of T is continuous ;
hence ex b1 being Function of S,T st b1 is continuous ; ::_thesis: verum
end;
end;
definition
let T be TopStruct ;
attrT is T_0 means :: PRE_TOPC:def 8
for x, y being Point of T st ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) holds
x = y;
attrT is T_1 means :Def9: :: PRE_TOPC:def 9
for p, q being Point of T st p <> q holds
ex G being Subset of T st
( G is open & p in G & q in G ` );
attrT is T_2 means :Def10: :: PRE_TOPC:def 10
for p, q being Point of T st p <> q holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 );
attrT is regular means :: PRE_TOPC:def 11
for p being Point of T
for F being Subset of T st F is closed & p in F ` holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 );
attrT is normal means :: PRE_TOPC:def 12
for F1, F2 being Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 );
end;
:: deftheorem defines T_0 PRE_TOPC:def_8_:_
for T being TopStruct holds
( T is T_0 iff for x, y being Point of T st ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) holds
x = y );
:: deftheorem Def9 defines T_1 PRE_TOPC:def_9_:_
for T being TopStruct holds
( T is T_1 iff for p, q being Point of T st p <> q holds
ex G being Subset of T st
( G is open & p in G & q in G ` ) );
:: deftheorem Def10 defines T_2 PRE_TOPC:def_10_:_
for T being TopStruct holds
( T is T_2 iff for p, q being Point of T st p <> q holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 ) );
:: deftheorem defines regular PRE_TOPC:def_11_:_
for T being TopStruct holds
( T is regular iff for p being Point of T
for F being Subset of T st F is closed & p in F ` holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 ) );
:: deftheorem defines normal PRE_TOPC:def_12_:_
for T being TopStruct holds
( T is normal iff for F1, F2 being Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 ) );
definition
let T be TopStruct ;
attrT is T_3 means :Def13: :: PRE_TOPC:def 13
( T is T_1 & T is regular );
attrT is T_4 means :Def14: :: PRE_TOPC:def 14
( T is T_1 & T is normal );
end;
:: deftheorem Def13 defines T_3 PRE_TOPC:def_13_:_
for T being TopStruct holds
( T is T_3 iff ( T is T_1 & T is regular ) );
:: deftheorem Def14 defines T_4 PRE_TOPC:def_14_:_
for T being TopStruct holds
( T is T_4 iff ( T is T_1 & T is normal ) );
registration
cluster T_3 -> T_1 regular for TopStruct ;
coherence
for b1 being TopStruct st b1 is T_3 holds
( b1 is T_1 & b1 is regular ) by Def13;
cluster T_1 regular -> T_3 for TopStruct ;
coherence
for b1 being TopStruct st b1 is T_1 & b1 is regular holds
b1 is T_3 by Def13;
cluster T_4 -> T_1 normal for TopStruct ;
coherence
for b1 being TopStruct st b1 is T_4 holds
( b1 is T_1 & b1 is normal ) by Def14;
cluster T_1 normal -> T_4 for TopStruct ;
coherence
for b1 being TopStruct st b1 is T_1 & b1 is normal holds
b1 is T_4 by Def14;
end;
registration
cluster non empty TopSpace-like T_1 for TopStruct ;
existence
ex b1 being non empty TopSpace st b1 is T_1
proof
set T = TopStruct(# 1,([#] (bool 1)) #);
A1: ( [#] the carrier of TopStruct(# 1,([#] (bool 1)) #) = the carrier of TopStruct(# 1,([#] (bool 1)) #) & ( for a being Subset-Family of TopStruct(# 1,([#] (bool 1)) #) st a c= the topology of TopStruct(# 1,([#] (bool 1)) #) holds
union a in the topology of TopStruct(# 1,([#] (bool 1)) #) ) ) ;
for a, b being Subset of TopStruct(# 1,([#] (bool 1)) #) st a in the topology of TopStruct(# 1,([#] (bool 1)) #) & b in the topology of TopStruct(# 1,([#] (bool 1)) #) holds
a /\ b in the topology of TopStruct(# 1,([#] (bool 1)) #) ;
then reconsider T = TopStruct(# 1,([#] (bool 1)) #) as non empty TopSpace by A1, Def1;
take T ; ::_thesis: T is T_1
let p, q be Point of T; :: according to PRE_TOPC:def_9 ::_thesis: ( p <> q implies ex G being Subset of T st
( G is open & p in G & q in G ` ) )
p = 0 by CARD_1:49, TARSKI:def_1;
hence ( p <> q implies ex G being Subset of T st
( G is open & p in G & q in G ` ) ) by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
end;
registration
cluster T_1 -> T_0 for TopStruct ;
coherence
for b1 being TopStruct st b1 is T_1 holds
b1 is T_0
proof
let T be TopStruct ; ::_thesis: ( T is T_1 implies T is T_0 )
assume A1: T is T_1 ; ::_thesis: T is T_0
let x be Point of T; :: according to PRE_TOPC:def_8 ::_thesis: for y being Point of T st ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) holds
x = y
let y be Point of T; ::_thesis: ( ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) implies x = y )
assume A2: for G being Subset of T st G is open holds
( x in G iff y in G ) ; ::_thesis: x = y
assume x <> y ; ::_thesis: contradiction
then consider G being Subset of T such that
A3: ( G is open & x in G ) and
A4: y in G ` by A1, Def9;
not y in G by A4, XBOOLE_0:def_5;
hence contradiction by A2, A3; ::_thesis: verum
end;
cluster T_2 -> T_1 for TopStruct ;
coherence
for b1 being TopStruct st b1 is T_2 holds
b1 is T_1
proof
let T be TopStruct ; ::_thesis: ( T is T_2 implies T is T_1 )
assume A5: T is T_2 ; ::_thesis: T is T_1
let p, q be Point of T; :: according to PRE_TOPC:def_9 ::_thesis: ( p <> q implies ex G being Subset of T st
( G is open & p in G & q in G ` ) )
assume p <> q ; ::_thesis: ex G being Subset of T st
( G is open & p in G & q in G ` )
then consider G1, G2 being Subset of T such that
A6: G1 is open and
G2 is open and
A7: p in G1 and
A8: q in G2 and
A9: G1 misses G2 by A5, Def10;
take G1 ; ::_thesis: ( G1 is open & p in G1 & q in G1 ` )
thus G1 is open by A6; ::_thesis: ( p in G1 & q in G1 ` )
thus p in G1 by A7; ::_thesis: q in G1 `
G2 c= G1 ` by A9, SUBSET_1:23;
hence q in G1 ` by A8; ::_thesis: verum
end;
end;
registration
let T be TopSpace;
cluster TopStruct(# the carrier of T, the topology of T #) -> TopSpace-like ;
coherence
TopStruct(# the carrier of T, the topology of T #) is TopSpace-like
proof
set S = TopStruct(# the carrier of T, the topology of T #);
thus ( the carrier of TopStruct(# the carrier of T, the topology of T #) in the topology of TopStruct(# the carrier of T, the topology of T #) & ( for a being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st a c= the topology of TopStruct(# the carrier of T, the topology of T #) holds
union a in the topology of TopStruct(# the carrier of T, the topology of T #) ) & ( for a, b being Subset of TopStruct(# the carrier of T, the topology of T #) st a in the topology of TopStruct(# the carrier of T, the topology of T #) & b in the topology of TopStruct(# the carrier of T, the topology of T #) holds
a /\ b in the topology of TopStruct(# the carrier of T, the topology of T #) ) ) by Def1; :: according to PRE_TOPC:def_1 ::_thesis: verum
end;
end;
registration
let T be non empty TopStruct ;
cluster TopStruct(# the carrier of T, the topology of T #) -> non empty ;
coherence
not TopStruct(# the carrier of T, the topology of T #) is empty ;
end;
theorem :: PRE_TOPC:28
for T being TopStruct st TopStruct(# the carrier of T, the topology of T #) is TopSpace-like holds
T is TopSpace-like
proof
let T be TopStruct ; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) is TopSpace-like implies T is TopSpace-like )
set S = TopStruct(# the carrier of T, the topology of T #);
assume ( the carrier of TopStruct(# the carrier of T, the topology of T #) in the topology of TopStruct(# the carrier of T, the topology of T #) & ( for a being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st a c= the topology of TopStruct(# the carrier of T, the topology of T #) holds
union a in the topology of TopStruct(# the carrier of T, the topology of T #) ) & ( for a, b being Subset of TopStruct(# the carrier of T, the topology of T #) st a in the topology of TopStruct(# the carrier of T, the topology of T #) & b in the topology of TopStruct(# the carrier of T, the topology of T #) holds
a /\ b in the topology of TopStruct(# the carrier of T, the topology of T #) ) ) ; :: according to PRE_TOPC:def_1 ::_thesis: T is TopSpace-like
hence ( the carrier of T in the topology of T & ( for a being Subset-Family of T st a c= the topology of T holds
union a in the topology of T ) & ( for a, b being Subset of T st a in the topology of T & b in the topology of T holds
a /\ b in the topology of T ) ) ; :: according to PRE_TOPC:def_1 ::_thesis: verum
end;
theorem :: PRE_TOPC:29
for T being TopStruct
for S being SubSpace of TopStruct(# the carrier of T, the topology of T #) holds S is SubSpace of T
proof
let T be TopStruct ; ::_thesis: for S being SubSpace of TopStruct(# the carrier of T, the topology of T #) holds S is SubSpace of T
let S be SubSpace of TopStruct(# the carrier of T, the topology of T #); ::_thesis: S is SubSpace of T
[#] S c= [#] TopStruct(# the carrier of T, the topology of T #) by Def4;
hence ( [#] S c= [#] T & ( for P being Subset of S holds
( P in the topology of S iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) ) ) ) by Def4; :: according to PRE_TOPC:def_4 ::_thesis: verum
end;
registration
let T be TopSpace;
cluster open for Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is open
proof
take {} T ; ::_thesis: {} T is open
thus {} T in the topology of T by Th1; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
end;
theorem :: PRE_TOPC:30
for T being TopSpace
for X being set holds
( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) )
proof
let T be TopSpace; ::_thesis: for X being set holds
( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) )
let X be set ; ::_thesis: ( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) )
( X in the topology of T iff X in the topology of TopStruct(# the carrier of T, the topology of T #) ) ;
hence ( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) ) by Def2; ::_thesis: verum
end;
theorem Th31: :: PRE_TOPC:31
for T being TopSpace
for X being set holds
( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) )
proof
let T be TopSpace; ::_thesis: for X being set holds
( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) )
let X be set ; ::_thesis: ( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) )
( ([#] T) \ X in the topology of T iff ([#] TopStruct(# the carrier of T, the topology of T #)) \ X in the topology of TopStruct(# the carrier of T, the topology of T #) ) ;
then ( ([#] T) \ X is open iff ([#] TopStruct(# the carrier of T, the topology of T #)) \ X is open ) by Def2;
hence ( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) ) by Def3; ::_thesis: verum
end;
theorem Th32: :: PRE_TOPC:32
for S, T being TopSpace
for f being Function of S,T
for g being Function of TopStruct(# the carrier of S, the topology of S #),T st f = g holds
( f is continuous iff g is continuous )
proof
let S, T be TopSpace; ::_thesis: for f being Function of S,T
for g being Function of TopStruct(# the carrier of S, the topology of S #),T st f = g holds
( f is continuous iff g is continuous )
let f be Function of S,T; ::_thesis: for g being Function of TopStruct(# the carrier of S, the topology of S #),T st f = g holds
( f is continuous iff g is continuous )
let g be Function of TopStruct(# the carrier of S, the topology of S #),T; ::_thesis: ( f = g implies ( f is continuous iff g is continuous ) )
assume A1: f = g ; ::_thesis: ( f is continuous iff g is continuous )
thus ( f is continuous implies g is continuous ) ::_thesis: ( g is continuous implies f is continuous )
proof
assume A2: f is continuous ; ::_thesis: g is continuous
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( P1 is closed implies g " P1 is closed )
assume P1 is closed ; ::_thesis: g " P1 is closed
then f " P1 is closed by A2, Def6;
hence g " P1 is closed by A1, Th31; ::_thesis: verum
end;
assume A3: g is continuous ; ::_thesis: f is continuous
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( P1 is closed implies f " P1 is closed )
assume P1 is closed ; ::_thesis: f " P1 is closed
then g " P1 is closed by A3, Def6;
hence f " P1 is closed by A1, Th31; ::_thesis: verum
end;
theorem Th33: :: PRE_TOPC:33
for S, T being TopSpace
for f being Function of S,T
for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
proof
let S, T be TopSpace; ::_thesis: for f being Function of S,T
for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
let f be Function of S,T; ::_thesis: for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
let g be Function of S,TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( f = g implies ( f is continuous iff g is continuous ) )
assume A1: f = g ; ::_thesis: ( f is continuous iff g is continuous )
thus ( f is continuous implies g is continuous ) ::_thesis: ( g is continuous implies f is continuous )
proof
assume A2: f is continuous ; ::_thesis: g is continuous
let P1 be Subset of TopStruct(# the carrier of T, the topology of T #); :: according to PRE_TOPC:def_6 ::_thesis: ( P1 is closed implies g " P1 is closed )
reconsider P = P1 as Subset of T ;
assume P1 is closed ; ::_thesis: g " P1 is closed
then P is closed by Th31;
hence g " P1 is closed by A1, A2, Def6; ::_thesis: verum
end;
assume A3: g is continuous ; ::_thesis: f is continuous
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( P1 is closed implies f " P1 is closed )
reconsider P = P1 as Subset of TopStruct(# the carrier of T, the topology of T #) ;
assume P1 is closed ; ::_thesis: f " P1 is closed
then P is closed by Th31;
hence f " P1 is closed by A1, A3, Def6; ::_thesis: verum
end;
theorem :: PRE_TOPC:34
for S, T being TopSpace
for f being Function of S,T
for g being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
proof
let S, T be TopSpace; ::_thesis: for f being Function of S,T
for g being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
let f be Function of S,T; ::_thesis: for g being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
let g be Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( f = g implies ( f is continuous iff g is continuous ) )
assume A1: f = g ; ::_thesis: ( f is continuous iff g is continuous )
reconsider h = f as Function of S,TopStruct(# the carrier of T, the topology of T #) ;
( h is continuous iff g is continuous ) by A1, Th32;
hence ( f is continuous iff g is continuous ) by Th33; ::_thesis: verum
end;
registration
let T be TopStruct ;
let P be empty Subset of T;
clusterT | P -> empty strict ;
coherence
T | P is empty by Th8;
end;
theorem Th35: :: PRE_TOPC:35
for S, T being TopStruct holds
( S is SubSpace of T iff S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )
proof
let S, T be TopStruct ; ::_thesis: ( S is SubSpace of T iff S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )
thus ( S is SubSpace of T implies S is SubSpace of TopStruct(# the carrier of T, the topology of T #) ) ::_thesis: ( S is SubSpace of TopStruct(# the carrier of T, the topology of T #) implies S is SubSpace of T )
proof
assume A1: S is SubSpace of T ; ::_thesis: S is SubSpace of TopStruct(# the carrier of T, the topology of T #)
then [#] S c= [#] T by Def4;
hence [#] S c= [#] TopStruct(# the carrier of T, the topology of T #) ; :: according to PRE_TOPC:def_4 ::_thesis: for P being Subset of S holds
( P in the topology of S iff ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) )
let P be Subset of S; ::_thesis: ( P in the topology of S iff ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) )
thus ( P in the topology of S implies ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) ) by A1, Def4; ::_thesis: ( ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) implies P in the topology of S )
given Q being Subset of TopStruct(# the carrier of T, the topology of T #) such that A2: ( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) ; ::_thesis: P in the topology of S
thus P in the topology of S by A1, A2, Def4; ::_thesis: verum
end;
assume A3: S is SubSpace of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: S is SubSpace of T
then [#] S c= [#] TopStruct(# the carrier of T, the topology of T #) by Def4;
hence [#] S c= [#] T ; :: according to PRE_TOPC:def_4 ::_thesis: for P being Subset of S holds
( P in the topology of S iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) )
let P be Subset of S; ::_thesis: ( P in the topology of S iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) )
thus ( P in the topology of S implies ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) ) by A3, Def4; ::_thesis: ( ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) implies P in the topology of S )
given Q being Subset of T such that A4: ( Q in the topology of T & P = Q /\ ([#] S) ) ; ::_thesis: P in the topology of S
thus P in the topology of S by A3, A4, Def4; ::_thesis: verum
end;
theorem :: PRE_TOPC:36
for T being TopStruct
for X being Subset of T
for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y
proof
let T be TopStruct ; ::_thesis: for X being Subset of T
for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y
let X be Subset of T; ::_thesis: for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y
let Y be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( X = Y implies TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y )
assume X = Y ; ::_thesis: TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y
then A1: [#] TopStruct(# the carrier of (T | X), the topology of (T | X) #) = Y by Def5;
TopStruct(# the carrier of (T | X), the topology of (T | X) #) is strict SubSpace of TopStruct(# the carrier of T, the topology of T #) by Th35;
hence TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y by A1, Def5; ::_thesis: verum
end;
registration
cluster empty strict for TopStruct ;
existence
ex b1 being TopStruct st
( b1 is strict & b1 is empty )
proof
set T = the TopStruct ;
take the TopStruct | ({} the TopStruct ) ; ::_thesis: ( the TopStruct | ({} the TopStruct ) is strict & the TopStruct | ({} the TopStruct ) is empty )
thus ( the TopStruct | ({} the TopStruct ) is strict & the TopStruct | ({} the TopStruct ) is empty ) ; ::_thesis: verum
end;
end;
registration
let A be non empty set ;
let t be Subset-Family of A;
cluster TopStruct(# A,t #) -> non empty ;
coherence
not TopStruct(# A,t #) is empty ;
end;
registration
cluster empty -> T_0 for TopStruct ;
coherence
for b1 being TopStruct st b1 is empty holds
b1 is T_0
proof
let T be TopStruct ; ::_thesis: ( T is empty implies T is T_0 )
assume A1: T is empty ; ::_thesis: T is T_0
let x, y be Point of T; :: according to PRE_TOPC:def_8 ::_thesis: ( ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) implies x = y )
assume for G being Subset of T st G is open holds
( x in G iff y in G ) ; ::_thesis: x = y
thus x = {} by A1, SUBSET_1:def_1
.= y by A1, SUBSET_1:def_1 ; ::_thesis: verum
end;
end;
registration
cluster empty strict TopSpace-like for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & b1 is empty )
proof
set T = the TopSpace;
take the TopSpace | ({} the TopSpace) ; ::_thesis: ( the TopSpace | ({} the TopSpace) is strict & the TopSpace | ({} the TopSpace) is empty )
thus ( the TopSpace | ({} the TopSpace) is strict & the TopSpace | ({} the TopSpace) is empty ) ; ::_thesis: verum
end;
end;