:: TSP_1 semantic presentation
begin
definition
let Y be TopStruct ;
redefine mode SubSpace of Y means :Def1: :: TSP_1:def 1
( the carrier of it c= the carrier of Y & ( for G0 being Subset of it holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of it ) ) ) );
compatibility
for b1 being TopStruct holds
( b1 is SubSpace of Y iff ( the carrier of b1 c= the carrier of Y & ( for G0 being Subset of b1 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of b1 ) ) ) ) )
proof
let Y0 be TopStruct ; ::_thesis: ( Y0 is SubSpace of Y iff ( the carrier of Y0 c= the carrier of Y & ( for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) ) ) )
A1: ( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ;
thus ( Y0 is SubSpace of Y implies ( the carrier of Y0 c= the carrier of Y & ( for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) ) ) ) ::_thesis: ( the carrier of Y0 c= the carrier of Y & ( for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) ) implies Y0 is SubSpace of Y )
proof
assume A2: Y0 is SubSpace of Y ; ::_thesis: ( the carrier of Y0 c= the carrier of Y & ( for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) ) )
hence the carrier of Y0 c= the carrier of Y by A1, PRE_TOPC:def_4; ::_thesis: for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) )
thus for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) ::_thesis: verum
proof
let G0 be Subset of Y0; ::_thesis: ( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) )
thus ( G0 is open implies ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) ::_thesis: ( ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) implies G0 is open )
proof
assume G0 is open ; ::_thesis: ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 )
then G0 in the topology of Y0 by PRE_TOPC:def_2;
then consider G being Subset of Y such that
A3: G in the topology of Y and
A4: G0 = G /\ ([#] Y0) by A2, PRE_TOPC:def_4;
reconsider G = G as Subset of Y ;
take G ; ::_thesis: ( G is open & G0 = G /\ the carrier of Y0 )
thus G is open by A3, PRE_TOPC:def_2; ::_thesis: G0 = G /\ the carrier of Y0
thus G0 = G /\ the carrier of Y0 by A4; ::_thesis: verum
end;
given G being Subset of Y such that A5: G is open and
A6: G0 = G /\ the carrier of Y0 ; ::_thesis: G0 is open
now__::_thesis:_ex_G_being_Subset_of_Y_st_
(_G_in_the_topology_of_Y_&_G0_=_G_/\_([#]_Y0)_)
take G = G; ::_thesis: ( G in the topology of Y & G0 = G /\ ([#] Y0) )
thus G in the topology of Y by A5, PRE_TOPC:def_2; ::_thesis: G0 = G /\ ([#] Y0)
thus G0 = G /\ ([#] Y0) by A6; ::_thesis: verum
end;
then G0 in the topology of Y0 by A2, PRE_TOPC:def_4;
hence G0 is open by PRE_TOPC:def_2; ::_thesis: verum
end;
end;
assume that
A7: the carrier of Y0 c= the carrier of Y and
A8: for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) ; ::_thesis: Y0 is SubSpace of Y
A9: for G0 being Subset of Y0 holds
( G0 in the topology of Y0 iff ex G being Subset of Y st
( G in the topology of Y & G0 = G /\ ([#] Y0) ) )
proof
let G0 be Subset of Y0; ::_thesis: ( G0 in the topology of Y0 iff ex G being Subset of Y st
( G in the topology of Y & G0 = G /\ ([#] Y0) ) )
reconsider M = G0 as Subset of Y0 ;
thus ( G0 in the topology of Y0 implies ex G being Subset of Y st
( G in the topology of Y & G0 = G /\ ([#] Y0) ) ) ::_thesis: ( ex G being Subset of Y st
( G in the topology of Y & G0 = G /\ ([#] Y0) ) implies G0 in the topology of Y0 )
proof
reconsider M = G0 as Subset of Y0 ;
assume G0 in the topology of Y0 ; ::_thesis: ex G being Subset of Y st
( G in the topology of Y & G0 = G /\ ([#] Y0) )
then M is open by PRE_TOPC:def_2;
then consider G being Subset of Y such that
A10: G is open and
A11: G0 = G /\ the carrier of Y0 by A8;
take G ; ::_thesis: ( G in the topology of Y & G0 = G /\ ([#] Y0) )
thus G in the topology of Y by A10, PRE_TOPC:def_2; ::_thesis: G0 = G /\ ([#] Y0)
thus G0 = G /\ ([#] Y0) by A11; ::_thesis: verum
end;
given G being Subset of Y such that A12: G in the topology of Y and
A13: G0 = G /\ ([#] Y0) ; ::_thesis: G0 in the topology of Y0
reconsider G = G as Subset of Y ;
now__::_thesis:_ex_G_being_Subset_of_Y_st_
(_G_is_open_&_G0_=_G_/\_the_carrier_of_Y0_)
take G = G; ::_thesis: ( G is open & G0 = G /\ the carrier of Y0 )
thus G is open by A12, PRE_TOPC:def_2; ::_thesis: G0 = G /\ the carrier of Y0
thus G0 = G /\ the carrier of Y0 by A13; ::_thesis: verum
end;
then M is open by A8;
hence G0 in the topology of Y0 by PRE_TOPC:def_2; ::_thesis: verum
end;
[#] Y0 c= [#] Y by A7;
hence Y0 is SubSpace of Y by A9, PRE_TOPC:def_4; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines SubSpace TSP_1:def_1_:_
for Y, b2 being TopStruct holds
( b2 is SubSpace of Y iff ( the carrier of b2 c= the carrier of Y & ( for G0 being Subset of b2 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of b2 ) ) ) ) );
theorem Th1: :: TSP_1:1
for Y being TopStruct
for Y0 being SubSpace of Y
for G being Subset of Y st G is open holds
ex G0 being Subset of Y0 st
( G0 is open & G0 = G /\ the carrier of Y0 )
proof
let Y be TopStruct ; ::_thesis: for Y0 being SubSpace of Y
for G being Subset of Y st G is open holds
ex G0 being Subset of Y0 st
( G0 is open & G0 = G /\ the carrier of Y0 )
let Y0 be SubSpace of Y; ::_thesis: for G being Subset of Y st G is open holds
ex G0 being Subset of Y0 st
( G0 is open & G0 = G /\ the carrier of Y0 )
let G be Subset of Y; ::_thesis: ( G is open implies ex G0 being Subset of Y0 st
( G0 is open & G0 = G /\ the carrier of Y0 ) )
assume A1: G is open ; ::_thesis: ex G0 being Subset of Y0 st
( G0 is open & G0 = G /\ the carrier of Y0 )
( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ;
then reconsider A = the carrier of Y0 as Subset of Y by PRE_TOPC:def_4;
reconsider G0 = G /\ A as Subset of Y0 by XBOOLE_1:17;
take G0 ; ::_thesis: ( G0 is open & G0 = G /\ the carrier of Y0 )
thus G0 is open by A1, Def1; ::_thesis: G0 = G /\ the carrier of Y0
thus G0 = G /\ the carrier of Y0 ; ::_thesis: verum
end;
definition
let Y be TopStruct ;
redefine mode SubSpace of Y means :Def2: :: TSP_1:def 2
( the carrier of it c= the carrier of Y & ( for F0 being Subset of it holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of it ) ) ) );
compatibility
for b1 being TopStruct holds
( b1 is SubSpace of Y iff ( the carrier of b1 c= the carrier of Y & ( for F0 being Subset of b1 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of b1 ) ) ) ) )
proof
let Y0 be TopStruct ; ::_thesis: ( Y0 is SubSpace of Y iff ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 ) ) ) ) )
A1: ( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ;
thus ( Y0 is SubSpace of Y implies ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 ) ) ) ) ) ::_thesis: ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 ) ) ) implies Y0 is SubSpace of Y )
proof
assume A2: Y0 is SubSpace of Y ; ::_thesis: ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 ) ) ) )
hence the carrier of Y0 c= the carrier of Y by A1, PRE_TOPC:def_4; ::_thesis: for F0 being Subset of Y0 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 ) )
[#] Y0 c= [#] Y by A2, PRE_TOPC:def_4;
then A3: ([#] Y0) \ ([#] Y) = {} by XBOOLE_1:37;
thus for F0 being Subset of Y0 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 ) ) ::_thesis: verum
proof
let F0 be Subset of Y0; ::_thesis: ( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 ) )
set G0 = ([#] Y0) \ F0;
thus ( F0 is closed implies ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 ) ) ::_thesis: ( ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 ) implies F0 is closed )
proof
assume F0 is closed ; ::_thesis: ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 )
then ([#] Y0) \ F0 is open by PRE_TOPC:def_3;
then consider G being Subset of Y such that
A4: G is open and
A5: ([#] Y0) \ F0 = G /\ the carrier of Y0 by A2, Def1;
take F = ([#] Y) \ G; ::_thesis: ( F is closed & F0 = F /\ the carrier of Y0 )
A6: G = ([#] Y) \ F by PRE_TOPC:3;
hence F is closed by A4, PRE_TOPC:def_3; ::_thesis: F0 = F /\ the carrier of Y0
F0 = ([#] Y0) \ (G /\ the carrier of Y0) by A5, PRE_TOPC:3
.= (([#] Y0) \ G) \/ (([#] Y0) \ the carrier of Y0) by XBOOLE_1:54
.= (([#] Y0) \ G) \/ {} by XBOOLE_1:37
.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ F) by A6, XBOOLE_1:52
.= ([#] Y0) /\ F by A3 ;
hence F0 = F /\ the carrier of Y0 ; ::_thesis: verum
end;
given F being Subset of Y such that A7: F is closed and
A8: F0 = F /\ the carrier of Y0 ; ::_thesis: F0 is closed
now__::_thesis:_ex_G_being_Element_of_K19(_the_carrier_of_Y)_st_
(_G_is_open_&_([#]_Y0)_\_F0_=_G_/\_the_carrier_of_Y0_)
take G = ([#] Y) \ F; ::_thesis: ( G is open & ([#] Y0) \ F0 = G /\ the carrier of Y0 )
A9: F = ([#] Y) \ G by PRE_TOPC:3;
thus G is open by A7, PRE_TOPC:def_3; ::_thesis: ([#] Y0) \ F0 = G /\ the carrier of Y0
([#] Y0) \ F0 = (([#] Y0) \ F) \/ (([#] Y0) \ the carrier of Y0) by A8, XBOOLE_1:54
.= (([#] Y0) \ F) \/ {} by XBOOLE_1:37
.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ G) by A9, XBOOLE_1:52
.= ([#] Y0) /\ G by A3 ;
hence ([#] Y0) \ F0 = G /\ the carrier of Y0 ; ::_thesis: verum
end;
then ([#] Y0) \ F0 is open by A2, Def1;
hence F0 is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
end;
assume that
A10: the carrier of Y0 c= the carrier of Y and
A11: for F0 being Subset of Y0 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of Y0 ) ) ; ::_thesis: Y0 is SubSpace of Y
A12: ([#] Y0) \ ([#] Y) = {} by A10, XBOOLE_1:37;
for G0 being Subset of Y0 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) )
proof
let G0 be Subset of Y0; ::_thesis: ( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) )
set F0 = ([#] Y0) \ G0;
thus ( G0 is open implies ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) ) ::_thesis: ( ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 ) implies G0 is open )
proof
set F0 = ([#] Y0) \ G0;
A13: G0 = ([#] Y0) \ (([#] Y0) \ G0) by PRE_TOPC:3;
assume G0 is open ; ::_thesis: ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of Y0 )
then ([#] Y0) \ G0 is closed by A13, PRE_TOPC:def_3;
then consider F being Subset of Y such that
A14: F is closed and
A15: ([#] Y0) \ G0 = F /\ the carrier of Y0 by A11;
take G = ([#] Y) \ F; ::_thesis: ( G is open & G0 = G /\ the carrier of Y0 )
thus G is open by A14, PRE_TOPC:def_3; ::_thesis: G0 = G /\ the carrier of Y0
A16: F = ([#] Y) \ G by PRE_TOPC:3;
G0 = (([#] Y0) \ F) \/ (([#] Y0) \ the carrier of Y0) by A13, A15, XBOOLE_1:54
.= (([#] Y0) \ F) \/ {} by XBOOLE_1:37
.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ G) by A16, XBOOLE_1:52
.= ([#] Y0) /\ G by A12 ;
hence G0 = G /\ the carrier of Y0 ; ::_thesis: verum
end;
given G being Subset of Y such that A17: G is open and
A18: G0 = G /\ the carrier of Y0 ; ::_thesis: G0 is open
now__::_thesis:_ex_F_being_Element_of_K19(_the_carrier_of_Y)_st_
(_F_is_closed_&_([#]_Y0)_\_G0_=_F_/\_the_carrier_of_Y0_)
take F = ([#] Y) \ G; ::_thesis: ( F is closed & ([#] Y0) \ G0 = F /\ the carrier of Y0 )
A19: G = ([#] Y) \ F by PRE_TOPC:3;
hence F is closed by A17, PRE_TOPC:def_3; ::_thesis: ([#] Y0) \ G0 = F /\ the carrier of Y0
([#] Y0) \ G0 = (([#] Y0) \ G) \/ (([#] Y0) \ the carrier of Y0) by A18, XBOOLE_1:54
.= (([#] Y0) \ G) \/ {} by XBOOLE_1:37
.= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ F) by A19, XBOOLE_1:52
.= ([#] Y0) /\ F by A12 ;
hence ([#] Y0) \ G0 = F /\ the carrier of Y0 ; ::_thesis: verum
end;
then ( G0 = ([#] Y0) \ (([#] Y0) \ G0) & ([#] Y0) \ G0 is closed ) by A11, PRE_TOPC:3;
hence G0 is open by PRE_TOPC:def_3; ::_thesis: verum
end;
hence Y0 is SubSpace of Y by A10, Def1; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines SubSpace TSP_1:def_2_:_
for Y, b2 being TopStruct holds
( b2 is SubSpace of Y iff ( the carrier of b2 c= the carrier of Y & ( for F0 being Subset of b2 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of b2 ) ) ) ) );
theorem Th2: :: TSP_1:2
for Y being TopStruct
for Y0 being SubSpace of Y
for F being Subset of Y st F is closed holds
ex F0 being Subset of Y0 st
( F0 is closed & F0 = F /\ the carrier of Y0 )
proof
let Y be TopStruct ; ::_thesis: for Y0 being SubSpace of Y
for F being Subset of Y st F is closed holds
ex F0 being Subset of Y0 st
( F0 is closed & F0 = F /\ the carrier of Y0 )
let Y0 be SubSpace of Y; ::_thesis: for F being Subset of Y st F is closed holds
ex F0 being Subset of Y0 st
( F0 is closed & F0 = F /\ the carrier of Y0 )
let F be Subset of Y; ::_thesis: ( F is closed implies ex F0 being Subset of Y0 st
( F0 is closed & F0 = F /\ the carrier of Y0 ) )
assume A1: F is closed ; ::_thesis: ex F0 being Subset of Y0 st
( F0 is closed & F0 = F /\ the carrier of Y0 )
( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ;
then reconsider A = the carrier of Y0 as Subset of Y by PRE_TOPC:def_4;
reconsider F0 = F /\ A as Subset of Y0 by XBOOLE_1:17;
take F0 ; ::_thesis: ( F0 is closed & F0 = F /\ the carrier of Y0 )
thus F0 is closed by A1, Def2; ::_thesis: F0 = F /\ the carrier of Y0
thus F0 = F /\ the carrier of Y0 ; ::_thesis: verum
end;
begin
definition
let T be TopStruct ;
redefine attr T is T_0 means :Def3: :: TSP_1:def 3
( T is empty or for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) );
compatibility
( T is T_0 iff ( T is empty or for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) ) )
proof
hereby ::_thesis: ( ( T is empty or for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) ) implies T is T_0 )
assume A1: T is T_0 ; ::_thesis: ( not T is empty implies for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) )
assume A2: not T is empty ; ::_thesis: for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) )
let x, y be Point of T; ::_thesis: ( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) )
assume x <> y ; ::_thesis: ( ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) )
then ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) by A1, A2, T_0TOPSP:def_7;
hence ( ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
assume A3: ( T is empty or for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) ) ; ::_thesis: T is T_0
assume A4: not T is empty ; :: according to T_0TOPSP:def_7 ::_thesis: for b1, b2 being Element of the carrier of T holds
( b1 = b2 or ex b3 being Element of K19( the carrier of T) st
( b3 is open & ( ( b1 in b3 & not b2 in b3 ) or ( b2 in b3 & not b1 in b3 ) ) ) )
let x, y be Point of T; ::_thesis: ( x = y or ex b1 being Element of K19( the carrier of T) st
( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) ) )
assume x <> y ; ::_thesis: ex b1 being Element of K19( the carrier of T) st
( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) )
then ( ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) by A3, A4;
hence ex b1 being Element of K19( the carrier of T) st
( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines T_0 TSP_1:def_3_:_
for T being TopStruct holds
( T is T_0 iff ( T is empty or for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) ) );
definition
let Y be TopStruct ;
redefine attr Y is T_0 means :Def4: :: TSP_1:def 4
( Y is empty or for x, y being Point of Y holds
( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) );
compatibility
( Y is T_0 iff ( Y is empty or for x, y being Point of Y holds
( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ) )
proof
thus ( not Y is T_0 or Y is empty or for x, y being Point of Y holds
( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ) ::_thesis: ( ( Y is empty or for x, y being Point of Y holds
( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ) implies Y is T_0 )
proof
assume A1: ( Y is empty or for x, y being Point of Y holds
( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ) ; :: according to TSP_1:def_3 ::_thesis: ( Y is empty or for x, y being Point of Y holds
( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) )
assume A2: not Y is empty ; ::_thesis: for x, y being Point of Y holds
( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
let x, y be Point of Y; ::_thesis: ( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
assume A3: x <> y ; ::_thesis: ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
hereby ::_thesis: verum
percases ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A1, A2, A3;
suppose ex V being Subset of Y st
( V is open & x in V & not y in V ) ; ::_thesis: ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
then consider V being Subset of Y such that
A4: V is open and
A5: x in V and
A6: not y in V ;
now__::_thesis:_ex_F_being_Element_of_K19(_the_carrier_of_Y)_st_
(_F_is_closed_&_not_x_in_F_&_y_in_F_)
take F = V ` ; ::_thesis: ( F is closed & not x in F & y in F )
V = ([#] Y) \ F by PRE_TOPC:3;
hence F is closed by A4, PRE_TOPC:def_3; ::_thesis: ( not x in F & y in F )
thus not x in F by A5, XBOOLE_0:def_5; ::_thesis: y in F
thus y in F by A2, A6, SUBSET_1:29; ::_thesis: verum
end;
hence ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ; ::_thesis: verum
end;
suppose ex W being Subset of Y st
( W is open & not x in W & y in W ) ; ::_thesis: ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
then consider W being Subset of Y such that
A7: W is open and
A8: not x in W and
A9: y in W ;
now__::_thesis:_ex_E_being_Element_of_K19(_the_carrier_of_Y)_st_
(_E_is_closed_&_x_in_E_&_not_y_in_E_)
take E = W ` ; ::_thesis: ( E is closed & x in E & not y in E )
W = ([#] Y) \ E by PRE_TOPC:3;
hence E is closed by A7, PRE_TOPC:def_3; ::_thesis: ( x in E & not y in E )
thus x in E by A2, A8, SUBSET_1:29; ::_thesis: not y in E
thus not y in E by A9, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ; ::_thesis: verum
end;
end;
end;
end;
assume A10: ( Y is empty or for x, y being Point of Y holds
( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ) ; ::_thesis: Y is T_0
( not Y is empty implies for x, y being Point of Y holds
( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) )
proof
assume A11: not Y is empty ; ::_thesis: for x, y being Point of Y holds
( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
let x, y be Point of Y; ::_thesis: ( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
assume A12: x <> y ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
hereby ::_thesis: verum
percases ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) by A10, A11, A12;
suppose ex E being Subset of Y st
( E is closed & x in E & not y in E ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
then consider E being Subset of Y such that
A13: E is closed and
A14: x in E and
A15: not y in E ;
now__::_thesis:_ex_W_being_Element_of_K19(_the_carrier_of_Y)_st_
(_W_is_open_&_not_x_in_W_&_y_in_W_)
take W = E ` ; ::_thesis: ( W is open & not x in W & y in W )
W = ([#] Y) \ E ;
hence W is open by A13, PRE_TOPC:def_3; ::_thesis: ( not x in W & y in W )
thus not x in W by A14, XBOOLE_0:def_5; ::_thesis: y in W
thus y in W by A11, A15, SUBSET_1:29; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
suppose ex F being Subset of Y st
( F is closed & not x in F & y in F ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
then consider F being Subset of Y such that
A16: F is closed and
A17: not x in F and
A18: y in F ;
now__::_thesis:_ex_V_being_Element_of_K19(_the_carrier_of_Y)_st_
(_V_is_open_&_x_in_V_&_not_y_in_V_)
take V = F ` ; ::_thesis: ( V is open & x in V & not y in V )
V = ([#] Y) \ F ;
hence V is open by A16, PRE_TOPC:def_3; ::_thesis: ( x in V & not y in V )
thus x in V by A11, A17, SUBSET_1:29; ::_thesis: not y in V
thus not y in V by A18, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
end;
end;
end;
hence Y is T_0 by Def3; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines T_0 TSP_1:def_4_:_
for Y being TopStruct holds
( Y is T_0 iff ( Y is empty or for x, y being Point of Y holds
( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ) );
registration
cluster non empty trivial -> non empty T_0 for TopStruct ;
coherence
for b1 being non empty TopStruct st b1 is trivial holds
b1 is T_0
proof
let Y be non empty TopStruct ; ::_thesis: ( Y is trivial implies Y is T_0 )
assume Y is trivial ; ::_thesis: Y is T_0
then consider a being Point of Y such that
A1: the carrier of Y = {a} by TEX_1:def_1;
now__::_thesis:_for_x,_y_being_Point_of_Y_holds_
(_not_x_<>_y_or_ex_V_being_Subset_of_Y_st_
(_V_is_open_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_
(_W_is_open_&_not_x_in_W_&_y_in_W_)_)
let x, y be Point of Y; ::_thesis: ( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
assume A2: x <> y ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
x = a by A1, TARSKI:def_1;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A1, A2, TARSKI:def_1; ::_thesis: verum
end;
hence Y is T_0 by Def3; ::_thesis: verum
end;
end;
Lm1: for X being non trivial anti-discrete TopStruct holds not X is T_0
proof
let X be non trivial anti-discrete TopStruct ; ::_thesis: not X is T_0
now__::_thesis:_ex_x,_y_being_Point_of_X_st_
(_x_<>_y_&_(_for_V_being_Subset_of_X_holds_
(_not_V_is_open_or_not_x_in_V_or_y_in_V_)_)_&_(_for_W_being_Subset_of_X_holds_
(_not_W_is_open_or_x_in_W_or_not_y_in_W_)_)_)
consider x, y being Point of X such that
A1: x <> y by STRUCT_0:def_10;
take x = x; ::_thesis: ex y being Point of X st
( x <> y & ( for V being Subset of X holds
( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds
( not W is open or x in W or not y in W ) ) )
take y = y; ::_thesis: ( x <> y & ( for V being Subset of X holds
( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds
( not W is open or x in W or not y in W ) ) )
thus x <> y by A1; ::_thesis: ( ( for V being Subset of X holds
( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds
( not W is open or x in W or not y in W ) ) )
A2: now__::_thesis:_for_V_being_Subset_of_X_st_V_is_open_&_y_in_V_holds_
x_in_V
let V be Subset of X; ::_thesis: ( V is open & y in V implies x in V )
assume V is open ; ::_thesis: ( y in V implies x in V )
then A3: ( V = {} or V = the carrier of X ) by TDLAT_3:18;
assume y in V ; ::_thesis: x in V
hence x in V by A3; ::_thesis: verum
end;
now__::_thesis:_for_V_being_Subset_of_X_st_V_is_open_&_x_in_V_holds_
y_in_V
let V be Subset of X; ::_thesis: ( V is open & x in V implies y in V )
assume V is open ; ::_thesis: ( x in V implies y in V )
then A4: ( V = {} or V = the carrier of X ) by TDLAT_3:18;
assume x in V ; ::_thesis: y in V
hence y in V by A4; ::_thesis: verum
end;
hence ( ( for V being Subset of X holds
( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds
( not W is open or x in W or not y in W ) ) ) by A2; ::_thesis: verum
end;
hence not X is T_0 by Def3; ::_thesis: verum
end;
registration
cluster non empty strict TopSpace-like T_0 for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & b1 is T_0 & not b1 is empty )
proof
set X = the non empty trivial strict TopSpace;
take the non empty trivial strict TopSpace ; ::_thesis: ( the non empty trivial strict TopSpace is strict & the non empty trivial strict TopSpace is T_0 & not the non empty trivial strict TopSpace is empty )
thus ( the non empty trivial strict TopSpace is strict & the non empty trivial strict TopSpace is T_0 & not the non empty trivial strict TopSpace is empty ) ; ::_thesis: verum
end;
cluster non empty strict TopSpace-like non T_0 for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & not b1 is T_0 & not b1 is empty )
proof
set X = the non empty non trivial strict anti-discrete TopSpace;
take the non empty non trivial strict anti-discrete TopSpace ; ::_thesis: ( the non empty non trivial strict anti-discrete TopSpace is strict & not the non empty non trivial strict anti-discrete TopSpace is T_0 & not the non empty non trivial strict anti-discrete TopSpace is empty )
thus ( the non empty non trivial strict anti-discrete TopSpace is strict & not the non empty non trivial strict anti-discrete TopSpace is T_0 & not the non empty non trivial strict anti-discrete TopSpace is empty ) by Lm1; ::_thesis: verum
end;
end;
registration
cluster non empty TopSpace-like discrete -> non empty T_0 for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is discrete holds
b1 is T_0
proof
let Y be non empty TopSpace; ::_thesis: ( Y is discrete implies Y is T_0 )
assume A1: Y is discrete ; ::_thesis: Y is T_0
now__::_thesis:_for_x,_y_being_Point_of_Y_holds_
(_not_x_<>_y_or_ex_V_being_Subset_of_Y_st_
(_V_is_open_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_
(_W_is_open_&_not_x_in_W_&_y_in_W_)_)
let x, y be Point of Y; ::_thesis: ( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
assume A2: x <> y ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
now__::_thesis:_ex_V_being_Element_of_K19(_the_carrier_of_Y)_st_
(_V_is_open_&_x_in_V_&_not_y_in_V_)
take V = {x}; ::_thesis: ( V is open & x in V & not y in V )
thus V is open by A1, TDLAT_3:15; ::_thesis: ( x in V & not y in V )
thus x in V by TARSKI:def_1; ::_thesis: not y in V
thus not y in V by A2, TARSKI:def_1; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
hence Y is T_0 by Def3; ::_thesis: verum
end;
cluster non empty TopSpace-like non T_0 -> non empty non discrete for TopStruct ;
coherence
for b1 being non empty TopSpace st not b1 is T_0 holds
not b1 is discrete ;
cluster non empty non trivial TopSpace-like anti-discrete -> non empty non T_0 for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is anti-discrete & not b1 is trivial holds
not b1 is T_0 by Lm1;
cluster non empty TopSpace-like T_0 anti-discrete -> non empty trivial for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is anti-discrete & b1 is T_0 holds
b1 is trivial ;
cluster non empty non trivial TopSpace-like T_0 -> non empty non anti-discrete for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is T_0 & not b1 is trivial holds
not b1 is anti-discrete ;
end;
Lm2: for X being non empty TopSpace
for x being Point of X holds x in Cl {x}
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X holds x in Cl {x}
let x be Point of X; ::_thesis: x in Cl {x}
( x in {x} & {x} c= Cl {x} ) by PRE_TOPC:18, TARSKI:def_1;
hence x in Cl {x} ; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
redefine attr X is T_0 means :Def5: :: TSP_1:def 5
for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y};
compatibility
( X is T_0 iff for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y} )
proof
thus ( X is T_0 implies for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y} ) ::_thesis: ( ( for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y} ) implies X is T_0 )
proof
assume A1: X is T_0 ; ::_thesis: for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y}
hereby ::_thesis: verum
let x, y be Point of X; ::_thesis: ( x <> y implies Cl {x} <> Cl {y} )
assume A2: x <> y ; ::_thesis: Cl {x} <> Cl {y}
now__::_thesis:_not_Cl_{x}_=_Cl_{y}
percases ( ex V being Subset of X st
( V is open & x in V & not y in V ) or ex W being Subset of X st
( W is open & not x in W & y in W ) ) by A1, A2, Def3;
suppose ex V being Subset of X st
( V is open & x in V & not y in V ) ; ::_thesis: not Cl {x} = Cl {y}
then consider V being Subset of X such that
A3: V is open and
A4: x in V and
A5: not y in V ;
( x in {x} & {x} c= Cl {x} ) by PRE_TOPC:18, TARSKI:def_1;
then A6: (Cl {x}) /\ V <> {} by A4, XBOOLE_0:def_4;
y in V ` by A5, SUBSET_1:29;
then {y} c= V ` by ZFMISC_1:31;
then {y} misses V by SUBSET_1:23;
then A7: Cl {y} misses V by A3, TSEP_1:36;
assume Cl {x} = Cl {y} ; ::_thesis: contradiction
hence contradiction by A7, A6, XBOOLE_0:def_7; ::_thesis: verum
end;
suppose ex W being Subset of X st
( W is open & not x in W & y in W ) ; ::_thesis: not Cl {x} = Cl {y}
then consider W being Subset of X such that
A8: W is open and
A9: not x in W and
A10: y in W ;
( y in {y} & {y} c= Cl {y} ) by PRE_TOPC:18, TARSKI:def_1;
then A11: (Cl {y}) /\ W <> {} by A10, XBOOLE_0:def_4;
x in W ` by A9, SUBSET_1:29;
then {x} c= W ` by ZFMISC_1:31;
then {x} misses W by SUBSET_1:23;
then A12: Cl {x} misses W by A8, TSEP_1:36;
assume Cl {x} = Cl {y} ; ::_thesis: contradiction
hence contradiction by A12, A11, XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence Cl {x} <> Cl {y} ; ::_thesis: verum
end;
end;
assume A13: for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y} ; ::_thesis: X is T_0
now__::_thesis:_for_x,_y_being_Point_of_X_st_x_<>_y_&_(_for_E_being_Subset_of_X_st_E_is_closed_&_x_in_E_holds_
y_in_E_)_holds_
ex_F_being_Subset_of_X_st_
(_F_is_closed_&_not_x_in_F_&_y_in_F_)
let x, y be Point of X; ::_thesis: ( x <> y & ( for E being Subset of X st E is closed & x in E holds
y in E ) implies ex F being Subset of X st
( F is closed & not x in F & y in F ) )
assume A14: x <> y ; ::_thesis: ( ( for E being Subset of X st E is closed & x in E holds
y in E ) implies ex F being Subset of X st
( F is closed & not x in F & y in F ) )
assume A15: for E being Subset of X st E is closed & x in E holds
y in E ; ::_thesis: ex F being Subset of X st
( F is closed & not x in F & y in F )
thus ex F being Subset of X st
( F is closed & not x in F & y in F ) ::_thesis: verum
proof
set F = Cl {y};
take Cl {y} ; ::_thesis: ( Cl {y} is closed & not x in Cl {y} & y in Cl {y} )
thus Cl {y} is closed ; ::_thesis: ( not x in Cl {y} & y in Cl {y} )
now__::_thesis:_not_x_in_Cl_{y}
assume x in Cl {y} ; ::_thesis: contradiction
then {x} c= Cl {y} by ZFMISC_1:31;
then A16: Cl {x} c= Cl {y} by TOPS_1:5;
y in Cl {x} by A15, Lm2;
then {y} c= Cl {x} by ZFMISC_1:31;
then Cl {y} c= Cl {x} by TOPS_1:5;
then Cl {x} = Cl {y} by A16, XBOOLE_0:def_10;
hence contradiction by A13, A14; ::_thesis: verum
end;
hence not x in Cl {y} ; ::_thesis: y in Cl {y}
thus y in Cl {y} by Lm2; ::_thesis: verum
end;
end;
hence X is T_0 by Def4; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines T_0 TSP_1:def_5_:_
for X being non empty TopSpace holds
( X is T_0 iff for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y} );
definition
let X be non empty TopSpace;
redefine attr X is T_0 means :Def6: :: TSP_1:def 6
for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} );
compatibility
( X is T_0 iff for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} ) )
proof
thus ( X is T_0 implies for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) ::_thesis: ( ( for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) implies X is T_0 )
proof
assume A1: X is T_0 ; ::_thesis: for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} )
hereby ::_thesis: verum
let x, y be Point of X; ::_thesis: ( x <> y & x in Cl {y} implies not y in Cl {x} )
assume A2: x <> y ; ::_thesis: ( x in Cl {y} implies not y in Cl {x} )
assume that
A3: x in Cl {y} and
A4: y in Cl {x} ; ::_thesis: contradiction
{y} c= Cl {x} by A4, ZFMISC_1:31;
then A5: Cl {y} c= Cl {x} by TOPS_1:5;
{x} c= Cl {y} by A3, ZFMISC_1:31;
then Cl {x} c= Cl {y} by TOPS_1:5;
then Cl {x} = Cl {y} by A5, XBOOLE_0:def_10;
hence contradiction by A1, A2, Def5; ::_thesis: verum
end;
end;
assume A6: for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} ) ; ::_thesis: X is T_0
for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y}
proof
let x, y be Point of X; ::_thesis: ( x <> y implies Cl {x} <> Cl {y} )
assume A7: x <> y ; ::_thesis: Cl {x} <> Cl {y}
assume A8: Cl {x} = Cl {y} ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( not x in Cl {y} or not y in Cl {x} ) by A6, A7;
suppose not x in Cl {y} ; ::_thesis: contradiction
hence contradiction by A8, Lm2; ::_thesis: verum
end;
suppose not y in Cl {x} ; ::_thesis: contradiction
hence contradiction by A8, Lm2; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence X is T_0 by Def5; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines T_0 TSP_1:def_6_:_
for X being non empty TopSpace holds
( X is T_0 iff for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} ) );
definition
let X be non empty TopSpace;
redefine attr X is T_0 means :: TSP_1:def 7
for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x};
compatibility
( X is T_0 iff for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} )
proof
thus ( X is T_0 implies for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} ) ::_thesis: ( ( for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} ) implies X is T_0 )
proof
assume A1: X is T_0 ; ::_thesis: for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x}
hereby ::_thesis: verum
let x, y be Point of X; ::_thesis: ( x <> y & x in Cl {y} implies not Cl {y} c= Cl {x} )
assume A2: x <> y ; ::_thesis: ( x in Cl {y} implies not Cl {y} c= Cl {x} )
assume x in Cl {y} ; ::_thesis: not Cl {y} c= Cl {x}
then {x} c= Cl {y} by ZFMISC_1:31;
then A3: Cl {x} c= Cl {y} by TOPS_1:5;
assume Cl {y} c= Cl {x} ; ::_thesis: contradiction
then Cl {x} = Cl {y} by A3, XBOOLE_0:def_10;
hence contradiction by A1, A2, Def5; ::_thesis: verum
end;
end;
assume A4: for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} ; ::_thesis: X is T_0
for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} )
proof
let x, y be Point of X; ::_thesis: ( not x <> y or not x in Cl {y} or not y in Cl {x} )
assume A5: x <> y ; ::_thesis: ( not x in Cl {y} or not y in Cl {x} )
assume A6: x in Cl {y} ; ::_thesis: not y in Cl {x}
assume y in Cl {x} ; ::_thesis: contradiction
then {y} c= Cl {x} by ZFMISC_1:31;
hence contradiction by A4, A5, A6, TOPS_1:5; ::_thesis: verum
end;
hence X is T_0 by Def6; ::_thesis: verum
end;
end;
:: deftheorem defines T_0 TSP_1:def_7_:_
for X being non empty TopSpace holds
( X is T_0 iff for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} );
registration
cluster non empty TopSpace-like T_0 almost_discrete -> non empty discrete for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is almost_discrete & b1 is T_0 holds
b1 is discrete
proof
let Y be non empty TopSpace; ::_thesis: ( Y is almost_discrete & Y is T_0 implies Y is discrete )
assume A1: ( Y is almost_discrete & Y is T_0 ) ; ::_thesis: Y is discrete
for A being Subset of Y
for x being Point of Y st A = {x} holds
A is closed
proof
let A be Subset of Y; ::_thesis: for x being Point of Y st A = {x} holds
A is closed
let x be Point of Y; ::_thesis: ( A = {x} implies A is closed )
x in Cl {x} by Lm2;
then A2: {x} c= Cl {x} by ZFMISC_1:31;
A3: now__::_thesis:_Cl_{x}_c=_{x}
assume not Cl {x} c= {x} ; ::_thesis: contradiction
then consider a being set such that
A4: a in Cl {x} and
A5: not a in {x} by TARSKI:def_3;
reconsider a = a as Point of Y by A4;
a <> x by A5, TARSKI:def_1;
then not x in Cl {a} by A1, A4, Def6;
then x in (Cl {a}) ` by SUBSET_1:29;
then {x} c= (Cl {a}) ` by ZFMISC_1:31;
then A6: {x} misses Cl {a} by SUBSET_1:23;
A7: ( a in {a} & {a} c= Cl {a} ) by PRE_TOPC:18, TARSKI:def_1;
Cl {a} is open by A1, TDLAT_3:22;
then Cl {x} misses Cl {a} by A6, TSEP_1:36;
hence contradiction by A4, A7, XBOOLE_0:3; ::_thesis: verum
end;
assume A = {x} ; ::_thesis: A is closed
hence A is closed by A2, A3, XBOOLE_0:def_10; ::_thesis: verum
end;
hence Y is discrete by A1, TDLAT_3:26; ::_thesis: verum
end;
cluster non empty TopSpace-like non discrete almost_discrete -> non empty non T_0 for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is almost_discrete & not b1 is discrete holds
not b1 is T_0 ;
cluster non empty TopSpace-like T_0 non discrete -> non empty non almost_discrete for TopStruct ;
coherence
for b1 being non empty TopSpace st not b1 is discrete & b1 is T_0 holds
not b1 is almost_discrete ;
end;
definition
mode Kolmogorov_space is non empty T_0 TopSpace;
mode non-Kolmogorov_space is non empty non T_0 TopSpace;
end;
registration
cluster non empty non trivial strict TopSpace-like T_0 for TopStruct ;
existence
ex b1 being Kolmogorov_space st
( not b1 is trivial & b1 is strict )
proof
set X = the non empty non trivial strict discrete TopSpace;
take the non empty non trivial strict discrete TopSpace ; ::_thesis: ( not the non empty non trivial strict discrete TopSpace is trivial & the non empty non trivial strict discrete TopSpace is strict )
thus ( not the non empty non trivial strict discrete TopSpace is trivial & the non empty non trivial strict discrete TopSpace is strict ) ; ::_thesis: verum
end;
cluster non empty non trivial strict TopSpace-like non T_0 non discrete for TopStruct ;
existence
ex b1 being non-Kolmogorov_space st
( not b1 is trivial & b1 is strict )
proof
set X = the non empty non trivial strict anti-discrete TopSpace;
take the non empty non trivial strict anti-discrete TopSpace ; ::_thesis: ( not the non empty non trivial strict anti-discrete TopSpace is trivial & the non empty non trivial strict anti-discrete TopSpace is strict )
thus ( not the non empty non trivial strict anti-discrete TopSpace is trivial & the non empty non trivial strict anti-discrete TopSpace is strict ) ; ::_thesis: verum
end;
end;
begin
definition
let Y be TopStruct ;
let IT be Subset of Y;
attrIT is T_0 means :Def8: :: TSP_1:def 8
for x, y being Point of Y st x in IT & y in IT & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W );
end;
:: deftheorem Def8 defines T_0 TSP_1:def_8_:_
for Y being TopStruct
for IT being Subset of Y holds
( IT is T_0 iff for x, y being Point of Y st x in IT & y in IT & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) );
definition
let Y be non empty TopStruct ;
let A be Subset of Y;
redefine attr A is T_0 means :Def9: :: TSP_1:def 9
for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F );
compatibility
( A is T_0 iff for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
proof
thus ( A is T_0 implies for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ::_thesis: ( ( for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) implies A is T_0 )
proof
assume A1: for x, y being Point of Y st x in A & y in A & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) ; :: according to TSP_1:def_8 ::_thesis: for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F )
let x, y be Point of Y; ::_thesis: ( x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) implies ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
assume A2: ( x in A & y in A & x <> y ) ; ::_thesis: ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
hereby ::_thesis: verum
percases ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A1, A2;
suppose ex V being Subset of Y st
( V is open & x in V & not y in V ) ; ::_thesis: ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
then consider V being Subset of Y such that
A3: V is open and
A4: x in V and
A5: not y in V ;
now__::_thesis:_ex_F_being_Element_of_K19(_the_carrier_of_Y)_st_
(_F_is_closed_&_not_x_in_F_&_y_in_F_)
take F = V ` ; ::_thesis: ( F is closed & not x in F & y in F )
V = ([#] Y) \ F by PRE_TOPC:3;
hence F is closed by A3, PRE_TOPC:def_3; ::_thesis: ( not x in F & y in F )
thus not x in F by A4, XBOOLE_0:def_5; ::_thesis: y in F
thus y in F by A5, SUBSET_1:29; ::_thesis: verum
end;
hence ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ; ::_thesis: verum
end;
suppose ex W being Subset of Y st
( W is open & not x in W & y in W ) ; ::_thesis: ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
then consider W being Subset of Y such that
A6: W is open and
A7: not x in W and
A8: y in W ;
now__::_thesis:_ex_E_being_Element_of_K19(_the_carrier_of_Y)_st_
(_E_is_closed_&_x_in_E_&_not_y_in_E_)
take E = W ` ; ::_thesis: ( E is closed & x in E & not y in E )
W = ([#] Y) \ E by PRE_TOPC:3;
hence E is closed by A6, PRE_TOPC:def_3; ::_thesis: ( x in E & not y in E )
thus x in E by A7, SUBSET_1:29; ::_thesis: not y in E
thus not y in E by A8, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ; ::_thesis: verum
end;
end;
end;
end;
assume A9: for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) ; ::_thesis: A is T_0
for x, y being Point of Y st x in A & y in A & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W )
proof
let x, y be Point of Y; ::_thesis: ( x in A & y in A & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) implies ex W being Subset of Y st
( W is open & not x in W & y in W ) )
assume A10: ( x in A & y in A & x <> y ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
hereby ::_thesis: verum
percases ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) by A9, A10;
suppose ex E being Subset of Y st
( E is closed & x in E & not y in E ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
then consider E being Subset of Y such that
A11: E is closed and
A12: x in E and
A13: not y in E ;
now__::_thesis:_ex_W_being_Element_of_K19(_the_carrier_of_Y)_st_
(_W_is_open_&_not_x_in_W_&_y_in_W_)
take W = E ` ; ::_thesis: ( W is open & not x in W & y in W )
W = ([#] Y) \ E ;
hence W is open by A11, PRE_TOPC:def_3; ::_thesis: ( not x in W & y in W )
thus not x in W by A12, XBOOLE_0:def_5; ::_thesis: y in W
thus y in W by A13, SUBSET_1:29; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
suppose ex F being Subset of Y st
( F is closed & not x in F & y in F ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
then consider F being Subset of Y such that
A14: F is closed and
A15: not x in F and
A16: y in F ;
now__::_thesis:_ex_V_being_Element_of_K19(_the_carrier_of_Y)_st_
(_V_is_open_&_x_in_V_&_not_y_in_V_)
take V = F ` ; ::_thesis: ( V is open & x in V & not y in V )
V = ([#] Y) \ F ;
hence V is open by A14, PRE_TOPC:def_3; ::_thesis: ( x in V & not y in V )
thus x in V by A15, SUBSET_1:29; ::_thesis: not y in V
thus not y in V by A16, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
end;
end;
end;
hence A is T_0 by Def8; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines T_0 TSP_1:def_9_:_
for Y being non empty TopStruct
for A being Subset of Y holds
( A is T_0 iff for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) );
theorem :: TSP_1:3
for Y0, Y1 being TopStruct
for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 holds
D1 is T_0
proof
let Y0, Y1 be TopStruct ; ::_thesis: for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 holds
D1 is T_0
let D0 be Subset of Y0; ::_thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 holds
D1 is T_0
let D1 be Subset of Y1; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 implies D1 is T_0 )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not D0 = D1 or not D0 is T_0 or D1 is T_0 )
assume A2: D0 = D1 ; ::_thesis: ( not D0 is T_0 or D1 is T_0 )
assume A3: D0 is T_0 ; ::_thesis: D1 is T_0
now__::_thesis:_for_x,_y_being_Point_of_Y1_st_x_in_D1_&_y_in_D1_&_x_<>_y_&_(_for_V1_being_Subset_of_Y1_holds_
(_not_V1_is_open_or_not_x_in_V1_or_y_in_V1_)_)_holds_
ex_W1_being_Subset_of_Y1_st_
(_W1_is_open_&_not_x_in_W1_&_y_in_W1_)
let x, y be Point of Y1; ::_thesis: ( x in D1 & y in D1 & x <> y & ( for V1 being Subset of Y1 holds
( not V1 is open or not x in V1 or y in V1 ) ) implies ex W1 being Subset of Y1 st
( W1 is open & not x in W1 & y in W1 ) )
reconsider x0 = x, y0 = y as Point of Y0 by A1;
assume A4: ( x in D1 & y in D1 ) ; ::_thesis: ( not x <> y or ex V1 being Subset of Y1 st
( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st
( W1 is open & not x in W1 & y in W1 ) )
assume A5: x <> y ; ::_thesis: ( ex V1 being Subset of Y1 st
( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st
( W1 is open & not x in W1 & y in W1 ) )
hereby ::_thesis: verum
percases ( ex V being Subset of Y0 st
( V is open & x0 in V & not y0 in V ) or ex W being Subset of Y0 st
( W is open & not x0 in W & y0 in W ) ) by A2, A3, A4, A5, Def8;
suppose ex V being Subset of Y0 st
( V is open & x0 in V & not y0 in V ) ; ::_thesis: ( ex V1 being Subset of Y1 st
( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st
( W1 is open & not x in W1 & y in W1 ) )
then consider V being Subset of Y0 such that
A6: V is open and
A7: ( x0 in V & not y0 in V ) ;
reconsider V1 = V as Subset of Y1 by A1;
now__::_thesis:_ex_V1_being_Subset_of_Y1_st_
(_V1_is_open_&_x_in_V1_&_not_y_in_V1_)
take V1 = V1; ::_thesis: ( V1 is open & x in V1 & not y in V1 )
V1 in the topology of Y1 by A1, A6, PRE_TOPC:def_2;
hence V1 is open by PRE_TOPC:def_2; ::_thesis: ( x in V1 & not y in V1 )
thus ( x in V1 & not y in V1 ) by A7; ::_thesis: verum
end;
hence ( ex V1 being Subset of Y1 st
( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st
( W1 is open & not x in W1 & y in W1 ) ) ; ::_thesis: verum
end;
suppose ex W being Subset of Y0 st
( W is open & not x0 in W & y0 in W ) ; ::_thesis: ( ex V1 being Subset of Y1 st
( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st
( W1 is open & not x in W1 & y in W1 ) )
then consider W being Subset of Y0 such that
A8: W is open and
A9: ( not x0 in W & y0 in W ) ;
reconsider W1 = W as Subset of Y1 by A1;
now__::_thesis:_ex_W1_being_Subset_of_Y1_st_
(_W1_is_open_&_not_x_in_W1_&_y_in_W1_)
take W1 = W1; ::_thesis: ( W1 is open & not x in W1 & y in W1 )
W1 in the topology of Y1 by A1, A8, PRE_TOPC:def_2;
hence W1 is open by PRE_TOPC:def_2; ::_thesis: ( not x in W1 & y in W1 )
thus ( not x in W1 & y in W1 ) by A9; ::_thesis: verum
end;
hence ( ex V1 being Subset of Y1 st
( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st
( W1 is open & not x in W1 & y in W1 ) ) ; ::_thesis: verum
end;
end;
end;
end;
hence D1 is T_0 by Def8; ::_thesis: verum
end;
theorem Th4: :: TSP_1:4
for Y being non empty TopStruct
for A being Subset of Y st A = the carrier of Y holds
( A is T_0 iff Y is T_0 )
proof
let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y st A = the carrier of Y holds
( A is T_0 iff Y is T_0 )
let A be Subset of Y; ::_thesis: ( A = the carrier of Y implies ( A is T_0 iff Y is T_0 ) )
assume A1: A = the carrier of Y ; ::_thesis: ( A is T_0 iff Y is T_0 )
hereby ::_thesis: ( Y is T_0 implies A is T_0 )
assume A is T_0 ; ::_thesis: Y is T_0
then for x, y being Point of Y holds
( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A1, Def8;
hence Y is T_0 by Def3; ::_thesis: verum
end;
hereby ::_thesis: verum
assume Y is T_0 ; ::_thesis: A is T_0
then for x, y being Point of Y st x in A & y in A & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) by Def3;
hence A is T_0 by Def8; ::_thesis: verum
end;
end;
theorem Th5: :: TSP_1:5
for Y being non empty TopStruct
for A, B being Subset of Y st B c= A & A is T_0 holds
B is T_0
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st B c= A & A is T_0 holds
B is T_0
let A, B be Subset of Y; ::_thesis: ( B c= A & A is T_0 implies B is T_0 )
assume A1: B c= A ; ::_thesis: ( not A is T_0 or B is T_0 )
assume A is T_0 ; ::_thesis: B is T_0
then for x, y being Point of Y st x in B & y in B & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) by A1, Def8;
hence B is T_0 by Def8; ::_thesis: verum
end;
theorem Th6: :: TSP_1:6
for Y being non empty TopStruct
for A, B being Subset of Y st ( A is T_0 or B is T_0 ) holds
A /\ B is T_0
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st ( A is T_0 or B is T_0 ) holds
A /\ B is T_0
let A, B be Subset of Y; ::_thesis: ( ( A is T_0 or B is T_0 ) implies A /\ B is T_0 )
assume A1: ( A is T_0 or B is T_0 ) ; ::_thesis: A /\ B is T_0
hereby ::_thesis: verum
percases ( A is T_0 or B is T_0 ) by A1;
suppose A is T_0 ; ::_thesis: A /\ B is T_0
hence A /\ B is T_0 by Th5, XBOOLE_1:17; ::_thesis: verum
end;
suppose B is T_0 ; ::_thesis: A /\ B is T_0
hence A /\ B is T_0 by Th5, XBOOLE_1:17; ::_thesis: verum
end;
end;
end;
end;
theorem Th7: :: TSP_1:7
for Y being non empty TopStruct
for A, B being Subset of Y st ( A is open or B is open ) & A is T_0 & B is T_0 holds
A \/ B is T_0
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st ( A is open or B is open ) & A is T_0 & B is T_0 holds
A \/ B is T_0
let A, B be Subset of Y; ::_thesis: ( ( A is open or B is open ) & A is T_0 & B is T_0 implies A \/ B is T_0 )
assume A1: ( A is open or B is open ) ; ::_thesis: ( not A is T_0 or not B is T_0 or A \/ B is T_0 )
assume that
A2: A is T_0 and
A3: B is T_0 ; ::_thesis: A \/ B is T_0
now__::_thesis:_for_x,_y_being_Point_of_Y_st_x_in_A_\/_B_&_y_in_A_\/_B_&_x_<>_y_&_(_for_V_being_Subset_of_Y_holds_
(_not_V_is_open_or_not_x_in_V_or_y_in_V_)_)_holds_
ex_W_being_Subset_of_Y_st_
(_W_is_open_&_not_x_in_W_&_y_in_W_)
let x, y be Point of Y; ::_thesis: ( x in A \/ B & y in A \/ B & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) implies ex W being Subset of Y st
( W is open & not x in W & y in W ) )
assume A4: ( x in A \/ B & y in A \/ B ) ; ::_thesis: ( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
then A5: ( x in (A \ B) \/ B & y in (A \ B) \/ B ) by XBOOLE_1:39;
assume A6: x <> y ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
A7: ( x in A \/ (B \ A) & y in A \/ (B \ A) ) by A4, XBOOLE_1:39;
now__::_thesis:_(_ex_V_being_Subset_of_Y_st_
(_V_is_open_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_
(_W_is_open_&_not_x_in_W_&_y_in_W_)_)
percases ( A is open or B is open ) by A1;
supposeA8: A is open ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
now__::_thesis:_(_ex_V_being_Subset_of_Y_st_
(_V_is_open_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_
(_W_is_open_&_not_x_in_W_&_y_in_W_)_)
percases ( ( x in A & y in A ) or ( x in A & y in B \ A ) or ( x in B \ A & y in A ) or ( x in B \ A & y in B \ A ) ) by A7, XBOOLE_0:def_3;
suppose ( x in A & y in A ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A2, A6, Def8; ::_thesis: verum
end;
supposeA9: ( x in A & y in B \ A ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
now__::_thesis:_ex_A_being_Subset_of_Y_st_
(_A_is_open_&_x_in_A_&_not_y_in_A_)
take A = A; ::_thesis: ( A is open & x in A & not y in A )
thus A is open by A8; ::_thesis: ( x in A & not y in A )
thus x in A by A9; ::_thesis: not y in A
thus not y in A by A9, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
supposeA10: ( x in B \ A & y in A ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
now__::_thesis:_ex_A_being_Subset_of_Y_st_
(_A_is_open_&_not_x_in_A_&_y_in_A_)
take A = A; ::_thesis: ( A is open & not x in A & y in A )
thus A is open by A8; ::_thesis: ( not x in A & y in A )
thus not x in A by A10, XBOOLE_0:def_5; ::_thesis: y in A
thus y in A by A10; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
supposeA11: ( x in B \ A & y in B \ A ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
B \ A c= B by XBOOLE_1:36;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A3, A6, A11, Def8; ::_thesis: verum
end;
end;
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
supposeA12: B is open ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
now__::_thesis:_(_ex_V_being_Subset_of_Y_st_
(_V_is_open_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_
(_W_is_open_&_not_x_in_W_&_y_in_W_)_)
percases ( ( x in A \ B & y in A \ B ) or ( x in A \ B & y in B ) or ( x in B & y in A \ B ) or ( x in B & y in B ) ) by A5, XBOOLE_0:def_3;
supposeA13: ( x in A \ B & y in A \ B ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
A \ B c= A by XBOOLE_1:36;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A2, A6, A13, Def8; ::_thesis: verum
end;
supposeA14: ( x in A \ B & y in B ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
now__::_thesis:_ex_B_being_Subset_of_Y_st_
(_B_is_open_&_not_x_in_B_&_y_in_B_)
take B = B; ::_thesis: ( B is open & not x in B & y in B )
thus B is open by A12; ::_thesis: ( not x in B & y in B )
thus not x in B by A14, XBOOLE_0:def_5; ::_thesis: y in B
thus y in B by A14; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
supposeA15: ( x in B & y in A \ B ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
now__::_thesis:_ex_B_being_Subset_of_Y_st_
(_B_is_open_&_x_in_B_&_not_y_in_B_)
take B = B; ::_thesis: ( B is open & x in B & not y in B )
thus B is open by A12; ::_thesis: ( x in B & not y in B )
thus x in B by A15; ::_thesis: not y in B
thus not y in B by A15, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
suppose ( x in B & y in B ) ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A3, A6, Def8; ::_thesis: verum
end;
end;
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
end;
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
hence A \/ B is T_0 by Def8; ::_thesis: verum
end;
theorem Th8: :: TSP_1:8
for Y being non empty TopStruct
for A, B being Subset of Y st ( A is closed or B is closed ) & A is T_0 & B is T_0 holds
A \/ B is T_0
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st ( A is closed or B is closed ) & A is T_0 & B is T_0 holds
A \/ B is T_0
let A, B be Subset of Y; ::_thesis: ( ( A is closed or B is closed ) & A is T_0 & B is T_0 implies A \/ B is T_0 )
assume A1: ( A is closed or B is closed ) ; ::_thesis: ( not A is T_0 or not B is T_0 or A \/ B is T_0 )
assume that
A2: A is T_0 and
A3: B is T_0 ; ::_thesis: A \/ B is T_0
now__::_thesis:_for_x,_y_being_Point_of_Y_st_x_in_A_\/_B_&_y_in_A_\/_B_&_x_<>_y_&_(_for_V_being_Subset_of_Y_holds_
(_not_V_is_closed_or_not_x_in_V_or_y_in_V_)_)_holds_
ex_W_being_Subset_of_Y_st_
(_W_is_closed_&_not_x_in_W_&_y_in_W_)
let x, y be Point of Y; ::_thesis: ( x in A \/ B & y in A \/ B & x <> y & ( for V being Subset of Y holds
( not V is closed or not x in V or y in V ) ) implies ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
assume A4: ( x in A \/ B & y in A \/ B ) ; ::_thesis: ( not x <> y or ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
then A5: ( x in (A \ B) \/ B & y in (A \ B) \/ B ) by XBOOLE_1:39;
assume A6: x <> y ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
A7: ( x in A \/ (B \ A) & y in A \/ (B \ A) ) by A4, XBOOLE_1:39;
now__::_thesis:_(_ex_V_being_Subset_of_Y_st_
(_V_is_closed_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_
(_W_is_closed_&_not_x_in_W_&_y_in_W_)_)
percases ( A is closed or B is closed ) by A1;
supposeA8: A is closed ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
now__::_thesis:_(_ex_V_being_Subset_of_Y_st_
(_V_is_closed_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_
(_W_is_closed_&_not_x_in_W_&_y_in_W_)_)
percases ( ( x in A & y in A ) or ( x in A & y in B \ A ) or ( x in B \ A & y in A ) or ( x in B \ A & y in B \ A ) ) by A7, XBOOLE_0:def_3;
suppose ( x in A & y in A ) ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) by A2, A6, Def9; ::_thesis: verum
end;
supposeA9: ( x in A & y in B \ A ) ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
now__::_thesis:_ex_A_being_Subset_of_Y_st_
(_A_is_closed_&_x_in_A_&_not_y_in_A_)
take A = A; ::_thesis: ( A is closed & x in A & not y in A )
thus A is closed by A8; ::_thesis: ( x in A & not y in A )
thus x in A by A9; ::_thesis: not y in A
thus not y in A by A9, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; ::_thesis: verum
end;
supposeA10: ( x in B \ A & y in A ) ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
now__::_thesis:_ex_A_being_Subset_of_Y_st_
(_A_is_closed_&_not_x_in_A_&_y_in_A_)
take A = A; ::_thesis: ( A is closed & not x in A & y in A )
thus A is closed by A8; ::_thesis: ( not x in A & y in A )
thus not x in A by A10, XBOOLE_0:def_5; ::_thesis: y in A
thus y in A by A10; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; ::_thesis: verum
end;
supposeA11: ( x in B \ A & y in B \ A ) ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
B \ A c= B by XBOOLE_1:36;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) by A3, A6, A11, Def9; ::_thesis: verum
end;
end;
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; ::_thesis: verum
end;
supposeA12: B is closed ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
now__::_thesis:_(_ex_V_being_Subset_of_Y_st_
(_V_is_closed_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_
(_W_is_closed_&_not_x_in_W_&_y_in_W_)_)
percases ( ( x in A \ B & y in A \ B ) or ( x in A \ B & y in B ) or ( x in B & y in A \ B ) or ( x in B & y in B ) ) by A5, XBOOLE_0:def_3;
supposeA13: ( x in A \ B & y in A \ B ) ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
A \ B c= A by XBOOLE_1:36;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) by A2, A6, A13, Def9; ::_thesis: verum
end;
supposeA14: ( x in A \ B & y in B ) ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
now__::_thesis:_ex_B_being_Subset_of_Y_st_
(_B_is_closed_&_not_x_in_B_&_y_in_B_)
take B = B; ::_thesis: ( B is closed & not x in B & y in B )
thus B is closed by A12; ::_thesis: ( not x in B & y in B )
thus not x in B by A14, XBOOLE_0:def_5; ::_thesis: y in B
thus y in B by A14; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; ::_thesis: verum
end;
supposeA15: ( x in B & y in A \ B ) ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
now__::_thesis:_ex_B_being_Subset_of_Y_st_
(_B_is_closed_&_x_in_B_&_not_y_in_B_)
take B = B; ::_thesis: ( B is closed & x in B & not y in B )
thus B is closed by A12; ::_thesis: ( x in B & not y in B )
thus x in B by A15; ::_thesis: not y in B
thus not y in B by A15, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; ::_thesis: verum
end;
suppose ( x in B & y in B ) ; ::_thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) by A3, A6, Def9; ::_thesis: verum
end;
end;
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; ::_thesis: verum
end;
end;
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; ::_thesis: verum
end;
hence A \/ B is T_0 by Def9; ::_thesis: verum
end;
theorem Th9: :: TSP_1:9
for Y being non empty TopStruct
for A being Subset of Y st A is discrete holds
A is T_0
proof
let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y st A is discrete holds
A is T_0
let A be Subset of Y; ::_thesis: ( A is discrete implies A is T_0 )
assume A1: A is discrete ; ::_thesis: A is T_0
now__::_thesis:_for_x,_y_being_Point_of_Y_st_x_in_A_&_y_in_A_&_x_<>_y_&_(_for_V_being_Subset_of_Y_holds_
(_not_V_is_open_or_not_x_in_V_or_y_in_V_)_)_holds_
ex_W_being_Subset_of_Y_st_
(_W_is_open_&_not_x_in_W_&_y_in_W_)
let x, y be Point of Y; ::_thesis: ( x in A & y in A & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) implies ex W being Subset of Y st
( W is open & not x in W & y in W ) )
assume that
A2: x in A and
A3: y in A ; ::_thesis: ( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
{x} c= A by A2, ZFMISC_1:31;
then consider G being Subset of Y such that
A4: G is open and
A5: A /\ G = {x} by A1, TEX_2:def_3;
assume A6: x <> y ; ::_thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
now__::_thesis:_ex_G_being_Subset_of_Y_st_
(_G_is_open_&_x_in_G_&_not_y_in_G_)
take G = G; ::_thesis: ( G is open & x in G & not y in G )
thus G is open by A4; ::_thesis: ( x in G & not y in G )
x in {x} by TARSKI:def_1;
hence x in G by A5, XBOOLE_0:def_4; ::_thesis: not y in G
now__::_thesis:_not_y_in_G
assume y in G ; ::_thesis: contradiction
then y in {x} by A3, A5, XBOOLE_0:def_4;
hence contradiction by A6, TARSKI:def_1; ::_thesis: verum
end;
hence not y in G ; ::_thesis: verum
end;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: verum
end;
hence A is T_0 by Def8; ::_thesis: verum
end;
theorem :: TSP_1:10
for Y being non empty TopStruct
for A being non empty Subset of Y st A is anti-discrete & not A is trivial holds
not A is T_0
proof
let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y st A is anti-discrete & not A is trivial holds
not A is T_0
let A be non empty Subset of Y; ::_thesis: ( A is anti-discrete & not A is trivial implies not A is T_0 )
assume A1: A is anti-discrete ; ::_thesis: ( A is trivial or not A is T_0 )
consider s being set such that
A2: s in A by XBOOLE_0:def_1;
reconsider s0 = s as Element of A by A2;
assume not A is trivial ; ::_thesis: not A is T_0
then A <> {s0} ;
then consider t being set such that
A3: t in A and
A4: t <> s0 by ZFMISC_1:35;
reconsider s = s, t = t as Point of Y by A2, A3;
assume A5: A is T_0 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( ex E being Subset of Y st
( E is closed & s in E & not t in E ) or ex F being Subset of Y st
( F is closed & not s in F & t in F ) ) by A3, A4, A5, Def9;
suppose ex E being Subset of Y st
( E is closed & s in E & not t in E ) ; ::_thesis: contradiction
then consider E being Subset of Y such that
A6: ( E is closed & s in E ) and
A7: not t in E ;
A c= E by A1, A2, A6, TEX_4:def_2;
hence contradiction by A3, A7; ::_thesis: verum
end;
suppose ex F being Subset of Y st
( F is closed & not s in F & t in F ) ; ::_thesis: contradiction
then consider F being Subset of Y such that
A8: F is closed and
A9: not s in F and
A10: t in F ;
A c= F by A1, A3, A8, A10, TEX_4:def_2;
hence contradiction by A2, A9; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :Def10: :: TSP_1:def 10
for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y};
compatibility
( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y} )
proof
thus ( A is T_0 implies for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y} ) ::_thesis: ( ( for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y} ) implies A is T_0 )
proof
assume A1: A is T_0 ; ::_thesis: for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y}
hereby ::_thesis: verum
let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y implies Cl {x} <> Cl {y} )
assume A2: ( x in A & y in A & x <> y ) ; ::_thesis: Cl {x} <> Cl {y}
now__::_thesis:_not_Cl_{x}_=_Cl_{y}
percases ( ex V being Subset of X st
( V is open & x in V & not y in V ) or ex W being Subset of X st
( W is open & not x in W & y in W ) ) by A1, A2, Def8;
suppose ex V being Subset of X st
( V is open & x in V & not y in V ) ; ::_thesis: not Cl {x} = Cl {y}
then consider V being Subset of X such that
A3: V is open and
A4: x in V and
A5: not y in V ;
y in V ` by A5, SUBSET_1:29;
then {y} c= V ` by ZFMISC_1:31;
then A6: {y} misses V by SUBSET_1:23;
assume A7: Cl {x} = Cl {y} ; ::_thesis: contradiction
( x in {x} & {x} c= Cl {x} ) by PRE_TOPC:18, TARSKI:def_1;
then Cl {x} meets V by A4, XBOOLE_0:3;
hence contradiction by A3, A6, A7, TSEP_1:36; ::_thesis: verum
end;
suppose ex W being Subset of X st
( W is open & not x in W & y in W ) ; ::_thesis: not Cl {x} = Cl {y}
then consider W being Subset of X such that
A8: W is open and
A9: not x in W and
A10: y in W ;
x in W ` by A9, SUBSET_1:29;
then {x} c= W ` by ZFMISC_1:31;
then A11: {x} misses W by SUBSET_1:23;
assume A12: Cl {x} = Cl {y} ; ::_thesis: contradiction
( y in {y} & {y} c= Cl {y} ) by PRE_TOPC:18, TARSKI:def_1;
then Cl {y} meets W by A10, XBOOLE_0:3;
hence contradiction by A8, A11, A12, TSEP_1:36; ::_thesis: verum
end;
end;
end;
hence Cl {x} <> Cl {y} ; ::_thesis: verum
end;
end;
assume A13: for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y} ; ::_thesis: A is T_0
now__::_thesis:_for_x,_y_being_Point_of_X_st_x_in_A_&_y_in_A_&_x_<>_y_&_(_for_E_being_Subset_of_X_st_E_is_closed_&_x_in_E_holds_
y_in_E_)_holds_
ex_F_being_Subset_of_X_st_
(_F_is_closed_&_not_x_in_F_&_y_in_F_)
let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y & ( for E being Subset of X st E is closed & x in E holds
y in E ) implies ex F being Subset of X st
( F is closed & not x in F & y in F ) )
assume A14: ( x in A & y in A & x <> y ) ; ::_thesis: ( ( for E being Subset of X st E is closed & x in E holds
y in E ) implies ex F being Subset of X st
( F is closed & not x in F & y in F ) )
assume A15: for E being Subset of X st E is closed & x in E holds
y in E ; ::_thesis: ex F being Subset of X st
( F is closed & not x in F & y in F )
thus ex F being Subset of X st
( F is closed & not x in F & y in F ) ::_thesis: verum
proof
set F = Cl {y};
take Cl {y} ; ::_thesis: ( Cl {y} is closed & not x in Cl {y} & y in Cl {y} )
thus Cl {y} is closed ; ::_thesis: ( not x in Cl {y} & y in Cl {y} )
now__::_thesis:_not_x_in_Cl_{y}
assume x in Cl {y} ; ::_thesis: contradiction
then {x} c= Cl {y} by ZFMISC_1:31;
then A16: Cl {x} c= Cl {y} by TOPS_1:5;
y in Cl {x} by A15, Lm2;
then {y} c= Cl {x} by ZFMISC_1:31;
then Cl {y} c= Cl {x} by TOPS_1:5;
then Cl {x} = Cl {y} by A16, XBOOLE_0:def_10;
hence contradiction by A13, A14; ::_thesis: verum
end;
hence not x in Cl {y} ; ::_thesis: y in Cl {y}
thus y in Cl {y} by Lm2; ::_thesis: verum
end;
end;
hence A is T_0 by Def9; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines T_0 TSP_1:def_10_:_
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y} );
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :Def11: :: TSP_1:def 11
for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not y in Cl {x};
compatibility
( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not y in Cl {x} )
proof
thus ( A is T_0 implies for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not y in Cl {x} ) ::_thesis: ( ( for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not y in Cl {x} ) implies A is T_0 )
proof
assume A1: A is T_0 ; ::_thesis: for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not y in Cl {x}
hereby ::_thesis: verum
let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y & x in Cl {y} implies not y in Cl {x} )
assume A2: ( x in A & y in A & x <> y ) ; ::_thesis: ( x in Cl {y} implies not y in Cl {x} )
assume that
A3: x in Cl {y} and
A4: y in Cl {x} ; ::_thesis: contradiction
{y} c= Cl {x} by A4, ZFMISC_1:31;
then A5: Cl {y} c= Cl {x} by TOPS_1:5;
{x} c= Cl {y} by A3, ZFMISC_1:31;
then Cl {x} c= Cl {y} by TOPS_1:5;
then Cl {x} = Cl {y} by A5, XBOOLE_0:def_10;
hence contradiction by A1, A2, Def10; ::_thesis: verum
end;
end;
assume A6: for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not y in Cl {x} ; ::_thesis: A is T_0
for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y}
proof
let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y implies Cl {x} <> Cl {y} )
assume A7: ( x in A & y in A & x <> y ) ; ::_thesis: Cl {x} <> Cl {y}
assume A8: Cl {x} = Cl {y} ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( not x in Cl {y} or not y in Cl {x} ) by A6, A7;
suppose not x in Cl {y} ; ::_thesis: contradiction
hence contradiction by A8, Lm2; ::_thesis: verum
end;
suppose not y in Cl {x} ; ::_thesis: contradiction
hence contradiction by A8, Lm2; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence A is T_0 by Def10; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines T_0 TSP_1:def_11_:_
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not y in Cl {x} );
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :: TSP_1:def 12
for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x};
compatibility
( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} )
proof
thus ( A is T_0 implies for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} ) ::_thesis: ( ( for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} ) implies A is T_0 )
proof
assume A1: A is T_0 ; ::_thesis: for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x}
hereby ::_thesis: verum
let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y & x in Cl {y} implies not Cl {y} c= Cl {x} )
assume A2: ( x in A & y in A & x <> y ) ; ::_thesis: ( x in Cl {y} implies not Cl {y} c= Cl {x} )
assume x in Cl {y} ; ::_thesis: not Cl {y} c= Cl {x}
then {x} c= Cl {y} by ZFMISC_1:31;
then A3: Cl {x} c= Cl {y} by TOPS_1:5;
assume Cl {y} c= Cl {x} ; ::_thesis: contradiction
then Cl {x} = Cl {y} by A3, XBOOLE_0:def_10;
hence contradiction by A1, A2, Def10; ::_thesis: verum
end;
end;
assume A4: for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} ; ::_thesis: A is T_0
for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not y in Cl {x}
proof
let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y & x in Cl {y} implies not y in Cl {x} )
assume A5: ( x in A & y in A & x <> y ) ; ::_thesis: ( not x in Cl {y} or not y in Cl {x} )
assume A6: x in Cl {y} ; ::_thesis: not y in Cl {x}
assume y in Cl {x} ; ::_thesis: contradiction
then {y} c= Cl {x} by ZFMISC_1:31;
hence contradiction by A4, A5, A6, TOPS_1:5; ::_thesis: verum
end;
hence A is T_0 by Def11; ::_thesis: verum
end;
end;
:: deftheorem defines T_0 TSP_1:def_12_:_
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} );
theorem Th11: :: TSP_1:11
for X being non empty TopSpace
for A being empty Subset of X holds A is T_0
proof
let X be non empty TopSpace; ::_thesis: for A being empty Subset of X holds A is T_0
let A be empty Subset of X; ::_thesis: A is T_0
A is discrete by TEX_2:29;
hence A is T_0 by Th9; ::_thesis: verum
end;
theorem :: TSP_1:12
for X being non empty TopSpace
for x being Point of X holds {x} is T_0 by Th9, TEX_2:30;
begin
registration
let Y be non empty TopStruct ;
cluster non empty strict T_0 for SubSpace of Y;
existence
ex b1 being SubSpace of Y st
( b1 is strict & b1 is T_0 & not b1 is empty )
proof
set X0 = the non empty trivial strict SubSpace of Y;
take the non empty trivial strict SubSpace of Y ; ::_thesis: ( the non empty trivial strict SubSpace of Y is strict & the non empty trivial strict SubSpace of Y is T_0 & not the non empty trivial strict SubSpace of Y is empty )
thus ( the non empty trivial strict SubSpace of Y is strict & the non empty trivial strict SubSpace of Y is T_0 & not the non empty trivial strict SubSpace of Y is empty ) ; ::_thesis: verum
end;
end;
Lm3: now__::_thesis:_for_Z_being_TopStruct_
for_Z0_being_SubSpace_of_Z_holds_the_carrier_of_Z0_is_Subset_of_Z
let Z be TopStruct ; ::_thesis: for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z
let Z0 be SubSpace of Z; ::_thesis: the carrier of Z0 is Subset of Z
[#] Z0 c= [#] Z by PRE_TOPC:def_4;
hence the carrier of Z0 is Subset of Z ; ::_thesis: verum
end;
definition
let Y be TopStruct ;
let Y0 be SubSpace of Y;
:: original: T_0
redefine attrY0 is T_0 means :: TSP_1:def 13
( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) );
compatibility
( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) ) )
proof
reconsider A = the carrier of Y0 as Subset of Y by Lm3;
thus ( not Y0 is T_0 or Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ::_thesis: ( ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) ) implies Y0 is T_0 )
proof
assume A1: Y0 is T_0 ; ::_thesis: ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) )
hereby ::_thesis: verum
assume A2: not Y0 is empty ; ::_thesis: for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is open or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is open & not x in F & y in F )
let x, y be Point of Y; ::_thesis: ( x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is open or not x in E or y in E ) ) implies ex F being Subset of Y st
( F is open & not x in F & y in F ) )
assume ( x is Point of Y0 & y is Point of Y0 ) ; ::_thesis: ( not x <> y or ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) )
then reconsider x0 = x, y0 = y as Point of Y0 ;
assume A3: x <> y ; ::_thesis: ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) )
now__::_thesis:_(_ex_E_being_Subset_of_Y_st_
(_E_is_open_&_x_in_E_&_not_y_in_E_)_or_ex_F_being_Subset_of_Y_st_
(_F_is_open_&_not_x_in_F_&_y_in_F_)_)
percases ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) ) by A1, A2, A3, Def3;
suppose ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) ; ::_thesis: ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) )
then consider E0 being Subset of Y0 such that
A4: E0 is open and
A5: x0 in E0 and
A6: not y0 in E0 ;
now__::_thesis:_ex_E_being_Subset_of_Y_st_
(_E_is_open_&_x_in_E_&_not_y_in_E_)
consider E being Subset of Y such that
A7: E is open and
A8: E0 = E /\ A by A4, Def1;
take E = E; ::_thesis: ( E is open & x in E & not y in E )
thus E is open by A7; ::_thesis: ( x in E & not y in E )
E /\ A c= E by XBOOLE_1:17;
hence x in E by A5, A8; ::_thesis: not y in E
thus not y in E by A2, A6, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) ) ; ::_thesis: verum
end;
suppose ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) ; ::_thesis: ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) )
then consider F0 being Subset of Y0 such that
A9: F0 is open and
A10: not x0 in F0 and
A11: y0 in F0 ;
now__::_thesis:_ex_F_being_Subset_of_Y_st_
(_F_is_open_&_not_x_in_F_&_y_in_F_)
consider F being Subset of Y such that
A12: F is open and
A13: F0 = F /\ A by A9, Def1;
take F = F; ::_thesis: ( F is open & not x in F & y in F )
thus F is open by A12; ::_thesis: ( not x in F & y in F )
thus not x in F by A2, A10, A13, XBOOLE_0:def_4; ::_thesis: y in F
F /\ A c= F by XBOOLE_1:17;
hence y in F by A11, A13; ::_thesis: verum
end;
hence ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) ) ; ::_thesis: verum
end;
end;
end;
hence ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) ) ; ::_thesis: verum
end;
end;
assume A14: ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; ::_thesis: Y0 is T_0
now__::_thesis:_(_not_Y0_is_empty_implies_for_x0,_y0_being_Point_of_Y0_holds_
(_not_x0_<>_y0_or_ex_E0_being_Subset_of_Y0_st_
(_E0_is_open_&_x0_in_E0_&_not_y0_in_E0_)_or_ex_F0_being_Subset_of_Y0_st_
(_F0_is_open_&_not_x0_in_F0_&_y0_in_F0_)_)_)
A15: the carrier of Y0 c= the carrier of Y by Def1;
assume A16: not Y0 is empty ; ::_thesis: for x0, y0 being Point of Y0 holds
( not x0 <> y0 or ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )
let x0, y0 be Point of Y0; ::_thesis: ( not x0 <> y0 or ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )
the carrier of Y0 <> {} by A16;
then ( x0 in the carrier of Y0 & y0 in the carrier of Y0 ) ;
then reconsider x = x0, y = y0 as Point of Y by A15;
assume A17: x0 <> y0 ; ::_thesis: ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )
now__::_thesis:_(_ex_E0_being_Subset_of_Y0_st_
(_E0_is_open_&_x0_in_E0_&_not_y0_in_E0_)_or_ex_F0_being_Subset_of_Y0_st_
(_F0_is_open_&_not_x0_in_F0_&_y0_in_F0_)_)
percases ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) ) by A14, A16, A17;
suppose ex E being Subset of Y st
( E is open & x in E & not y in E ) ; ::_thesis: ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )
then consider E being Subset of Y such that
A18: E is open and
A19: x in E and
A20: not y in E ;
now__::_thesis:_ex_E0_being_Subset_of_Y0_st_
(_E0_is_open_&_x0_in_E0_&_not_y0_in_E0_)
consider E0 being Subset of Y0 such that
A21: E0 is open and
A22: E0 = E /\ A by A18, Th1;
take E0 = E0; ::_thesis: ( E0 is open & x0 in E0 & not y0 in E0 )
thus E0 is open by A21; ::_thesis: ( x0 in E0 & not y0 in E0 )
thus x0 in E0 by A16, A19, A22, XBOOLE_0:def_4; ::_thesis: not y0 in E0
now__::_thesis:_not_y0_in_E0
A23: E /\ A c= E by XBOOLE_1:17;
assume y0 in E0 ; ::_thesis: contradiction
hence contradiction by A20, A22, A23; ::_thesis: verum
end;
hence not y0 in E0 ; ::_thesis: verum
end;
hence ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) ) ; ::_thesis: verum
end;
suppose ex F being Subset of Y st
( F is open & not x in F & y in F ) ; ::_thesis: ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )
then consider F being Subset of Y such that
A24: F is open and
A25: not x in F and
A26: y in F ;
now__::_thesis:_ex_F0_being_Subset_of_Y0_st_
(_F0_is_open_&_not_x0_in_F0_&_y0_in_F0_)
consider F0 being Subset of Y0 such that
A27: F0 is open and
A28: F0 = F /\ A by A24, Th1;
take F0 = F0; ::_thesis: ( F0 is open & not x0 in F0 & y0 in F0 )
thus F0 is open by A27; ::_thesis: ( not x0 in F0 & y0 in F0 )
now__::_thesis:_not_x0_in_F0
A29: F /\ A c= F by XBOOLE_1:17;
assume x0 in F0 ; ::_thesis: contradiction
hence contradiction by A25, A28, A29; ::_thesis: verum
end;
hence not x0 in F0 ; ::_thesis: y0 in F0
thus y0 in F0 by A16, A26, A28, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) ) ; ::_thesis: verum
end;
end;
end;
hence ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) ) ; ::_thesis: verum
end;
hence Y0 is T_0 by Def3; ::_thesis: verum
end;
end;
:: deftheorem defines T_0 TSP_1:def_13_:_
for Y being TopStruct
for Y0 being SubSpace of Y holds
( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) ) );
definition
let Y be TopStruct ;
let Y0 be SubSpace of Y;
:: original: T_0
redefine attrY0 is T_0 means :Def14: :: TSP_1:def 14
( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) );
compatibility
( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) )
proof
reconsider A = the carrier of Y0 as Subset of Y by Lm3;
thus ( not Y0 is V138() or Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ::_thesis: ( ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) implies Y0 is T_0 )
proof
assume A1: Y0 is V138() ; ::_thesis: ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
hereby ::_thesis: verum
assume A2: not Y0 is empty ; ::_thesis: for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F )
let x, y be Point of Y; ::_thesis: ( x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) implies ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
assume ( x is Point of Y0 & y is Point of Y0 ) ; ::_thesis: ( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
then reconsider x0 = x, y0 = y as Point of Y0 ;
assume A3: x <> y ; ::_thesis: ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
now__::_thesis:_(_ex_E_being_Subset_of_Y_st_
(_E_is_closed_&_x_in_E_&_not_y_in_E_)_or_ex_F_being_Subset_of_Y_st_
(_F_is_closed_&_not_x_in_F_&_y_in_F_)_)
percases ( ex E0 being Subset of Y0 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is closed & not x0 in F0 & y0 in F0 ) ) by A1, A2, A3, Def4;
suppose ex E0 being Subset of Y0 st
( E0 is closed & x0 in E0 & not y0 in E0 ) ; ::_thesis: ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
then consider E0 being Subset of Y0 such that
A4: E0 is closed and
A5: x0 in E0 and
A6: not y0 in E0 ;
now__::_thesis:_ex_E_being_Subset_of_Y_st_
(_E_is_closed_&_x_in_E_&_not_y_in_E_)
consider E being Subset of Y such that
A7: E is closed and
A8: E0 = E /\ A by A4, Def2;
take E = E; ::_thesis: ( E is closed & x in E & not y in E )
thus E is closed by A7; ::_thesis: ( x in E & not y in E )
E /\ A c= E by XBOOLE_1:17;
hence x in E by A5, A8; ::_thesis: not y in E
thus not y in E by A2, A6, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ; ::_thesis: verum
end;
suppose ex F0 being Subset of Y0 st
( F0 is closed & not x0 in F0 & y0 in F0 ) ; ::_thesis: ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
then consider F0 being Subset of Y0 such that
A9: F0 is closed and
A10: not x0 in F0 and
A11: y0 in F0 ;
now__::_thesis:_ex_F_being_Subset_of_Y_st_
(_F_is_closed_&_not_x_in_F_&_y_in_F_)
consider F being Subset of Y such that
A12: F is closed and
A13: F0 = F /\ A by A9, Def2;
take F = F; ::_thesis: ( F is closed & not x in F & y in F )
thus F is closed by A12; ::_thesis: ( not x in F & y in F )
thus not x in F by A2, A10, A13, XBOOLE_0:def_4; ::_thesis: y in F
F /\ A c= F by XBOOLE_1:17;
hence y in F by A11, A13; ::_thesis: verum
end;
hence ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ; ::_thesis: verum
end;
end;
end;
hence ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ; ::_thesis: verum
end;
end;
assume A14: ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ; ::_thesis: Y0 is T_0
now__::_thesis:_(_not_Y0_is_empty_implies_for_x0,_y0_being_Point_of_Y0_holds_
(_not_x0_<>_y0_or_ex_E0_being_Subset_of_Y0_st_
(_E0_is_closed_&_x0_in_E0_&_not_y0_in_E0_)_or_ex_F0_being_Subset_of_Y0_st_
(_F0_is_closed_&_not_x0_in_F0_&_y0_in_F0_)_)_)
A15: the carrier of Y0 c= the carrier of Y by Def1;
assume A16: not Y0 is empty ; ::_thesis: for x0, y0 being Point of Y0 holds
( not x0 <> y0 or ex E0 being Subset of Y0 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is closed & not x0 in F0 & y0 in F0 ) )
let x0, y0 be Point of Y0; ::_thesis: ( not x0 <> y0 or ex E0 being Subset of Y0 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is closed & not x0 in F0 & y0 in F0 ) )
the carrier of Y0 <> {} by A16;
then ( x0 in the carrier of Y0 & y0 in the carrier of Y0 ) ;
then reconsider x = x0, y = y0 as Point of Y by A15;
assume A17: x0 <> y0 ; ::_thesis: ( ex E0 being Subset of Y0 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is closed & not x0 in F0 & y0 in F0 ) )
now__::_thesis:_(_ex_E0_being_Subset_of_Y0_st_
(_E0_is_closed_&_x0_in_E0_&_not_y0_in_E0_)_or_ex_F0_being_Subset_of_Y0_st_
(_F0_is_closed_&_not_x0_in_F0_&_y0_in_F0_)_)
percases ( ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) by A14, A16, A17;
suppose ex E being Subset of Y st
( E is closed & x in E & not y in E ) ; ::_thesis: ( ex E0 being Subset of Y0 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is closed & not x0 in F0 & y0 in F0 ) )
then consider E being Subset of Y such that
A18: E is closed and
A19: x in E and
A20: not y in E ;
now__::_thesis:_ex_E0_being_Subset_of_Y0_st_
(_E0_is_closed_&_x0_in_E0_&_not_y0_in_E0_)
consider E0 being Subset of Y0 such that
A21: E0 is closed and
A22: E0 = E /\ A by A18, Th2;
take E0 = E0; ::_thesis: ( E0 is closed & x0 in E0 & not y0 in E0 )
thus E0 is closed by A21; ::_thesis: ( x0 in E0 & not y0 in E0 )
thus x0 in E0 by A16, A19, A22, XBOOLE_0:def_4; ::_thesis: not y0 in E0
now__::_thesis:_not_y0_in_E0
A23: E /\ A c= E by XBOOLE_1:17;
assume y0 in E0 ; ::_thesis: contradiction
hence contradiction by A20, A22, A23; ::_thesis: verum
end;
hence not y0 in E0 ; ::_thesis: verum
end;
hence ( ex E0 being Subset of Y0 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is closed & not x0 in F0 & y0 in F0 ) ) ; ::_thesis: verum
end;
suppose ex F being Subset of Y st
( F is closed & not x in F & y in F ) ; ::_thesis: ( ex E0 being Subset of Y0 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is closed & not x0 in F0 & y0 in F0 ) )
then consider F being Subset of Y such that
A24: F is closed and
A25: not x in F and
A26: y in F ;
now__::_thesis:_ex_F0_being_Subset_of_Y0_st_
(_F0_is_closed_&_not_x0_in_F0_&_y0_in_F0_)
consider F0 being Subset of Y0 such that
A27: F0 is closed and
A28: F0 = F /\ A by A24, Th2;
take F0 = F0; ::_thesis: ( F0 is closed & not x0 in F0 & y0 in F0 )
thus F0 is closed by A27; ::_thesis: ( not x0 in F0 & y0 in F0 )
now__::_thesis:_not_x0_in_F0
A29: F /\ A c= F by XBOOLE_1:17;
assume x0 in F0 ; ::_thesis: contradiction
hence contradiction by A25, A28, A29; ::_thesis: verum
end;
hence not x0 in F0 ; ::_thesis: y0 in F0
thus y0 in F0 by A16, A26, A28, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( ex E0 being Subset of Y0 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is closed & not x0 in F0 & y0 in F0 ) ) ; ::_thesis: verum
end;
end;
end;
hence ( ex E0 being Subset of Y0 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is closed & not x0 in F0 & y0 in F0 ) ) ; ::_thesis: verum
end;
hence Y0 is T_0 by Def4; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines T_0 TSP_1:def_14_:_
for Y being TopStruct
for Y0 being SubSpace of Y holds
( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) );
theorem Th13: :: TSP_1:13
for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is T_0 iff Y0 is V138() )
proof
let Y be non empty TopStruct ; ::_thesis: for Y0 being non empty SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is T_0 iff Y0 is V138() )
let Y0 be non empty SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 holds
( A is T_0 iff Y0 is V138() )
let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 implies ( A is T_0 iff Y0 is V138() ) )
assume A1: A = the carrier of Y0 ; ::_thesis: ( A is T_0 iff Y0 is V138() )
hereby ::_thesis: ( Y0 is V138() implies A is T_0 )
assume A is T_0 ; ::_thesis: Y0 is V138()
then for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) by A1, Def9;
hence Y0 is V138() by Def14; ::_thesis: verum
end;
hereby ::_thesis: verum
assume Y0 is V138() ; ::_thesis: A is T_0
then for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) by A1, Def14;
hence A is T_0 by Def9; ::_thesis: verum
end;
end;
theorem :: TSP_1:14
for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for Y1 being non empty V138() SubSpace of Y st Y0 is SubSpace of Y1 holds
Y0 is V138()
proof
let Y be non empty TopStruct ; ::_thesis: for Y0 being non empty SubSpace of Y
for Y1 being non empty V138() SubSpace of Y st Y0 is SubSpace of Y1 holds
Y0 is V138()
let Y0 be non empty SubSpace of Y; ::_thesis: for Y1 being non empty V138() SubSpace of Y st Y0 is SubSpace of Y1 holds
Y0 is V138()
let Y1 be non empty V138() SubSpace of Y; ::_thesis: ( Y0 is SubSpace of Y1 implies Y0 is V138() )
reconsider A1 = the carrier of Y1, A0 = the carrier of Y0 as non empty Subset of Y by Lm3;
assume A1: Y0 is SubSpace of Y1 ; ::_thesis: Y0 is V138()
A2: A1 is T_0 by Th13;
( [#] Y0 = A0 & [#] Y1 = A1 ) ;
then A0 c= A1 by A1, PRE_TOPC:def_4;
then A0 is T_0 by A2, Th5;
hence Y0 is V138() by Th13; ::_thesis: verum
end;
theorem :: TSP_1:15
for X being non empty TopSpace
for X1 being non empty V138() SubSpace of X
for X2 being non empty SubSpace of X st X1 meets X2 holds
X1 meet X2 is V138()
proof
let X be non empty TopSpace; ::_thesis: for X1 being non empty V138() SubSpace of X
for X2 being non empty SubSpace of X st X1 meets X2 holds
X1 meet X2 is V138()
let X1 be non empty V138() SubSpace of X; ::_thesis: for X2 being non empty SubSpace of X st X1 meets X2 holds
X1 meet X2 is V138()
let X2 be non empty SubSpace of X; ::_thesis: ( X1 meets X2 implies X1 meet X2 is V138() )
reconsider A1 = the carrier of X1 as non empty Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as non empty Subset of X by TSEP_1:1;
assume X1 meets X2 ; ::_thesis: X1 meet X2 is V138()
then A1: the carrier of (X1 meet X2) = A1 /\ A2 by TSEP_1:def_4;
A1 is T_0 by Th13;
then A1 /\ A2 is T_0 by Th6;
hence X1 meet X2 is V138() by A1, Th13; ::_thesis: verum
end;
theorem :: TSP_1:16
for X being non empty TopSpace
for X1, X2 being non empty V138() SubSpace of X st ( X1 is open or X2 is open ) holds
X1 union X2 is V138()
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty V138() SubSpace of X st ( X1 is open or X2 is open ) holds
X1 union X2 is V138()
let X1, X2 be non empty V138() SubSpace of X; ::_thesis: ( ( X1 is open or X2 is open ) implies X1 union X2 is V138() )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as non empty Subset of X by TSEP_1:1;
assume ( X1 is open or X2 is open ) ; ::_thesis: X1 union X2 is V138()
then A1: ( A1 is open or A2 is open ) by TSEP_1:16;
( A1 is T_0 & A2 is T_0 ) by Th13;
then ( the carrier of (X1 union X2) = A1 \/ A2 & A1 \/ A2 is T_0 ) by A1, Th7, TSEP_1:def_2;
hence X1 union X2 is V138() by Th13; ::_thesis: verum
end;
theorem :: TSP_1:17
for X being non empty TopSpace
for X1, X2 being non empty V138() SubSpace of X st ( X1 is closed or X2 is closed ) holds
X1 union X2 is V138()
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty V138() SubSpace of X st ( X1 is closed or X2 is closed ) holds
X1 union X2 is V138()
let X1, X2 be non empty V138() SubSpace of X; ::_thesis: ( ( X1 is closed or X2 is closed ) implies X1 union X2 is V138() )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as non empty Subset of X by TSEP_1:1;
assume ( X1 is closed or X2 is closed ) ; ::_thesis: X1 union X2 is V138()
then A1: ( A1 is closed or A2 is closed ) by TSEP_1:11;
( A1 is T_0 & A2 is T_0 ) by Th13;
then ( the carrier of (X1 union X2) = A1 \/ A2 & A1 \/ A2 is T_0 ) by A1, Th8, TSEP_1:def_2;
hence X1 union X2 is V138() by Th13; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
mode Kolmogorov_subspace of X is non empty V138() SubSpace of X;
end;
theorem :: TSP_1:18
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is T_0 holds
ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is T_0 holds
ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is T_0 implies ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0 )
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A0 is T_0 ; ::_thesis: ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0
then reconsider X0 = X0 as strict Kolmogorov_subspace of X by A1, Th13;
take X0 ; ::_thesis: A0 = the carrier of X0
thus A0 = the carrier of X0 by A1; ::_thesis: verum
end;
registration
let X be non trivial TopSpace;
cluster non empty strict T_0 proper for SubSpace of X;
existence
ex b1 being Kolmogorov_subspace of X st
( b1 is proper & b1 is strict )
proof
set X0 = the non empty trivial strict SubSpace of X;
take the non empty trivial strict SubSpace of X ; ::_thesis: ( the non empty trivial strict SubSpace of X is proper & the non empty trivial strict SubSpace of X is strict )
thus ( the non empty trivial strict SubSpace of X is proper & the non empty trivial strict SubSpace of X is strict ) ; ::_thesis: verum
end;
end;
registration
let X be Kolmogorov_space;
cluster non empty -> non empty V138() for SubSpace of X;
coherence
for b1 being non empty SubSpace of X holds b1 is V138()
proof
let X0 be non empty SubSpace of X; ::_thesis: X0 is V138()
reconsider A0 = the carrier of X0 as non empty Subset of X by TSEP_1:1;
X is SubSpace of X by TSEP_1:2;
then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1;
A is T_0 by Th4;
then A0 is T_0 by Th5;
hence X0 is V138() by Th13; ::_thesis: verum
end;
end;
registration
let X be non-Kolmogorov_space;
cluster non empty non proper -> non empty V138() for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is proper holds
not b1 is V138()
proof
let X0 be non empty SubSpace of X; ::_thesis: ( not X0 is proper implies not X0 is V138() )
reconsider A0 = the carrier of X0 as non empty Subset of X by TSEP_1:1;
X is SubSpace of X by TSEP_1:2;
then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1;
assume not X0 is proper ; ::_thesis: X0 is V138()
then not A0 is proper by TEX_2:8;
then A0 = A by SUBSET_1:def_6;
then not A0 is T_0 by Th4;
hence X0 is V138() by Th13; ::_thesis: verum
end;
cluster non empty V138() -> non empty proper for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is V138() holds
b1 is proper ;
end;
registration
let X be non-Kolmogorov_space;
cluster strict V138() for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is strict & b1 is V138() )
proof
set X0 = the non empty strict non proper SubSpace of X;
take the non empty strict non proper SubSpace of X ; ::_thesis: ( the non empty strict non proper SubSpace of X is strict & the non empty strict non proper SubSpace of X is V138() )
thus ( the non empty strict non proper SubSpace of X is strict & the non empty strict non proper SubSpace of X is V138() ) ; ::_thesis: verum
end;
end;
definition
let X be non-Kolmogorov_space;
mode non-Kolmogorov_subspace of X is V138() SubSpace of X;
end;
theorem :: TSP_1:19
for X being non-Kolmogorov_space
for A0 being Subset of X st not A0 is T_0 holds
ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0
proof
let X be non-Kolmogorov_space; ::_thesis: for A0 being Subset of X st not A0 is T_0 holds
ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0
let A0 be Subset of X; ::_thesis: ( not A0 is T_0 implies ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0 )
assume A1: not A0 is T_0 ; ::_thesis: ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0
then not A0 is empty by Th11;
then consider X0 being non empty strict SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
reconsider X0 = X0 as strict V138() SubSpace of X by A1, A2, Th13;
take X0 ; ::_thesis: A0 = the carrier of X0
thus A0 = the carrier of X0 by A2; ::_thesis: verum
end;