:: TSP_2 semantic presentation
begin
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :Def1: :: TSP_2:def 1
for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b;
compatibility
( A is T_0 iff for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b )
proof
thus ( A is T_0 implies for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b ) ::_thesis: ( ( for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b ) implies A is T_0 )
proof
assume A1: A is T_0 ; ::_thesis: for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b
let a, b be Point of X; ::_thesis: ( a in A & b in A & a <> b implies MaxADSet a misses MaxADSet b )
assume that
A2: a in A and
A3: b in A ; ::_thesis: ( not a <> b or MaxADSet a misses MaxADSet b )
assume A4: a <> b ; ::_thesis: MaxADSet a misses MaxADSet b
now__::_thesis:_(_ex_V_being_Subset_of_X_st_
(_V_is_open_&_MaxADSet_a_c=_V_&_V_misses_MaxADSet_b_)_or_ex_W_being_Subset_of_X_st_
(_W_is_open_&_W_misses_MaxADSet_a_&_MaxADSet_b_c=_W_)_)
percases ( ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) ) by A1, A2, A3, A4, TSP_1:def_8;
suppose ex V being Subset of X st
( V is open & a in V & not b in V ) ; ::_thesis: ( ex V being Subset of X st
( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st
( W is open & W misses MaxADSet a & MaxADSet b c= W ) )
then consider V being Subset of X such that
A5: V is open and
A6: a in V and
A7: not b in V ;
now__::_thesis:_ex_V_being_Subset_of_X_st_
(_V_is_open_&_MaxADSet_a_c=_V_&_V_misses_MaxADSet_b_)
take V = V; ::_thesis: ( V is open & MaxADSet a c= V & V misses MaxADSet b )
thus V is open by A5; ::_thesis: ( MaxADSet a c= V & V misses MaxADSet b )
thus MaxADSet a c= V by A5, A6, TEX_4:24; ::_thesis: V misses MaxADSet b
b in ([#] X) \ V by A7, XBOOLE_0:def_5;
then MaxADSet b c= V ` by A5, TEX_4:23;
hence V misses MaxADSet b by SUBSET_1:23; ::_thesis: verum
end;
hence ( ex V being Subset of X st
( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st
( W is open & W misses MaxADSet a & MaxADSet b c= W ) ) ; ::_thesis: verum
end;
suppose ex W being Subset of X st
( W is open & not a in W & b in W ) ; ::_thesis: ( ex V being Subset of X st
( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st
( W is open & W misses MaxADSet a & MaxADSet b c= W ) )
then consider W being Subset of X such that
A8: W is open and
A9: not a in W and
A10: b in W ;
now__::_thesis:_ex_W_being_Subset_of_X_st_
(_W_is_open_&_W_misses_MaxADSet_a_&_MaxADSet_b_c=_W_)
take W = W; ::_thesis: ( W is open & W misses MaxADSet a & MaxADSet b c= W )
thus W is open by A8; ::_thesis: ( W misses MaxADSet a & MaxADSet b c= W )
a in ([#] X) \ W by A9, XBOOLE_0:def_5;
then MaxADSet a c= W ` by A8, TEX_4:23;
hence W misses MaxADSet a by SUBSET_1:23; ::_thesis: MaxADSet b c= W
thus MaxADSet b c= W by A8, A10, TEX_4:24; ::_thesis: verum
end;
hence ( ex V being Subset of X st
( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st
( W is open & W misses MaxADSet a & MaxADSet b c= W ) ) ; ::_thesis: verum
end;
end;
end;
hence MaxADSet a misses MaxADSet b by TEX_4:53; ::_thesis: verum
end;
assume A11: for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b ; ::_thesis: A is T_0
now__::_thesis:_for_a,_b_being_Point_of_X_st_a_in_A_&_b_in_A_&_a_<>_b_&_(_for_V_being_Subset_of_X_holds_
(_not_V_is_open_or_not_a_in_V_or_b_in_V_)_)_holds_
ex_W_being_Subset_of_X_st_
(_W_is_open_&_not_a_in_W_&_b_in_W_)
let a, b be Point of X; ::_thesis: ( a in A & b in A & a <> b & ( for V being Subset of X holds
( not V is open or not a in V or b in V ) ) implies ex W being Subset of X st
( W is open & not a in W & b in W ) )
assume that
A12: a in A and
A13: b in A ; ::_thesis: ( not a <> b or ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) )
assume a <> b ; ::_thesis: ( ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) )
then A14: MaxADSet a misses MaxADSet b by A11, A12, A13;
now__::_thesis:_(_ex_V_being_Subset_of_X_st_
(_V_is_open_&_a_in_V_&_not_b_in_V_)_or_ex_W_being_Subset_of_X_st_
(_W_is_open_&_not_a_in_W_&_b_in_W_)_)
percases ( ex V being Subset of X st
( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st
( W is open & W misses MaxADSet a & MaxADSet b c= W ) ) by A14, TEX_4:53;
suppose ex V being Subset of X st
( V is open & MaxADSet a c= V & V misses MaxADSet b ) ; ::_thesis: ( ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) )
then consider V being Subset of X such that
A15: V is open and
A16: MaxADSet a c= V and
A17: V misses MaxADSet b ;
now__::_thesis:_ex_V_being_Subset_of_X_st_
(_V_is_open_&_a_in_V_&_not_b_in_V_)
take V = V; ::_thesis: ( V is open & a in V & not b in V )
thus V is open by A15; ::_thesis: ( a in V & not b in V )
{a} c= MaxADSet a by TEX_4:18;
then a in MaxADSet a by ZFMISC_1:31;
hence a in V by A16; ::_thesis: not b in V
now__::_thesis:_not_b_in_V
{b} c= MaxADSet b by TEX_4:18;
then A18: b in MaxADSet b by ZFMISC_1:31;
assume b in V ; ::_thesis: contradiction
hence contradiction by A17, A18, XBOOLE_0:3; ::_thesis: verum
end;
hence not b in V ; ::_thesis: verum
end;
hence ( ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) ) ; ::_thesis: verum
end;
suppose ex W being Subset of X st
( W is open & W misses MaxADSet a & MaxADSet b c= W ) ; ::_thesis: ( ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) )
then consider W being Subset of X such that
A19: W is open and
A20: W misses MaxADSet a and
A21: MaxADSet b c= W ;
now__::_thesis:_ex_W_being_Subset_of_X_st_
(_W_is_open_&_not_a_in_W_&_b_in_W_)
take W = W; ::_thesis: ( W is open & not a in W & b in W )
thus W is open by A19; ::_thesis: ( not a in W & b in W )
now__::_thesis:_not_a_in_W
{a} c= MaxADSet a by TEX_4:18;
then A22: a in MaxADSet a by ZFMISC_1:31;
assume a in W ; ::_thesis: contradiction
hence contradiction by A20, A22, XBOOLE_0:3; ::_thesis: verum
end;
hence not a in W ; ::_thesis: b in W
{b} c= MaxADSet b by TEX_4:18;
then b in MaxADSet b by ZFMISC_1:31;
hence b in W by A21; ::_thesis: verum
end;
hence ( ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) ) ; ::_thesis: verum
end;
end;
end;
hence ( ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) ) ; ::_thesis: verum
end;
hence A is T_0 by TSP_1:def_8; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines T_0 TSP_2:def_1_:_
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b );
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :Def2: :: TSP_2:def 2
for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a};
compatibility
( A is T_0 iff for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} )
proof
thus ( A is T_0 implies for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} ) ::_thesis: ( ( for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} ) implies A is T_0 )
proof
assume A1: A is T_0 ; ::_thesis: for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a}
let a be Point of X; ::_thesis: ( a in A implies A /\ (MaxADSet a) = {a} )
assume A2: a in A ; ::_thesis: A /\ (MaxADSet a) = {a}
assume A3: A /\ (MaxADSet a) <> {a} ; ::_thesis: contradiction
{a} c= MaxADSet a by TEX_4:18;
then a in MaxADSet a by ZFMISC_1:31;
then a in A /\ (MaxADSet a) by A2, XBOOLE_0:def_4;
then consider b being set such that
A4: b in A /\ (MaxADSet a) and
A5: b <> a by A3, ZFMISC_1:35;
reconsider b = b as Point of X by A4;
b in A by A4, XBOOLE_0:def_4;
then A6: MaxADSet a misses MaxADSet b by A1, A2, A5, Def1;
b in MaxADSet a by A4, XBOOLE_0:def_4;
hence contradiction by A6, TEX_4:21; ::_thesis: verum
end;
assume A7: for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} ; ::_thesis: A is T_0
now__::_thesis:_for_a,_b_being_Point_of_X_st_a_in_A_&_b_in_A_&_a_<>_b_holds_
not_MaxADSet_a_meets_MaxADSet_b
let a, b be Point of X; ::_thesis: ( a in A & b in A & a <> b implies not MaxADSet a meets MaxADSet b )
assume that
A8: a in A and
A9: b in A ; ::_thesis: ( a <> b implies not MaxADSet a meets MaxADSet b )
A10: A /\ (MaxADSet a) = {a} by A7, A8;
A11: A /\ (MaxADSet b) = {b} by A7, A9;
assume A12: a <> b ; ::_thesis: not MaxADSet a meets MaxADSet b
assume MaxADSet a meets MaxADSet b ; ::_thesis: contradiction
then {a} = {b} by A10, A11, TEX_4:22;
hence contradiction by A12, ZFMISC_1:3; ::_thesis: verum
end;
hence A is T_0 by Def1; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines T_0 TSP_2:def_2_:_
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} );
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :: TSP_2:def 3
for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} );
compatibility
( A is T_0 iff for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} ) )
proof
thus ( A is T_0 implies for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} ) ) ::_thesis: ( ( for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} ) ) implies A is T_0 )
proof
assume A1: A is T_0 ; ::_thesis: for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} )
let a be Point of X; ::_thesis: ( a in A implies ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} ) )
assume A2: a in A ; ::_thesis: ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} )
take D = MaxADSet a; ::_thesis: ( D is maximal_anti-discrete & A /\ D = {a} )
thus D is maximal_anti-discrete by TEX_4:20; ::_thesis: A /\ D = {a}
thus A /\ D = {a} by A1, A2, Def2; ::_thesis: verum
end;
assume A3: for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} ) ; ::_thesis: A is T_0
now__::_thesis:_for_a_being_Point_of_X_st_a_in_A_holds_
A_/\_(MaxADSet_a)_=_{a}
let a be Point of X; ::_thesis: ( a in A implies A /\ (MaxADSet a) = {a} )
assume a in A ; ::_thesis: A /\ (MaxADSet a) = {a}
then consider D being Subset of X such that
A4: D is maximal_anti-discrete and
A5: A /\ D = {a} by A3;
a in A /\ D by A5, ZFMISC_1:31;
then a in D by XBOOLE_0:def_4;
hence A /\ (MaxADSet a) = {a} by A4, A5, TEX_4:27; ::_thesis: verum
end;
hence A is T_0 by Def2; ::_thesis: verum
end;
end;
:: deftheorem defines T_0 TSP_2:def_3_:_
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} ) );
definition
let Y be TopStruct ;
let IT be Subset of Y;
attrIT is maximal_T_0 means :Def4: :: TSP_2:def 4
( IT is T_0 & ( for D being Subset of Y st D is T_0 & IT c= D holds
IT = D ) );
end;
:: deftheorem Def4 defines maximal_T_0 TSP_2:def_4_:_
for Y being TopStruct
for IT being Subset of Y holds
( IT is maximal_T_0 iff ( IT is T_0 & ( for D being Subset of Y st D is T_0 & IT c= D holds
IT = D ) ) );
theorem :: TSP_2:1
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 maximal_T_0 holds
D1 is maximal_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 maximal_T_0 holds
D1 is maximal_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 maximal_T_0 holds
D1 is maximal_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 maximal_T_0 implies D1 is maximal_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 maximal_T_0 or D1 is maximal_T_0 )
assume A2: D0 = D1 ; ::_thesis: ( not D0 is maximal_T_0 or D1 is maximal_T_0 )
assume A3: D0 is maximal_T_0 ; ::_thesis: D1 is maximal_T_0
A4: now__::_thesis:_for_D_being_Subset_of_Y1_st_D_is_T_0_&_D1_c=_D_holds_
D1_=_D
let D be Subset of Y1; ::_thesis: ( D is T_0 & D1 c= D implies D1 = D )
reconsider E = D as Subset of Y0 by A1;
assume D is T_0 ; ::_thesis: ( D1 c= D implies D1 = D )
then A5: E is T_0 by A1, TSP_1:3;
assume D1 c= D ; ::_thesis: D1 = D
hence D1 = D by A2, A3, A5, Def4; ::_thesis: verum
end;
D0 is T_0 by A3, Def4;
then D1 is T_0 by A1, A2, TSP_1:3;
hence D1 is maximal_T_0 by A4, Def4; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
let M be Subset of X;
redefine attr M is maximal_T_0 means :Def5: :: TSP_2:def 5
( M is T_0 & MaxADSet M = the carrier of X );
compatibility
( M is maximal_T_0 iff ( M is T_0 & MaxADSet M = the carrier of X ) )
proof
thus ( M is maximal_T_0 implies ( M is T_0 & MaxADSet M = the carrier of X ) ) ::_thesis: ( M is T_0 & MaxADSet M = the carrier of X implies M is maximal_T_0 )
proof
assume A1: M is maximal_T_0 ; ::_thesis: ( M is T_0 & MaxADSet M = the carrier of X )
hence A2: M is T_0 by Def4; ::_thesis: MaxADSet M = the carrier of X
the carrier of X c= MaxADSet M
proof
assume not the carrier of X c= MaxADSet M ; ::_thesis: contradiction
then consider x being set such that
A3: x in the carrier of X and
A4: not x in MaxADSet M by TARSKI:def_3;
reconsider x = x as Point of X by A3;
set A = M \/ {x};
for a being Point of X st a in M \/ {x} holds
(M \/ {x}) /\ (MaxADSet a) = {a}
proof
let a be Point of X; ::_thesis: ( a in M \/ {x} implies (M \/ {x}) /\ (MaxADSet a) = {a} )
assume a in M \/ {x} ; ::_thesis: (M \/ {x}) /\ (MaxADSet a) = {a}
then A5: ( a in M or a in {x} ) by XBOOLE_0:def_3;
now__::_thesis:_(M_\/_{x})_/\_(MaxADSet_a)_=_{a}
percases ( a in M or a = x ) by A5, TARSKI:def_1;
supposeA6: a in M ; ::_thesis: (M \/ {x}) /\ (MaxADSet a) = {a}
{x} /\ (MaxADSet a) = {}
proof
assume {x} /\ (MaxADSet a) <> {} ; ::_thesis: contradiction
then {x} meets MaxADSet a by XBOOLE_0:def_7;
then A7: x in MaxADSet a by ZFMISC_1:50;
{a} c= M by A6, ZFMISC_1:31;
then MaxADSet {a} c= MaxADSet M by TEX_4:31;
then MaxADSet a c= MaxADSet M by TEX_4:28;
hence contradiction by A4, A7; ::_thesis: verum
end;
then (M \/ {x}) /\ (MaxADSet a) = (M /\ (MaxADSet a)) \/ {} by XBOOLE_1:23
.= M /\ (MaxADSet a) ;
hence (M \/ {x}) /\ (MaxADSet a) = {a} by A2, A6, Def2; ::_thesis: verum
end;
supposeA8: a = x ; ::_thesis: (M \/ {x}) /\ (MaxADSet a) = {a}
then A9: {x} c= MaxADSet a by TEX_4:18;
M /\ (MaxADSet a) = {}
proof
A10: M c= MaxADSet M by TEX_4:32;
assume M /\ (MaxADSet a) <> {} ; ::_thesis: contradiction
then (MaxADSet a) /\ (MaxADSet M) <> {} by A10, XBOOLE_1:3, XBOOLE_1:26;
then MaxADSet a meets MaxADSet M by XBOOLE_0:def_7;
then A11: MaxADSet a c= MaxADSet M by TEX_4:30;
x in MaxADSet a by A9, ZFMISC_1:31;
hence contradiction by A4, A11; ::_thesis: verum
end;
then (M \/ {x}) /\ (MaxADSet a) = {} \/ ({x} /\ (MaxADSet a)) by XBOOLE_1:23
.= {x} /\ (MaxADSet a) ;
hence (M \/ {x}) /\ (MaxADSet a) = {a} by A8, TEX_4:18, XBOOLE_1:28; ::_thesis: verum
end;
end;
end;
hence (M \/ {x}) /\ (MaxADSet a) = {a} ; ::_thesis: verum
end;
then A12: M \/ {x} is T_0 by Def2;
A13: M c= MaxADSet M by TEX_4:32;
A14: {x} c= M \/ {x} by XBOOLE_1:7;
M c= M \/ {x} by XBOOLE_1:7;
then M = M \/ {x} by A1, A12, Def4;
then x in M by A14, ZFMISC_1:31;
hence contradiction by A4, A13; ::_thesis: verum
end;
hence MaxADSet M = the carrier of X by XBOOLE_0:def_10; ::_thesis: verum
end;
assume A15: M is T_0 ; ::_thesis: ( not MaxADSet M = the carrier of X or M is maximal_T_0 )
assume A16: MaxADSet M = the carrier of X ; ::_thesis: M is maximal_T_0
for D being Subset of X st D is T_0 & M c= D holds
M = D
proof
let D be Subset of X; ::_thesis: ( D is T_0 & M c= D implies M = D )
assume A17: D is T_0 ; ::_thesis: ( not M c= D or M = D )
assume A18: M c= D ; ::_thesis: M = D
D c= M
proof
assume not D c= M ; ::_thesis: contradiction
then consider x being set such that
A19: x in D and
A20: not x in M by TARSKI:def_3;
A21: x in the carrier of X by A19;
reconsider x = x as Point of X by A19;
x in union { (MaxADSet a) where a is Point of X : a in M } by A16, A21, TEX_4:def_11;
then consider C being set such that
A22: x in C and
A23: C in { (MaxADSet a) where a is Point of X : a in M } by TARSKI:def_4;
consider a being Point of X such that
A24: C = MaxADSet a and
A25: a in M by A23;
M /\ (MaxADSet x) c= D /\ (MaxADSet x) by A18, XBOOLE_1:26;
then A26: M /\ (MaxADSet x) c= {x} by A17, A19, Def2;
MaxADSet a = MaxADSet x by A22, A24, TEX_4:21;
then M /\ (MaxADSet x) = {a} by A15, A25, Def2;
hence contradiction by A20, A25, A26, ZFMISC_1:18; ::_thesis: verum
end;
hence M = D by A18, XBOOLE_0:def_10; ::_thesis: verum
end;
hence M is maximal_T_0 by A15, Def4; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines maximal_T_0 TSP_2:def_5_:_
for X being non empty TopSpace
for M being Subset of X holds
( M is maximal_T_0 iff ( M is T_0 & MaxADSet M = the carrier of X ) );
theorem Th2: :: TSP_2:2
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
M is dense
proof
let X be non empty TopSpace; ::_thesis: for M being Subset of X st M is maximal_T_0 holds
M is dense
let M be Subset of X; ::_thesis: ( M is maximal_T_0 implies M is dense )
assume A1: M is maximal_T_0 ; ::_thesis: M is dense
then MaxADSet M = [#] X by Def5;
then A2: Cl (MaxADSet M) = MaxADSet M by PRE_TOPC:22;
MaxADSet M = the carrier of X by A1, Def5;
then Cl M = the carrier of X by A2, TEX_4:62;
hence M is dense by TOPS_3:def_2; ::_thesis: verum
end;
theorem Th3: :: TSP_2:3
for X being non empty TopSpace
for A being Subset of X st ( A is open or A is closed ) & A is maximal_T_0 holds
not A is proper
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st ( A is open or A is closed ) & A is maximal_T_0 holds
not A is proper
let A be Subset of X; ::_thesis: ( ( A is open or A is closed ) & A is maximal_T_0 implies not A is proper )
assume ( A is open or A is closed ) ; ::_thesis: ( not A is maximal_T_0 or not A is proper )
then A1: A = MaxADSet A by TEX_4:56, TEX_4:60;
assume A is maximal_T_0 ; ::_thesis: not A is proper
then A = the carrier of X by A1, Def5;
hence not A is proper by SUBSET_1:def_6; ::_thesis: verum
end;
theorem Th4: :: TSP_2:4
for X being non empty TopSpace
for A being empty Subset of X holds not A is maximal_T_0
proof
let X be non empty TopSpace; ::_thesis: for A being empty Subset of X holds not A is maximal_T_0
consider a being set such that
A1: a in the carrier of X by XBOOLE_0:def_1;
reconsider a = a as Point of X by A1;
let A be empty Subset of X; ::_thesis: not A is maximal_T_0
now__::_thesis:_ex_C_being_Element_of_bool_the_carrier_of_X_st_
(_C_is_T_0_&_A_c=_C_&_A_<>_C_)
take C = {a}; ::_thesis: ( C is T_0 & A c= C & A <> C )
thus ( C is T_0 & A c= C & A <> C ) by TSP_1:12, XBOOLE_1:2; ::_thesis: verum
end;
hence not A is maximal_T_0 by Def4; ::_thesis: verum
end;
theorem Th5: :: TSP_2:5
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X st A is closed holds
A = MaxADSet (M /\ A)
proof
let X be non empty TopSpace; ::_thesis: for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X st A is closed holds
A = MaxADSet (M /\ A)
let M be Subset of X; ::_thesis: ( M is maximal_T_0 implies for A being Subset of X st A is closed holds
A = MaxADSet (M /\ A) )
assume A1: M is maximal_T_0 ; ::_thesis: for A being Subset of X st A is closed holds
A = MaxADSet (M /\ A)
let A be Subset of X; ::_thesis: ( A is closed implies A = MaxADSet (M /\ A) )
assume A2: A is closed ; ::_thesis: A = MaxADSet (M /\ A)
then MaxADSet (M /\ A) = (MaxADSet M) /\ (MaxADSet A) by TEX_4:64;
then A3: MaxADSet (M /\ A) = (MaxADSet M) /\ A by A2, TEX_4:60;
A = the carrier of X /\ A by XBOOLE_1:28;
hence A = MaxADSet (M /\ A) by A1, A3, Def5; ::_thesis: verum
end;
theorem Th6: :: TSP_2:6
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X st A is open holds
A = MaxADSet (M /\ A)
proof
let X be non empty TopSpace; ::_thesis: for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X st A is open holds
A = MaxADSet (M /\ A)
let M be Subset of X; ::_thesis: ( M is maximal_T_0 implies for A being Subset of X st A is open holds
A = MaxADSet (M /\ A) )
assume A1: M is maximal_T_0 ; ::_thesis: for A being Subset of X st A is open holds
A = MaxADSet (M /\ A)
let A be Subset of X; ::_thesis: ( A is open implies A = MaxADSet (M /\ A) )
assume A2: A is open ; ::_thesis: A = MaxADSet (M /\ A)
then MaxADSet (M /\ A) = (MaxADSet M) /\ (MaxADSet A) by TEX_4:65;
then A3: MaxADSet (M /\ A) = (MaxADSet M) /\ A by A2, TEX_4:56;
A = the carrier of X /\ A by XBOOLE_1:28;
hence A = MaxADSet (M /\ A) by A1, A3, Def5; ::_thesis: verum
end;
theorem :: TSP_2:7
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X holds Cl A = MaxADSet (M /\ (Cl A)) by Th5;
theorem :: TSP_2:8
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X holds Int A = MaxADSet (M /\ (Int A)) by Th6;
definition
let X be non empty TopSpace;
let M be Subset of X;
redefine attr M is maximal_T_0 means :Def6: :: TSP_2:def 6
for x being Point of X ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} );
compatibility
( M is maximal_T_0 iff for x being Point of X ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} ) )
proof
thus ( M is maximal_T_0 implies for x being Point of X ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} ) ) ::_thesis: ( ( for x being Point of X ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} ) ) implies M is maximal_T_0 )
proof
assume A1: M is maximal_T_0 ; ::_thesis: for x being Point of X ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} )
then A2: M is T_0 by Def4;
let x be Point of X; ::_thesis: ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} )
x in the carrier of X ;
then x in MaxADSet M by A1, Def5;
then x in union { (MaxADSet a) where a is Point of X : a in M } by TEX_4:def_11;
then consider C being set such that
A3: x in C and
A4: C in { (MaxADSet a) where a is Point of X : a in M } by TARSKI:def_4;
consider a being Point of X such that
A5: C = MaxADSet a and
A6: a in M by A4;
MaxADSet a = MaxADSet x by A3, A5, TEX_4:21;
then M /\ (MaxADSet x) = {a} by A2, A6, Def2;
hence ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} ) by A6; ::_thesis: verum
end;
assume A7: for x being Point of X ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} ) ; ::_thesis: M is maximal_T_0
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_X_holds_
x_in_MaxADSet_M
let x be set ; ::_thesis: ( x in the carrier of X implies x in MaxADSet M )
A8: M c= MaxADSet M by TEX_4:32;
assume x in the carrier of X ; ::_thesis: x in MaxADSet M
then reconsider y = x as Point of X ;
consider a being Point of X such that
A9: a in M and
A10: M /\ (MaxADSet y) = {a} by A7;
{a} c= MaxADSet y by A10, XBOOLE_1:17;
then a in MaxADSet y by ZFMISC_1:31;
then (MaxADSet y) /\ (MaxADSet M) <> {} by A9, A8, XBOOLE_0:def_4;
then MaxADSet y meets MaxADSet M by XBOOLE_0:def_7;
then A11: MaxADSet y c= MaxADSet M by TEX_4:30;
{y} c= MaxADSet y by TEX_4:18;
then y in MaxADSet y by ZFMISC_1:31;
hence x in MaxADSet M by A11; ::_thesis: verum
end;
then the carrier of X c= MaxADSet M by TARSKI:def_3;
then A12: MaxADSet M = the carrier of X by XBOOLE_0:def_10;
for b being Point of X st b in M holds
M /\ (MaxADSet b) = {b}
proof
let b be Point of X; ::_thesis: ( b in M implies M /\ (MaxADSet b) = {b} )
A13: ex a being Point of X st
( a in M & M /\ (MaxADSet b) = {a} ) by A7;
{b} c= MaxADSet b by TEX_4:18;
then A14: b in MaxADSet b by ZFMISC_1:31;
assume b in M ; ::_thesis: M /\ (MaxADSet b) = {b}
then b in M /\ (MaxADSet b) by A14, XBOOLE_0:def_4;
hence M /\ (MaxADSet b) = {b} by A13, TARSKI:def_1; ::_thesis: verum
end;
then M is T_0 by Def2;
hence M is maximal_T_0 by A12, Def5; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines maximal_T_0 TSP_2:def_6_:_
for X being non empty TopSpace
for M being Subset of X holds
( M is maximal_T_0 iff for x being Point of X ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} ) );
theorem Th9: :: TSP_2:9
for X being non empty TopSpace
for A being Subset of X st A is T_0 holds
ex M being Subset of X st
( A c= M & M is maximal_T_0 )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is T_0 holds
ex M being Subset of X st
( A c= M & M is maximal_T_0 )
let A be Subset of X; ::_thesis: ( A is T_0 implies ex M being Subset of X st
( A c= M & M is maximal_T_0 ) )
set D = ([#] X) \ (MaxADSet A);
set F = { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } ;
now__::_thesis:_for_C_being_set_st_C_in__{__(MaxADSet_d)_where_d_is_Point_of_X_:_d_in_([#]_X)_\_(MaxADSet_A)__}__holds_
C_in_bool_the_carrier_of_X
let C be set ; ::_thesis: ( C in { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } implies C in bool the carrier of X )
assume C in { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } ; ::_thesis: C in bool the carrier of X
then ex a being Point of X st
( C = MaxADSet a & a in ([#] X) \ (MaxADSet A) ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
then reconsider F = { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } as Subset-Family of X by TARSKI:def_3;
assume A1: A is T_0 ; ::_thesis: ex M being Subset of X st
( A c= M & M is maximal_T_0 )
defpred S1[ Subset of X, set ] means ( $2 in ([#] X) \ (MaxADSet A) & $2 in $1 );
A2: ([#] X) \ (MaxADSet A) = (MaxADSet A) ` ;
then A3: MaxADSet A misses ([#] X) \ (MaxADSet A) by SUBSET_1:24;
A c= MaxADSet A by TEX_4:32;
then A misses ([#] X) \ (MaxADSet A) by A2, SUBSET_1:24;
then A4: A /\ (([#] X) \ (MaxADSet A)) = {} by XBOOLE_0:def_7;
reconsider F = F as Subset-Family of X ;
A5: for S being Subset of X st S in F holds
ex x being Point of X st S1[S,x]
proof
let S be Subset of X; ::_thesis: ( S in F implies ex x being Point of X st S1[S,x] )
assume S in F ; ::_thesis: ex x being Point of X st S1[S,x]
then consider d being Point of X such that
A6: S = MaxADSet d and
A7: d in ([#] X) \ (MaxADSet A) ;
take d ; ::_thesis: S1[S,d]
{d} c= MaxADSet d by TEX_4:18;
hence S1[S,d] by A6, A7, ZFMISC_1:31; ::_thesis: verum
end;
consider f being Function of F, the carrier of X such that
A8: for S being Subset of X st S in F holds
S1[S,f . S] from TEX_2:sch_1(A5);
set M = A \/ (f .: F);
now__::_thesis:_for_x_being_set_st_x_in_f_.:_F_holds_
x_in_([#]_X)_\_(MaxADSet_A)
let x be set ; ::_thesis: ( x in f .: F implies x in ([#] X) \ (MaxADSet A) )
assume x in f .: F ; ::_thesis: x in ([#] X) \ (MaxADSet A)
then ex S being set st
( S in F & S in F & x = f . S ) by FUNCT_2:64;
hence x in ([#] X) \ (MaxADSet A) by A8; ::_thesis: verum
end;
then f .: F c= ([#] X) \ (MaxADSet A) by TARSKI:def_3;
then A9: MaxADSet A misses f .: F by A3, XBOOLE_1:63;
thus ex M being Subset of X st
( A c= M & M is maximal_T_0 ) ::_thesis: verum
proof
take A \/ (f .: F) ; ::_thesis: ( A c= A \/ (f .: F) & A \/ (f .: F) is maximal_T_0 )
thus A10: A c= A \/ (f .: F) by XBOOLE_1:7; ::_thesis: A \/ (f .: F) is maximal_T_0
for x being Point of X ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )
proof
let x be Point of X; ::_thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )
A11: [#] X = (MaxADSet A) \/ (([#] X) \ (MaxADSet A)) by XBOOLE_1:45;
now__::_thesis:_ex_a_being_Point_of_X_st_
(_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(MaxADSet_x)_=_{a}_)
percases ( x in MaxADSet A or x in ([#] X) \ (MaxADSet A) ) by A11, XBOOLE_0:def_3;
supposeA12: x in MaxADSet A ; ::_thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )
now__::_thesis:_ex_a_being_Point_of_X_st_
(_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(MaxADSet_x)_=_{a}_)
{x} c= MaxADSet A by A12, ZFMISC_1:31;
then MaxADSet {x} c= MaxADSet A by TEX_4:34;
then MaxADSet x c= MaxADSet A by TEX_4:28;
then f .: F misses MaxADSet x by A9, XBOOLE_1:63;
then (f .: F) /\ (MaxADSet x) = {} by XBOOLE_0:def_7;
then A13: (A \/ (f .: F)) /\ (MaxADSet x) = (A /\ (MaxADSet x)) \/ {} by XBOOLE_1:23;
x in union { (MaxADSet a) where a is Point of X : a in A } by A12, TEX_4:def_11;
then consider C being set such that
A14: x in C and
A15: C in { (MaxADSet a) where a is Point of X : a in A } by TARSKI:def_4;
consider a being Point of X such that
A16: C = MaxADSet a and
A17: a in A by A15;
take a = a; ::_thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )
thus a in A \/ (f .: F) by A10, A17; ::_thesis: (A \/ (f .: F)) /\ (MaxADSet x) = {a}
MaxADSet a = MaxADSet x by A14, A16, TEX_4:21;
hence (A \/ (f .: F)) /\ (MaxADSet x) = {a} by A1, A17, A13, Def2; ::_thesis: verum
end;
hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) ; ::_thesis: verum
end;
supposeA18: x in ([#] X) \ (MaxADSet A) ; ::_thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )
then A19: MaxADSet x in F ;
now__::_thesis:_ex_a_being_Point_of_X_st_
(_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(MaxADSet_x)_=_{a}_)
reconsider a = f . (MaxADSet x) as Point of X by A19, FUNCT_2:5;
take a = a; ::_thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )
A20: f .: F c= A \/ (f .: F) by XBOOLE_1:7;
now__::_thesis:_for_y_being_set_st_y_in_(A_\/_(f_.:_F))_/\_(MaxADSet_x)_holds_
y_in_{a}
let y be set ; ::_thesis: ( y in (A \/ (f .: F)) /\ (MaxADSet x) implies y in {a} )
assume A21: y in (A \/ (f .: F)) /\ (MaxADSet x) ; ::_thesis: y in {a}
then reconsider z = y as Point of X ;
A22: z in A \/ (f .: F) by A21, XBOOLE_0:def_4;
A23: z in MaxADSet x by A21, XBOOLE_0:def_4;
then A24: MaxADSet z = MaxADSet x by TEX_4:21;
now__::_thesis:_MaxADSet_x_c=_([#]_X)_\_(MaxADSet_A)
assume not MaxADSet x c= ([#] X) \ (MaxADSet A) ; ::_thesis: contradiction
then MaxADSet x meets MaxADSet A by A2, SUBSET_1:23;
then A25: MaxADSet x c= MaxADSet A by TEX_4:30;
{x} c= MaxADSet x by TEX_4:18;
then x in MaxADSet x by ZFMISC_1:31;
hence contradiction by A3, A18, A25, XBOOLE_0:3; ::_thesis: verum
end;
then not z in A by A4, A23, XBOOLE_0:def_4;
then z in f .: F by A22, XBOOLE_0:def_3;
then consider C being set such that
A26: C in F and
C in F and
A27: z = f . C by FUNCT_2:64;
reconsider C = C as Subset of X by A26;
consider w being Point of X such that
A28: C = MaxADSet w and
w in ([#] X) \ (MaxADSet A) by A26;
z in MaxADSet w by A8, A26, A27, A28;
then f . (MaxADSet w) = a by A24, TEX_4:21;
hence y in {a} by A27, A28, TARSKI:def_1; ::_thesis: verum
end;
then A29: (A \/ (f .: F)) /\ (MaxADSet x) c= {a} by TARSKI:def_3;
A30: a in f .: F by A19, FUNCT_2:35;
hence a in A \/ (f .: F) by A20; ::_thesis: (A \/ (f .: F)) /\ (MaxADSet x) = {a}
a in MaxADSet x by A8, A19;
then A31: {a} c= MaxADSet x by ZFMISC_1:31;
{a} c= A \/ (f .: F) by A20, A30, ZFMISC_1:31;
then {a} c= (A \/ (f .: F)) /\ (MaxADSet x) by A31, XBOOLE_1:19;
hence (A \/ (f .: F)) /\ (MaxADSet x) = {a} by A29, XBOOLE_0:def_10; ::_thesis: verum
end;
hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) ; ::_thesis: verum
end;
end;
end;
hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) ; ::_thesis: verum
end;
hence A \/ (f .: F) is maximal_T_0 by Def6; ::_thesis: verum
end;
end;
theorem Th10: :: TSP_2:10
for X being non empty TopSpace ex M being Subset of X st M is maximal_T_0
proof
let X be non empty TopSpace; ::_thesis: ex M being Subset of X st M is maximal_T_0
set A = {} X;
{} X is discrete by TEX_2:29;
then consider M being Subset of X such that
{} X c= M and
A1: M is maximal_T_0 by Th9, TSP_1:9;
take M ; ::_thesis: M is maximal_T_0
thus M is maximal_T_0 by A1; ::_thesis: verum
end;
begin
definition
let Y be non empty TopStruct ;
let IT be SubSpace of Y;
attrIT is maximal_T_0 means :Def7: :: TSP_2:def 7
for A being Subset of Y st A = the carrier of IT holds
A is maximal_T_0 ;
end;
:: deftheorem Def7 defines maximal_T_0 TSP_2:def_7_:_
for Y being non empty TopStruct
for IT being SubSpace of Y holds
( IT is maximal_T_0 iff for A being Subset of Y st A = the carrier of IT holds
A is maximal_T_0 );
theorem Th11: :: TSP_2:11
for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is maximal_T_0 iff Y0 is maximal_T_0 )
proof
let Y be non empty TopStruct ; ::_thesis: for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is maximal_T_0 iff Y0 is maximal_T_0 )
let Y0 be SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 holds
( A is maximal_T_0 iff Y0 is maximal_T_0 )
let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 implies ( A is maximal_T_0 iff Y0 is maximal_T_0 ) )
assume A1: A = the carrier of Y0 ; ::_thesis: ( A is maximal_T_0 iff Y0 is maximal_T_0 )
hereby ::_thesis: ( Y0 is maximal_T_0 implies A is maximal_T_0 )
assume A is maximal_T_0 ; ::_thesis: Y0 is maximal_T_0
then for A being Subset of Y st A = the carrier of Y0 holds
A is maximal_T_0 by A1;
hence Y0 is maximal_T_0 by Def7; ::_thesis: verum
end;
thus ( Y0 is maximal_T_0 implies A is maximal_T_0 ) by A1, Def7; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_Z_being_non_empty_TopStruct_
for_Z0_being_SubSpace_of_Z_holds_the_carrier_of_Z0_is_Subset_of_Z
let Z be non empty 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;
registration
let Y be non empty TopStruct ;
cluster non empty maximal_T_0 -> non empty V56() for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is maximal_T_0 holds
b1 is V56()
proof
let Y0 be non empty SubSpace of Y; ::_thesis: ( Y0 is maximal_T_0 implies Y0 is V56() )
reconsider A = the carrier of Y0 as Subset of Y by Lm1;
assume Y0 is maximal_T_0 ; ::_thesis: Y0 is V56()
then A is maximal_T_0 by Th11;
then A is T_0 by Def4;
hence Y0 is V56() by TSP_1:13; ::_thesis: verum
end;
cluster non empty V56() -> non empty non maximal_T_0 for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is V56() holds
not b1 is maximal_T_0 ;
end;
definition
let X be non empty TopSpace;
let X0 be non empty SubSpace of X;
redefine attr X0 is maximal_T_0 means :: TSP_2:def 8
( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) );
compatibility
( X0 is maximal_T_0 iff ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) )
proof
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus ( X0 is maximal_T_0 implies ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) ) ::_thesis: ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) implies X0 is maximal_T_0 )
proof
assume X0 is maximal_T_0 ; ::_thesis: ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) )
then A1: A is maximal_T_0 by Th11;
then A is T_0 by Def4;
hence X0 is V56() by TSP_1:13; ::_thesis: for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #)
thus for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ::_thesis: verum
proof
let Y0 be non empty V56() SubSpace of X; ::_thesis: ( X0 is SubSpace of Y0 implies TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) )
reconsider D = the carrier of Y0 as Subset of X by TSEP_1:1;
assume X0 is SubSpace of Y0 ; ::_thesis: TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #)
then A2: A c= D by TSEP_1:4;
D is T_0 by TSP_1:13;
then A = D by A1, A2, Def4;
hence TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) by TSEP_1:5; ::_thesis: verum
end;
end;
assume X0 is V56() ; ::_thesis: ( ex Y0 being non empty V56() SubSpace of X st
( X0 is SubSpace of Y0 & not TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) or X0 is maximal_T_0 )
then A3: A is T_0 by TSP_1:13;
assume A4: for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ; ::_thesis: X0 is maximal_T_0
now__::_thesis:_for_D_being_Subset_of_X_st_D_is_T_0_&_A_c=_D_holds_
A_=_D
let D be Subset of X; ::_thesis: ( D is T_0 & A c= D implies A = D )
assume A5: D is T_0 ; ::_thesis: ( A c= D implies A = D )
assume A6: A c= D ; ::_thesis: A = D
then D <> {} ;
then consider Y0 being non empty strict V56() SubSpace of X such that
A7: D = the carrier of Y0 by A5, TSP_1:18;
X0 is SubSpace of Y0 by A6, A7, TSEP_1:4;
hence A = D by A4, A7; ::_thesis: verum
end;
then A is maximal_T_0 by A3, Def4;
hence X0 is maximal_T_0 by Th11; ::_thesis: verum
end;
end;
:: deftheorem defines maximal_T_0 TSP_2:def_8_:_
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is maximal_T_0 iff ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) );
theorem Th12: :: TSP_2:12
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is maximal_T_0 holds
ex X0 being non empty strict SubSpace of X st
( X0 is maximal_T_0 & A0 = the carrier of X0 )
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is maximal_T_0 holds
ex X0 being non empty strict SubSpace of X st
( X0 is maximal_T_0 & A0 = the carrier of X0 )
let A0 be non empty Subset of X; ::_thesis: ( A0 is maximal_T_0 implies ex X0 being non empty strict SubSpace of X st
( X0 is maximal_T_0 & A0 = the carrier of X0 ) )
assume A1: A0 is maximal_T_0 ; ::_thesis: ex X0 being non empty strict SubSpace of X st
( X0 is maximal_T_0 & A0 = the carrier of X0 )
consider X0 being non empty strict SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
take X0 ; ::_thesis: ( X0 is maximal_T_0 & A0 = the carrier of X0 )
thus ( X0 is maximal_T_0 & A0 = the carrier of X0 ) by A1, A2, Th11; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster maximal_T_0 -> dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is maximal_T_0 holds
b1 is dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is maximal_T_0 implies X0 is dense )
reconsider A = the carrier of X0 as Subset of X by Lm1;
assume X0 is maximal_T_0 ; ::_thesis: X0 is dense
then A is maximal_T_0 by Th11;
then A is dense by Th2;
hence X0 is dense by TEX_3:9; ::_thesis: verum
end;
cluster non dense -> non maximal_T_0 for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is dense holds
not b1 is maximal_T_0 ;
cluster open maximal_T_0 -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is open & b1 is maximal_T_0 holds
not b1 is proper
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is open & X0 is maximal_T_0 implies not X0 is proper )
reconsider A = the carrier of X0 as Subset of X by Lm1;
assume X0 is open ; ::_thesis: ( not X0 is maximal_T_0 or not X0 is proper )
then A1: A is open by TSEP_1:16;
assume X0 is maximal_T_0 ; ::_thesis: not X0 is proper
then A is maximal_T_0 by Th11;
then not A is proper by A1, Th3;
hence not X0 is proper by TEX_2:8; ::_thesis: verum
end;
cluster open proper -> non maximal_T_0 for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is open & b1 is proper holds
not b1 is maximal_T_0 ;
cluster proper maximal_T_0 -> non open for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper & b1 is maximal_T_0 holds
not b1 is open ;
cluster closed maximal_T_0 -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is closed & b1 is maximal_T_0 holds
not b1 is proper
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is closed & X0 is maximal_T_0 implies not X0 is proper )
reconsider A = the carrier of X0 as Subset of X by Lm1;
assume X0 is closed ; ::_thesis: ( not X0 is maximal_T_0 or not X0 is proper )
then A2: A is closed by TSEP_1:11;
assume X0 is maximal_T_0 ; ::_thesis: not X0 is proper
then A is maximal_T_0 by Th11;
then not A is proper by A2, Th3;
hence not X0 is proper by TEX_2:8; ::_thesis: verum
end;
cluster closed proper -> non maximal_T_0 for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is closed & b1 is proper holds
not b1 is maximal_T_0 ;
cluster proper maximal_T_0 -> non closed for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper & b1 is maximal_T_0 holds
not b1 is closed ;
end;
theorem :: TSP_2:13
for X being non empty TopSpace
for Y0 being non empty V56() SubSpace of X ex X0 being strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_T_0 )
proof
let X be non empty TopSpace; ::_thesis: for Y0 being non empty V56() SubSpace of X ex X0 being strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_T_0 )
let Y0 be non empty V56() SubSpace of X; ::_thesis: ex X0 being strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_T_0 )
reconsider A = the carrier of Y0 as Subset of X by Lm1;
A is T_0 by TSP_1:13;
then consider M being Subset of X such that
A1: A c= M and
A2: M is maximal_T_0 by Th9;
not M is empty by A2, Th4;
then consider X0 being non empty strict SubSpace of X such that
A3: X0 is maximal_T_0 and
A4: M = the carrier of X0 by A2, Th12;
take X0 ; ::_thesis: ( Y0 is SubSpace of X0 & X0 is maximal_T_0 )
thus ( Y0 is SubSpace of X0 & X0 is maximal_T_0 ) by A1, A3, A4, TSEP_1:4; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like maximal_T_0 for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is maximal_T_0 & b1 is strict & not b1 is empty )
proof
consider M being Subset of X such that
A1: M is maximal_T_0 by Th10;
not M is empty by A1, Th4;
then consider X0 being non empty strict SubSpace of X such that
A2: X0 is maximal_T_0 and
M = the carrier of X0 by A1, Th12;
take X0 ; ::_thesis: ( X0 is maximal_T_0 & X0 is strict & not X0 is empty )
thus ( X0 is maximal_T_0 & X0 is strict & not X0 is empty ) by A2; ::_thesis: verum
end;
end;
definition
let X be non empty TopSpace;
mode maximal_Kolmogorov_subspace of X is maximal_T_0 SubSpace of X;
end;
theorem Th14: :: TSP_2:14
for X being non empty TopSpace
for X0 being maximal_Kolmogorov_subspace of X
for G being Subset of X
for G0 being Subset of X0 st G0 = G holds
( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )
proof
let X be non empty TopSpace; ::_thesis: for X0 being maximal_Kolmogorov_subspace of X
for G being Subset of X
for G0 being Subset of X0 st G0 = G holds
( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )
let X0 be maximal_Kolmogorov_subspace of X; ::_thesis: for G being Subset of X
for G0 being Subset of X0 st G0 = G holds
( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )
let G be Subset of X; ::_thesis: for G0 being Subset of X0 st G0 = G holds
( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )
let G0 be Subset of X0; ::_thesis: ( G0 = G implies ( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) )
reconsider M = the carrier of X0 as Subset of X by Lm1;
assume A1: G0 = G ; ::_thesis: ( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )
A2: M is maximal_T_0 by Th11;
thus ( G0 is open implies ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) ::_thesis: ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 implies G0 is open )
proof
assume G0 is open ; ::_thesis: ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 )
then A3: ex H being Subset of X st
( H is open & G0 = H /\ M ) by TSP_1:def_1;
hence MaxADSet G is open by A2, A1, Th6; ::_thesis: G0 = (MaxADSet G) /\ the carrier of X0
thus G0 = (MaxADSet G) /\ the carrier of X0 by A2, A1, A3, Th6; ::_thesis: verum
end;
assume A4: MaxADSet G is open ; ::_thesis: ( not G0 = (MaxADSet G) /\ the carrier of X0 or G0 is open )
assume G0 = (MaxADSet G) /\ the carrier of X0 ; ::_thesis: G0 is open
hence G0 is open by A4, TSP_1:def_1; ::_thesis: verum
end;
theorem :: TSP_2:15
for X being non empty TopSpace
for X0 being maximal_Kolmogorov_subspace of X
for G being Subset of X holds
( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 ) ) )
proof
let X be non empty TopSpace; ::_thesis: for X0 being maximal_Kolmogorov_subspace of X
for G being Subset of X holds
( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 ) ) )
let X0 be maximal_Kolmogorov_subspace of X; ::_thesis: for G being Subset of X holds
( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 ) ) )
let G be Subset of X; ::_thesis: ( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 ) ) )
reconsider M = the carrier of X0 as Subset of X by Lm1;
thus ( G is open implies ( G = MaxADSet G & ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 ) ) ) ::_thesis: ( G = MaxADSet G & ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 ) implies G is open )
proof
reconsider G0 = G /\ M as Subset of X0 by XBOOLE_1:17;
reconsider G0 = G0 as Subset of X0 ;
assume A1: G is open ; ::_thesis: ( G = MaxADSet G & ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 ) )
hence G = MaxADSet G by TEX_4:56; ::_thesis: ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 )
take G0 ; ::_thesis: ( G0 is open & G0 = G /\ the carrier of X0 )
thus G0 is open by A1, TSP_1:def_1; ::_thesis: G0 = G /\ the carrier of X0
thus G0 = G /\ the carrier of X0 ; ::_thesis: verum
end;
assume A2: G = MaxADSet G ; ::_thesis: ( for G0 being Subset of X0 holds
( not G0 is open or not G0 = G /\ the carrier of X0 ) or G is open )
given G0 being Subset of X0 such that A3: G0 is open and
A4: G0 = G /\ the carrier of X0 ; ::_thesis: G is open
set E = G0;
G0 c= M ;
then reconsider E = G0 as Subset of X by XBOOLE_1:1;
A5: E c= MaxADSet G by A2, A4, XBOOLE_1:17;
A6: M is maximal_T_0 by Th11;
for x being set st x in G holds
x in MaxADSet E
proof
let x be set ; ::_thesis: ( x in G implies x in MaxADSet E )
assume A7: x in G ; ::_thesis: x in MaxADSet E
then reconsider a = x as Point of X ;
consider b being Point of X such that
A8: b in M and
A9: M /\ (MaxADSet a) = {b} by A6, Def6;
A10: {b} c= MaxADSet a by A9, XBOOLE_1:17;
{a} c= G by A7, ZFMISC_1:31;
then MaxADSet {a} c= G by A2, TEX_4:34;
then MaxADSet a c= G by TEX_4:28;
then {b} c= G by A10, XBOOLE_1:1;
then b in G by ZFMISC_1:31;
then b in E by A4, A8, XBOOLE_0:def_4;
then {b} c= E by ZFMISC_1:31;
then MaxADSet {b} c= MaxADSet E by TEX_4:31;
then A11: MaxADSet b c= MaxADSet E by TEX_4:28;
b in MaxADSet a by A10, ZFMISC_1:31;
then MaxADSet b = MaxADSet a by TEX_4:21;
then {a} c= MaxADSet b by TEX_4:18;
then a in MaxADSet b by ZFMISC_1:31;
hence x in MaxADSet E by A11; ::_thesis: verum
end;
then A12: G c= MaxADSet E by TARSKI:def_3;
MaxADSet E is open by A3, Th14;
hence G is open by A2, A5, A12, TEX_4:35; ::_thesis: verum
end;
theorem Th16: :: TSP_2:16
for X being non empty TopSpace
for X0 being maximal_Kolmogorov_subspace of X
for F being Subset of X
for F0 being Subset of X0 st F0 = F holds
( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )
proof
let X be non empty TopSpace; ::_thesis: for X0 being maximal_Kolmogorov_subspace of X
for F being Subset of X
for F0 being Subset of X0 st F0 = F holds
( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )
let X0 be maximal_Kolmogorov_subspace of X; ::_thesis: for F being Subset of X
for F0 being Subset of X0 st F0 = F holds
( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
let F be Subset of X; ::_thesis: for F0 being Subset of X0 st F0 = F holds
( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )
let F0 be Subset of X0; ::_thesis: ( F0 = F implies ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) )
assume A1: F0 = F ; ::_thesis: ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )
A2: M is maximal_T_0 by Th11;
thus ( F0 is closed implies ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) ::_thesis: ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 implies F0 is closed )
proof
assume F0 is closed ; ::_thesis: ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 )
then A3: ex H being Subset of X st
( H is closed & F0 = H /\ M ) by TSP_1:def_2;
hence MaxADSet F is closed by A2, A1, Th5; ::_thesis: F0 = (MaxADSet F) /\ the carrier of X0
thus F0 = (MaxADSet F) /\ the carrier of X0 by A2, A1, A3, Th5; ::_thesis: verum
end;
assume A4: MaxADSet F is closed ; ::_thesis: ( not F0 = (MaxADSet F) /\ the carrier of X0 or F0 is closed )
assume F0 = (MaxADSet F) /\ the carrier of X0 ; ::_thesis: F0 is closed
hence F0 is closed by A4, TSP_1:def_2; ::_thesis: verum
end;
theorem :: TSP_2:17
for X being non empty TopSpace
for X0 being maximal_Kolmogorov_subspace of X
for F being Subset of X holds
( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) )
proof
let X be non empty TopSpace; ::_thesis: for X0 being maximal_Kolmogorov_subspace of X
for F being Subset of X holds
( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) )
let X0 be maximal_Kolmogorov_subspace of X; ::_thesis: for F being Subset of X holds
( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) )
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
let F be Subset of X; ::_thesis: ( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) )
thus ( F is closed implies ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) ) ::_thesis: ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) implies F is closed )
proof
set F0 = F /\ M;
reconsider F0 = F /\ M as Subset of X0 by XBOOLE_1:17;
assume A1: F is closed ; ::_thesis: ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) )
hence F = MaxADSet F by TEX_4:60; ::_thesis: ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 )
take F0 ; ::_thesis: ( F0 is closed & F0 = F /\ the carrier of X0 )
thus F0 is closed by A1, TSP_1:def_2; ::_thesis: F0 = F /\ the carrier of X0
thus F0 = F /\ the carrier of X0 ; ::_thesis: verum
end;
assume A2: F = MaxADSet F ; ::_thesis: ( for F0 being Subset of X0 holds
( not F0 is closed or not F0 = F /\ the carrier of X0 ) or F is closed )
given F0 being Subset of X0 such that A3: F0 is closed and
A4: F0 = F /\ the carrier of X0 ; ::_thesis: F is closed
set E = F0;
F0 c= M ;
then reconsider E = F0 as Subset of X by XBOOLE_1:1;
A5: E c= MaxADSet F by A2, A4, XBOOLE_1:17;
A6: M is maximal_T_0 by Th11;
for x being set st x in F holds
x in MaxADSet E
proof
let x be set ; ::_thesis: ( x in F implies x in MaxADSet E )
assume A7: x in F ; ::_thesis: x in MaxADSet E
then reconsider a = x as Point of X ;
consider b being Point of X such that
A8: b in M and
A9: M /\ (MaxADSet a) = {b} by A6, Def6;
A10: {b} c= MaxADSet a by A9, XBOOLE_1:17;
{a} c= F by A7, ZFMISC_1:31;
then MaxADSet {a} c= F by A2, TEX_4:34;
then MaxADSet a c= F by TEX_4:28;
then {b} c= F by A10, XBOOLE_1:1;
then b in F by ZFMISC_1:31;
then b in E by A4, A8, XBOOLE_0:def_4;
then {b} c= E by ZFMISC_1:31;
then MaxADSet {b} c= MaxADSet E by TEX_4:31;
then A11: MaxADSet b c= MaxADSet E by TEX_4:28;
b in MaxADSet a by A10, ZFMISC_1:31;
then MaxADSet b = MaxADSet a by TEX_4:21;
then {a} c= MaxADSet b by TEX_4:18;
then a in MaxADSet b by ZFMISC_1:31;
hence x in MaxADSet E by A11; ::_thesis: verum
end;
then A12: F c= MaxADSet E by TARSKI:def_3;
MaxADSet E is closed by A3, Th16;
hence F is closed by A2, A5, A12, TEX_4:35; ::_thesis: verum
end;
begin
theorem Th18: :: TSP_2:18
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being Function of X,X0
for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is continuous Function of X,X0
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being Function of X,X0
for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is continuous Function of X,X0
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being Function of X,X0
for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is continuous Function of X,X0
let r be Function of X,X0; ::_thesis: for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is continuous Function of X,X0
let M be Subset of X; ::_thesis: ( M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) implies r is continuous Function of X,X0 )
assume A1: M = the carrier of X0 ; ::_thesis: ( ex a being Point of X st not M /\ (MaxADSet a) = {(r . a)} or r is continuous Function of X,X0 )
reconsider N = M as Subset of X ;
assume A2: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ; ::_thesis: r is continuous Function of X,X0
A3: N is maximal_T_0 by A1, Th11;
then A4: N is T_0 by Def4;
for F being Subset of X0 st F is closed holds
r " F is closed
proof
let F be Subset of X0; ::_thesis: ( F is closed implies r " F is closed )
reconsider E = F as Subset of X by A1, XBOOLE_1:1;
set R = { (MaxADSet a) where a is Point of X : a in E } ;
now__::_thesis:_for_x_being_set_st_x_in_r_"_F_holds_
x_in_union__{__(MaxADSet_a)_where_a_is_Point_of_X_:_a_in_E__}_
let x be set ; ::_thesis: ( x in r " F implies x in union { (MaxADSet a) where a is Point of X : a in E } )
assume A5: x in r " F ; ::_thesis: x in union { (MaxADSet a) where a is Point of X : a in E }
then reconsider b = x as Point of X ;
A6: r . b in F by A5, FUNCT_2:38;
E c= the carrier of X ;
then reconsider a = r . b as Point of X by A6;
MaxADSet a in { (MaxADSet a) where a is Point of X : a in E } by A6;
then A7: MaxADSet a c= union { (MaxADSet a) where a is Point of X : a in E } by ZFMISC_1:74;
M /\ (MaxADSet b) = {a} by A2;
then a in M /\ (MaxADSet b) by ZFMISC_1:31;
then a in MaxADSet b by XBOOLE_0:def_4;
then A8: MaxADSet a = MaxADSet b by TEX_4:21;
A9: {b} c= MaxADSet b by TEX_4:18;
b in {b} by TARSKI:def_1;
then b in MaxADSet a by A8, A9;
hence x in union { (MaxADSet a) where a is Point of X : a in E } by A7; ::_thesis: verum
end;
then A10: r " F c= union { (MaxADSet a) where a is Point of X : a in E } by TARSKI:def_3;
assume F is closed ; ::_thesis: r " F is closed
then ex P being Subset of X st
( P is closed & P /\ ([#] X0) = F ) by PRE_TOPC:13;
then A11: MaxADSet E is closed by A1, A3, Th5;
now__::_thesis:_for_C_being_set_st_C_in__{__(MaxADSet_a)_where_a_is_Point_of_X_:_a_in_E__}__holds_
C_c=_r_"_F
let C be set ; ::_thesis: ( C in { (MaxADSet a) where a is Point of X : a in E } implies C c= r " F )
assume C in { (MaxADSet a) where a is Point of X : a in E } ; ::_thesis: C c= r " F
then consider a being Point of X such that
A12: C = MaxADSet a and
A13: a in E ;
now__::_thesis:_for_x_being_set_st_x_in_C_holds_
x_in_r_"_F
let x be set ; ::_thesis: ( x in C implies x in r " F )
assume A14: x in C ; ::_thesis: x in r " F
then reconsider b = x as Point of X by A12;
A15: M /\ (MaxADSet b) = {(r . b)} by A2;
A16: M /\ (MaxADSet a) = {a} by A1, A4, A13, Def2;
MaxADSet a = MaxADSet b by A12, A14, TEX_4:21;
then a = r . x by A16, A15, ZFMISC_1:3;
hence x in r " F by A12, A13, A14, FUNCT_2:38; ::_thesis: verum
end;
hence C c= r " F by TARSKI:def_3; ::_thesis: verum
end;
then A17: union { (MaxADSet a) where a is Point of X : a in E } c= r " F by ZFMISC_1:76;
union { (MaxADSet a) where a is Point of X : a in E } = MaxADSet E by TEX_4:def_11;
hence r " F is closed by A11, A17, A10, XBOOLE_0:def_10; ::_thesis: verum
end;
hence r is continuous Function of X,X0 by PRE_TOPC:def_6; ::_thesis: verum
end;
theorem :: TSP_2:19
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds
r is continuous Function of X,X0
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds
r is continuous Function of X,X0
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds
r is continuous Function of X,X0
let r be Function of X,X0; ::_thesis: ( ( for a being Point of X holds r . a in MaxADSet a ) implies r is continuous Function of X,X0 )
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
assume A1: for a being Point of X holds r . a in MaxADSet a ; ::_thesis: r is continuous Function of X,X0
M is maximal_T_0 by Th11;
then A2: M is T_0 by Def4;
A3: M c= the carrier of X ;
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)}
proof
let a be Point of X; ::_thesis: M /\ (MaxADSet a) = {(r . a)}
reconsider s = r . a as Point of X by A3, TARSKI:def_3;
A4: s in MaxADSet a by A1;
M /\ (MaxADSet s) = {s} by A2, Def2;
hence M /\ (MaxADSet a) = {(r . a)} by A4, TEX_4:21; ::_thesis: verum
end;
hence r is continuous Function of X,X0 by Th18; ::_thesis: verum
end;
theorem Th20: :: TSP_2:20
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0
for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is being_a_retraction
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0
for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is being_a_retraction
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0
for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is being_a_retraction
let r be continuous Function of X,X0; ::_thesis: for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is being_a_retraction
let M be Subset of X; ::_thesis: ( M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) implies r is being_a_retraction )
reconsider N = M as Subset of X ;
assume A1: M = the carrier of X0 ; ::_thesis: ( ex a being Point of X st not M /\ (MaxADSet a) = {(r . a)} or r is being_a_retraction )
then N is maximal_T_0 by Th11;
then A2: N is T_0 by Def4;
assume A3: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ; ::_thesis: r is being_a_retraction
for x being Point of X st x in the carrier of X0 holds
r . x = x
proof
let x be Point of X; ::_thesis: ( x in the carrier of X0 implies r . x = x )
assume x in the carrier of X0 ; ::_thesis: r . x = x
then A4: M /\ (MaxADSet x) = {x} by A1, A2, Def2;
M /\ (MaxADSet x) = {(r . x)} by A3;
hence r . x = x by A4, ZFMISC_1:3; ::_thesis: verum
end;
hence r is being_a_retraction by BORSUK_1:def_16; ::_thesis: verum
end;
theorem Th21: :: TSP_2:21
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds
r is being_a_retraction
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds
r is being_a_retraction
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds
r is being_a_retraction
let r be continuous Function of X,X0; ::_thesis: ( ( for a being Point of X holds r . a in MaxADSet a ) implies r is being_a_retraction )
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
assume A1: for a being Point of X holds r . a in MaxADSet a ; ::_thesis: r is being_a_retraction
M is maximal_T_0 by Th11;
then A2: M is T_0 by Def4;
A3: M c= the carrier of X ;
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)}
proof
let a be Point of X; ::_thesis: M /\ (MaxADSet a) = {(r . a)}
reconsider s = r . a as Point of X by A3, TARSKI:def_3;
A4: s in MaxADSet a by A1;
M /\ (MaxADSet s) = {s} by A2, Def2;
hence M /\ (MaxADSet a) = {(r . a)} by A4, TEX_4:21; ::_thesis: verum
end;
hence r is being_a_retraction by Th20; ::_thesis: verum
end;
theorem Th22: :: TSP_2:22
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X ex r being continuous Function of X,X0 st r is being_a_retraction
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X ex r being continuous Function of X,X0 st r is being_a_retraction
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: ex r being continuous Function of X,X0 st r is being_a_retraction
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
defpred S1[ Point of X, set ] means M /\ (MaxADSet $1) = {$2};
A1: M is maximal_T_0 by Th11;
A2: for x being Point of X ex a being Point of X0 st S1[x,a]
proof
let x be Point of X; ::_thesis: ex a being Point of X0 st S1[x,a]
consider a being Point of X such that
A3: a in M and
A4: M /\ (MaxADSet x) = {a} by A1, Def6;
reconsider a = a as Point of X0 by A3;
take a ; ::_thesis: S1[x,a]
thus S1[x,a] by A4; ::_thesis: verum
end;
consider r being Function of X,X0 such that
A5: for x being Point of X holds S1[x,r . x] from FUNCT_2:sch_3(A2);
reconsider r = r as continuous Function of X,X0 by A5, Th18;
take r ; ::_thesis: r is being_a_retraction
thus r is being_a_retraction by A5, Th20; ::_thesis: verum
end;
theorem :: TSP_2:23
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X holds X0 is_a_retract_of X
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X holds X0 is_a_retract_of X
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: X0 is_a_retract_of X
ex r being continuous Function of X,X0 st r is being_a_retraction by Th22;
hence X0 is_a_retract_of X by BORSUK_1:def_17; ::_thesis: verum
end;
Lm2: for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a}
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a}
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a}
let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for a being Point of X
for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a} )
assume A1: r is being_a_retraction ; ::_thesis: for a being Point of X
for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a}
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let a be Point of X; ::_thesis: for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a}
let b be Point of X0; ::_thesis: ( a = b implies r " (Cl {b}) = Cl {a} )
A2: b in {b} by TARSKI:def_1;
assume A3: a = b ; ::_thesis: r " (Cl {b}) = Cl {a}
then r . a = b by A1, BORSUK_1:def_16;
then A4: a in r " {b} by A2, FUNCT_2:38;
A5: A is maximal_T_0 by Th11;
A6: r " (Cl {b}) c= Cl {a}
proof
assume not r " (Cl {b}) c= Cl {a} ; ::_thesis: contradiction
then consider c being set such that
A7: c in r " (Cl {b}) and
A8: not c in Cl {a} by TARSKI:def_3;
reconsider c = c as Point of X by A7;
consider d being Point of X such that
A9: d in A and
A10: A /\ (MaxADSet c) = {d} by A5, Def6;
A11: {d} c= MaxADSet c by A10, XBOOLE_1:17;
r " (Cl {b}) is closed by PRE_TOPC:def_6;
then MaxADSet c c= r " (Cl {b}) by A7, TEX_4:23;
then {d} c= r " (Cl {b}) by A11, XBOOLE_1:1;
then A12: d in r " (Cl {b}) by ZFMISC_1:31;
reconsider e = d as Point of X0 by A9;
{c} c= MaxADSet c by TEX_4:18;
then A13: c in MaxADSet c by ZFMISC_1:31;
A14: Cl {b} c= Cl {a} by A3, TOPS_3:53;
r . d = e by A1, BORSUK_1:def_16;
then e in Cl {b} by A12, FUNCT_2:38;
then A15: MaxADSet d c= Cl {a} by A14, TEX_4:23;
d in MaxADSet c by A11, ZFMISC_1:31;
then MaxADSet d = MaxADSet c by TEX_4:21;
hence contradiction by A8, A13, A15; ::_thesis: verum
end;
A16: r " (Cl {b}) is closed by PRE_TOPC:def_6;
r " {b} c= r " (Cl {b}) by PRE_TOPC:18, RELAT_1:143;
then {a} c= r " (Cl {b}) by A4, ZFMISC_1:31;
then Cl {a} c= r " (Cl {b}) by A16, TOPS_1:5;
hence r " (Cl {b}) = Cl {a} by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm3: for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds
for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} )
assume A1: r is being_a_retraction ; ::_thesis: for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} )
reconsider N = A as Subset of X ;
assume A2: A = the carrier of X0 ; ::_thesis: for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
let a be Point of X; ::_thesis: A /\ (MaxADSet a) = {(r . a)}
A3: N is maximal_T_0 by A2, Th11;
then consider c being Point of X such that
A4: c in A and
A5: A /\ (MaxADSet a) = {c} by Def6;
A6: {c} c= MaxADSet c by TEX_4:18;
r . a in A by A2;
then reconsider d = r . a as Point of X ;
{(r . a)} c= Cl {(r . a)} by PRE_TOPC:18;
then A7: r . a in Cl {(r . a)} by ZFMISC_1:31;
{c} c= MaxADSet a by A5, XBOOLE_1:17;
then c in MaxADSet a by ZFMISC_1:31;
then A8: MaxADSet c = MaxADSet a by TEX_4:21;
reconsider b = c as Point of X0 by A2, A4;
A9: {a} c= MaxADSet a by TEX_4:18;
A10: r " (Cl {b}) = Cl {c} by A1, Lm2;
then {c} c= r " (Cl {b}) by PRE_TOPC:18;
then c in r " (Cl {b}) by ZFMISC_1:31;
then MaxADSet a c= r " (Cl {b}) by A10, A8, TEX_4:23;
then {a} c= r " (Cl {b}) by A9, XBOOLE_1:1;
then a in r " (Cl {b}) by ZFMISC_1:31;
then A11: r . a in Cl {b} by FUNCT_2:38;
r " (Cl {(r . a)}) = Cl {d} by A1, Lm2;
then a in Cl {d} by A7, FUNCT_2:38;
then MaxADSet c c= Cl {d} by A8, TEX_4:23;
then {c} c= Cl {d} by A6, XBOOLE_1:1;
then A12: Cl {c} c= Cl {d} by TOPS_1:5;
Cl {b} c= Cl {c} by TOPS_3:53;
then {d} c= Cl {c} by A11, ZFMISC_1:31;
then Cl {d} c= Cl {c} by TOPS_1:5;
then Cl {d} = Cl {c} by A12, XBOOLE_0:def_10;
then A13: MaxADSet d = MaxADSet a by A8, TEX_4:49;
N is T_0 by A3, Def4;
hence A /\ (MaxADSet a) = {(r . a)} by A2, A13, Def2; ::_thesis: verum
end;
Lm4: for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
MaxADSet a c= r " {b}
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
MaxADSet a c= r " {b}
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
MaxADSet a c= r " {b}
let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for a being Point of X
for b being Point of X0 st a = b holds
MaxADSet a c= r " {b} )
assume A1: r is being_a_retraction ; ::_thesis: for a being Point of X
for b being Point of X0 st a = b holds
MaxADSet a c= r " {b}
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let a be Point of X; ::_thesis: for b being Point of X0 st a = b holds
MaxADSet a c= r " {b}
let b be Point of X0; ::_thesis: ( a = b implies MaxADSet a c= r " {b} )
assume A2: a = b ; ::_thesis: MaxADSet a c= r " {b}
assume not MaxADSet a c= r " {b} ; ::_thesis: contradiction
then consider s being set such that
A3: s in MaxADSet a and
A4: not s in r " {b} by TARSKI:def_3;
reconsider s = s as Point of X by A3;
A5: MaxADSet a = MaxADSet s by A3, TEX_4:21;
A6: {s} c= MaxADSet s by TEX_4:18;
A7: r " (Cl {b}) = Cl {a} by A1, A2, Lm2;
then {a} c= r " (Cl {b}) by PRE_TOPC:18;
then a in r " (Cl {b}) by ZFMISC_1:31;
then MaxADSet s c= r " (Cl {b}) by A7, A5, TEX_4:23;
then {s} c= r " (Cl {b}) by A6, XBOOLE_1:1;
then s in r " (Cl {b}) by ZFMISC_1:31;
then A8: r . s in Cl {b} by FUNCT_2:38;
A c= the carrier of X ;
then reconsider d = r . s as Point of X by TARSKI:def_3;
{(r . s)} c= Cl {(r . s)} by PRE_TOPC:18;
then A9: r . s in Cl {(r . s)} by ZFMISC_1:31;
A10: {a} c= MaxADSet a by TEX_4:18;
r " (Cl {(r . s)}) = Cl {d} by A1, Lm2;
then s in Cl {d} by A9, FUNCT_2:38;
then MaxADSet a c= Cl {d} by A5, TEX_4:23;
then {a} c= Cl {d} by A10, XBOOLE_1:1;
then A11: Cl {a} c= Cl {d} by TOPS_1:5;
Cl {b} c= Cl {a} by A2, TOPS_3:53;
then {d} c= Cl {a} by A8, ZFMISC_1:31;
then Cl {d} c= Cl {a} by TOPS_1:5;
then Cl {d} = Cl {a} by A11, XBOOLE_0:def_10;
then A12: MaxADSet d = MaxADSet a by TEX_4:49;
A is maximal_T_0 by Th11;
then A13: A is T_0 by Def4;
r . a = b by A1, A2, BORSUK_1:def_16;
then A /\ (MaxADSet a) = {b} by A1, Lm3;
then {b} = {(r . s)} by A13, A12, Def2;
then r . s in {b} by ZFMISC_1:31;
hence contradiction by A4, FUNCT_2:38; ::_thesis: verum
end;
Lm5: for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a )
assume A1: r is being_a_retraction ; ::_thesis: for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let a be Point of X; ::_thesis: for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
let b be Point of X0; ::_thesis: ( a = b implies r " {b} = MaxADSet a )
assume A2: a = b ; ::_thesis: r " {b} = MaxADSet a
A3: r " {b} c= MaxADSet a
proof
assume not r " {b} c= MaxADSet a ; ::_thesis: contradiction
then consider s being set such that
A4: s in r " {b} and
A5: not s in MaxADSet a by TARSKI:def_3;
reconsider s = s as Point of X by A4;
r . s in {b} by A4, FUNCT_2:38;
then {(r . s)} c= {b} by ZFMISC_1:31;
then {(r . s)} = {b} by ZFMISC_1:18;
then A /\ (MaxADSet s) = {b} by A1, Lm3;
then {a} c= MaxADSet s by A2, XBOOLE_1:17;
then a in MaxADSet s by ZFMISC_1:31;
then A6: MaxADSet s = MaxADSet a by TEX_4:21;
{s} c= MaxADSet s by TEX_4:18;
hence contradiction by A5, A6, ZFMISC_1:31; ::_thesis: verum
end;
MaxADSet a c= r " {b} by A1, A2, Lm4;
hence r " {b} = MaxADSet a by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm6: for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for E being Subset of X
for F being Subset of X0 st F = E holds
r " F = MaxADSet E
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for E being Subset of X
for F being Subset of X0 st F = E holds
r " F = MaxADSet E
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds
for E being Subset of X
for F being Subset of X0 st F = E holds
r " F = MaxADSet E
let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for E being Subset of X
for F being Subset of X0 st F = E holds
r " F = MaxADSet E )
assume A1: r is being_a_retraction ; ::_thesis: for E being Subset of X
for F being Subset of X0 st F = E holds
r " F = MaxADSet E
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let E be Subset of X; ::_thesis: for F being Subset of X0 st F = E holds
r " F = MaxADSet E
let F be Subset of X0; ::_thesis: ( F = E implies r " F = MaxADSet E )
set R = { (MaxADSet a) where a is Point of X : a in E } ;
assume A2: F = E ; ::_thesis: r " F = MaxADSet E
now__::_thesis:_for_x_being_set_st_x_in_r_"_F_holds_
x_in_union__{__(MaxADSet_a)_where_a_is_Point_of_X_:_a_in_E__}_
let x be set ; ::_thesis: ( x in r " F implies x in union { (MaxADSet a) where a is Point of X : a in E } )
assume A3: x in r " F ; ::_thesis: x in union { (MaxADSet a) where a is Point of X : a in E }
then reconsider b = x as Point of X ;
A4: r . b in F by A3, FUNCT_2:38;
then reconsider a = r . b as Point of X by A2;
MaxADSet a in { (MaxADSet a) where a is Point of X : a in E } by A2, A4;
then A5: MaxADSet a c= union { (MaxADSet a) where a is Point of X : a in E } by ZFMISC_1:74;
A /\ (MaxADSet b) = {a} by A1, Lm3;
then a in A /\ (MaxADSet b) by ZFMISC_1:31;
then a in MaxADSet b by XBOOLE_0:def_4;
then A6: MaxADSet a = MaxADSet b by TEX_4:21;
{b} c= MaxADSet b by TEX_4:18;
then b in MaxADSet a by A6, ZFMISC_1:31;
hence x in union { (MaxADSet a) where a is Point of X : a in E } by A5; ::_thesis: verum
end;
then A7: r " F c= union { (MaxADSet a) where a is Point of X : a in E } by TARSKI:def_3;
A is maximal_T_0 by Th11;
then A8: A is T_0 by Def4;
now__::_thesis:_for_C_being_set_st_C_in__{__(MaxADSet_a)_where_a_is_Point_of_X_:_a_in_E__}__holds_
C_c=_r_"_F
let C be set ; ::_thesis: ( C in { (MaxADSet a) where a is Point of X : a in E } implies C c= r " F )
assume C in { (MaxADSet a) where a is Point of X : a in E } ; ::_thesis: C c= r " F
then consider a being Point of X such that
A9: C = MaxADSet a and
A10: a in E ;
now__::_thesis:_for_x_being_set_st_x_in_C_holds_
x_in_r_"_F
let x be set ; ::_thesis: ( x in C implies x in r " F )
assume A11: x in C ; ::_thesis: x in r " F
then reconsider b = x as Point of X by A9;
A12: A /\ (MaxADSet b) = {(r . b)} by A1, Lm3;
A13: A /\ (MaxADSet a) = {a} by A2, A8, A10, Def2;
MaxADSet a = MaxADSet b by A9, A11, TEX_4:21;
then a = r . x by A13, A12, ZFMISC_1:3;
hence x in r " F by A2, A9, A10, A11, FUNCT_2:38; ::_thesis: verum
end;
hence C c= r " F by TARSKI:def_3; ::_thesis: verum
end;
then A14: union { (MaxADSet a) where a is Point of X : a in E } c= r " F by ZFMISC_1:76;
MaxADSet E = union { (MaxADSet a) where a is Point of X : a in E } by TEX_4:def_11;
hence r " F = MaxADSet E by A14, A7, XBOOLE_0:def_10; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
let X0 be non empty maximal_Kolmogorov_subspace of X;
func Stone-retraction (X,X0) -> continuous Function of X,X0 means :Def9: :: TSP_2:def 9
it is being_a_retraction ;
existence
ex b1 being continuous Function of X,X0 st b1 is being_a_retraction by Th22;
uniqueness
for b1, b2 being continuous Function of X,X0 st b1 is being_a_retraction & b2 is being_a_retraction holds
b1 = b2
proof
reconsider M = the carrier of X0 as non empty Subset of X by TSEP_1:1;
let r1, r2 be continuous Function of X,X0; ::_thesis: ( r1 is being_a_retraction & r2 is being_a_retraction implies r1 = r2 )
assume that
A1: r1 is being_a_retraction and
A2: r2 is being_a_retraction ; ::_thesis: r1 = r2
for x being set st x in the carrier of X holds
r1 . x = r2 . x
proof
let x be set ; ::_thesis: ( x in the carrier of X implies r1 . x = r2 . x )
assume x in the carrier of X ; ::_thesis: r1 . x = r2 . x
then reconsider a = x as Point of X ;
A3: M /\ (MaxADSet a) = {(r2 . a)} by A2, Lm3;
M /\ (MaxADSet a) = {(r1 . a)} by A1, Lm3;
hence r1 . x = r2 . x by A3, ZFMISC_1:3; ::_thesis: verum
end;
hence r1 = r2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines Stone-retraction TSP_2:def_9_:_
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for b3 being continuous Function of X,X0 holds
( b3 = Stone-retraction (X,X0) iff b3 is being_a_retraction );
theorem :: TSP_2:24
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X
for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " (Cl {b}) = Cl {a}
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X
for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " (Cl {b}) = Cl {a}
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for a being Point of X
for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " (Cl {b}) = Cl {a}
let a be Point of X; ::_thesis: for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " (Cl {b}) = Cl {a}
let b be Point of X0; ::_thesis: ( a = b implies (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} )
assume A1: a = b ; ::_thesis: (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a}
Stone-retraction (X,X0) is being_a_retraction by Def9;
hence (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} by A1, Lm2; ::_thesis: verum
end;
theorem Th25: :: TSP_2:25
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X
for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " {b} = MaxADSet a
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X
for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " {b} = MaxADSet a
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for a being Point of X
for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " {b} = MaxADSet a
let a be Point of X; ::_thesis: for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " {b} = MaxADSet a
let b be Point of X0; ::_thesis: ( a = b implies (Stone-retraction (X,X0)) " {b} = MaxADSet a )
assume A1: a = b ; ::_thesis: (Stone-retraction (X,X0)) " {b} = MaxADSet a
Stone-retraction (X,X0) is being_a_retraction by Def9;
hence (Stone-retraction (X,X0)) " {b} = MaxADSet a by A1, Lm5; ::_thesis: verum
end;
theorem Th26: :: TSP_2:26
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for E being Subset of X
for F being Subset of X0 st F = E holds
(Stone-retraction (X,X0)) " F = MaxADSet E
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for E being Subset of X
for F being Subset of X0 st F = E holds
(Stone-retraction (X,X0)) " F = MaxADSet E
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for E being Subset of X
for F being Subset of X0 st F = E holds
(Stone-retraction (X,X0)) " F = MaxADSet E
let E be Subset of X; ::_thesis: for F being Subset of X0 st F = E holds
(Stone-retraction (X,X0)) " F = MaxADSet E
let F be Subset of X0; ::_thesis: ( F = E implies (Stone-retraction (X,X0)) " F = MaxADSet E )
assume A1: F = E ; ::_thesis: (Stone-retraction (X,X0)) " F = MaxADSet E
Stone-retraction (X,X0) is being_a_retraction by Def9;
hence (Stone-retraction (X,X0)) " F = MaxADSet E by A1, Lm6; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
let X0 be non empty maximal_Kolmogorov_subspace of X;
redefine func Stone-retraction (X,X0) means :Def10: :: TSP_2:def 10
for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(it . a)};
compatibility
for b1 being continuous Function of X,X0 holds
( b1 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(b1 . a)} )
proof
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
let r be continuous Function of X,X0; ::_thesis: ( r = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} )
thus ( r = Stone-retraction (X,X0) implies for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) ::_thesis: ( ( for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) implies r = Stone-retraction (X,X0) )
proof
assume A1: r = Stone-retraction (X,X0) ; ::_thesis: for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)}
let M be Subset of X; ::_thesis: ( M = the carrier of X0 implies for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} )
A2: Stone-retraction (X,X0) is being_a_retraction by Def9;
assume M = the carrier of X0 ; ::_thesis: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)}
hence for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} by A1, A2, Lm3; ::_thesis: verum
end;
assume for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} ; ::_thesis: r = Stone-retraction (X,X0)
then for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ;
then r is being_a_retraction by Th20;
hence r = Stone-retraction (X,X0) by Def9; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines Stone-retraction TSP_2:def_10_:_
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for b3 being continuous Function of X,X0 holds
( b3 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(b3 . a)} );
definition
let X be non empty TopSpace;
let X0 be non empty maximal_Kolmogorov_subspace of X;
redefine func Stone-retraction (X,X0) means :Def11: :: TSP_2:def 11
for a being Point of X holds it . a in MaxADSet a;
compatibility
for b1 being continuous Function of X,X0 holds
( b1 = Stone-retraction (X,X0) iff for a being Point of X holds b1 . a in MaxADSet a )
proof
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let r be continuous Function of X,X0; ::_thesis: ( r = Stone-retraction (X,X0) iff for a being Point of X holds r . a in MaxADSet a )
thus ( r = Stone-retraction (X,X0) implies for a being Point of X holds r . a in MaxADSet a ) ::_thesis: ( ( for a being Point of X holds r . a in MaxADSet a ) implies r = Stone-retraction (X,X0) )
proof
assume A1: r = Stone-retraction (X,X0) ; ::_thesis: for a being Point of X holds r . a in MaxADSet a
let a be Point of X; ::_thesis: r . a in MaxADSet a
A /\ (MaxADSet a) = {(r . a)} by A1, Def10;
then {(r . a)} c= MaxADSet a by XBOOLE_1:17;
hence r . a in MaxADSet a by ZFMISC_1:31; ::_thesis: verum
end;
assume for a being Point of X holds r . a in MaxADSet a ; ::_thesis: r = Stone-retraction (X,X0)
then r is being_a_retraction by Th21;
hence r = Stone-retraction (X,X0) by Def9; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines Stone-retraction TSP_2:def_11_:_
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for b3 being continuous Function of X,X0 holds
( b3 = Stone-retraction (X,X0) iff for a being Point of X holds b3 . a in MaxADSet a );
theorem Th27: :: TSP_2:27
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a
let a be Point of X; ::_thesis: (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
set r = Stone-retraction (X,X0);
(Stone-retraction (X,X0)) . a in A ;
then reconsider b = (Stone-retraction (X,X0)) . a as Point of X ;
A1: (Stone-retraction (X,X0)) . a in MaxADSet a by Def11;
(Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet b by Th25;
hence (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a by A1, TEX_4:21; ::_thesis: verum
end;
theorem :: TSP_2:28
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X holds Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a)
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X holds Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a)
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for a being Point of X holds Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a)
let a be Point of X; ::_thesis: Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a)
set r = Stone-retraction (X,X0);
A1: dom (Stone-retraction (X,X0)) = [#] X by FUNCT_2:def_1;
A2: (Stone-retraction (X,X0)) .: ((Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)}) c= {((Stone-retraction (X,X0)) . a)} by FUNCT_1:75;
A3: (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a by Th27;
then (Stone-retraction (X,X0)) .: ((Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)}) <> {} by A1, RELAT_1:119;
then (Stone-retraction (X,X0)) .: ((Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)}) = {((Stone-retraction (X,X0)) . a)} by A2, ZFMISC_1:33;
hence Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a) by A1, A3, FUNCT_1:59; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
let X0 be non empty maximal_Kolmogorov_subspace of X;
redefine func Stone-retraction (X,X0) means :Def12: :: TSP_2:def 12
for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = it .: A;
compatibility
for b1 being continuous Function of X,X0 holds
( b1 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = b1 .: A )
proof
let r be continuous Function of X,X0; ::_thesis: ( r = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = r .: A )
thus ( r = Stone-retraction (X,X0) implies for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = r .: A ) ::_thesis: ( ( for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = r .: A ) implies r = Stone-retraction (X,X0) )
proof
assume A1: r = Stone-retraction (X,X0) ; ::_thesis: for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = r .: A
let M be Subset of X; ::_thesis: ( M = the carrier of X0 implies for A being Subset of X holds M /\ (MaxADSet A) = r .: A )
reconsider N = M as Subset of X ;
assume A2: M = the carrier of X0 ; ::_thesis: for A being Subset of X holds M /\ (MaxADSet A) = r .: A
let A be Subset of X; ::_thesis: M /\ (MaxADSet A) = r .: A
N is maximal_T_0 by A2, Th11;
then A3: N is T_0 by Def4;
for x being set st x in M /\ (MaxADSet A) holds
x in r .: A
proof
let x be set ; ::_thesis: ( x in M /\ (MaxADSet A) implies x in r .: A )
assume A4: x in M /\ (MaxADSet A) ; ::_thesis: x in r .: A
then reconsider c = x as Point of X ;
c in M by A4, XBOOLE_0:def_4;
then A5: M /\ (MaxADSet c) = {c} by A3, Def2;
c in MaxADSet A by A4, XBOOLE_0:def_4;
then c in union { (MaxADSet a) where a is Point of X : a in A } by TEX_4:def_11;
then consider D being set such that
A6: c in D and
A7: D in { (MaxADSet a) where a is Point of X : a in A } by TARSKI:def_4;
consider a being Point of X such that
A8: D = MaxADSet a and
A9: a in A by A7;
MaxADSet c = MaxADSet a by A6, A8, TEX_4:21;
then {(r . a)} = {c} by A1, A2, A5, Def10;
hence x in r .: A by A9, FUNCT_2:35, ZFMISC_1:3; ::_thesis: verum
end;
then A10: M /\ (MaxADSet A) c= r .: A by TARSKI:def_3;
for x being set st x in r .: A holds
x in M /\ (MaxADSet A)
proof
let x be set ; ::_thesis: ( x in r .: A implies x in M /\ (MaxADSet A) )
assume A11: x in r .: A ; ::_thesis: x in M /\ (MaxADSet A)
then reconsider b = x as Point of X0 ;
consider a being set such that
A12: a in the carrier of X and
A13: a in A and
A14: b = r . a by A11, FUNCT_2:64;
reconsider a = a as Point of X by A12;
{a} c= A by A13, ZFMISC_1:31;
then MaxADSet {a} c= MaxADSet A by TEX_4:31;
then MaxADSet a c= MaxADSet A by TEX_4:28;
then A15: M /\ (MaxADSet a) c= M /\ (MaxADSet A) by XBOOLE_1:26;
M /\ (MaxADSet a) = {b} by A1, A2, A14, Def10;
hence x in M /\ (MaxADSet A) by A15, ZFMISC_1:31; ::_thesis: verum
end;
then r .: A c= M /\ (MaxADSet A) by TARSKI:def_3;
hence M /\ (MaxADSet A) = r .: A by A10, XBOOLE_0:def_10; ::_thesis: verum
end;
assume A16: for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = r .: A ; ::_thesis: r = Stone-retraction (X,X0)
A17: dom r = [#] X by FUNCT_2:def_1;
for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)}
proof
let M be Subset of X; ::_thesis: ( M = the carrier of X0 implies for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} )
assume A18: M = the carrier of X0 ; ::_thesis: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)}
let a be Point of X; ::_thesis: M /\ (MaxADSet a) = {(r . a)}
M /\ (MaxADSet {a}) = Im (r,a) by A16, A18;
then M /\ (MaxADSet a) = Im (r,a) by TEX_4:28;
hence M /\ (MaxADSet a) = {(r . a)} by A17, FUNCT_1:59; ::_thesis: verum
end;
hence r = Stone-retraction (X,X0) by Def10; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines Stone-retraction TSP_2:def_12_:_
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for b3 being continuous Function of X,X0 holds
( b3 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = b3 .: A );
theorem Th29: :: TSP_2:29
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X holds (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X holds (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A being Subset of X holds (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A
let A be Subset of X; ::_thesis: (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A
reconsider C = the carrier of X0 as non empty Subset of X by TSEP_1:1;
set r = Stone-retraction (X,X0);
C c= the carrier of X ;
then reconsider B = (Stone-retraction (X,X0)) .: A as Subset of X by XBOOLE_1:1;
C /\ (MaxADSet A) = B by Def12;
then A1: B c= MaxADSet A by XBOOLE_1:17;
A2: (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet B by Th26;
then A c= MaxADSet B by FUNCT_2:42;
hence (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A by A2, A1, TEX_4:35; ::_thesis: verum
end;
theorem :: TSP_2:30
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X holds (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A)
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X holds (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A)
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A being Subset of X holds (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A)
let A be Subset of X; ::_thesis: (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A)
set r = Stone-retraction (X,X0);
A1: rng (Stone-retraction (X,X0)) = (Stone-retraction (X,X0)) .: the carrier of X by RELSET_1:22;
(Stone-retraction (X,X0)) .: ((Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A)) = (Stone-retraction (X,X0)) .: (MaxADSet A) by Th29;
hence (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A) by A1, FUNCT_1:77, RELAT_1:123; ::_thesis: verum
end;
theorem :: TSP_2:31
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A, B being Subset of X holds (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B)
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A, B being Subset of X holds (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B)
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A, B being Subset of X holds (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B)
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set r = Stone-retraction (X,X0);
let A, B be Subset of X; ::_thesis: (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B)
(Stone-retraction (X,X0)) .: (A \/ B) = M /\ (MaxADSet (A \/ B)) by Def12
.= M /\ ((MaxADSet A) \/ (MaxADSet B)) by TEX_4:36
.= (M /\ (MaxADSet A)) \/ (M /\ (MaxADSet B)) by XBOOLE_1:23
.= ((Stone-retraction (X,X0)) .: A) \/ (M /\ (MaxADSet B)) by Def12
.= ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B) by Def12 ;
hence (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B) ; ::_thesis: verum
end;
theorem :: TSP_2:32
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A, B being Subset of X st ( A is open or B is open ) holds
(Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A, B being Subset of X st ( A is open or B is open ) holds
(Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A, B being Subset of X st ( A is open or B is open ) holds
(Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set r = Stone-retraction (X,X0);
let A, B be Subset of X; ::_thesis: ( ( A is open or B is open ) implies (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) )
assume A1: ( A is open or B is open ) ; ::_thesis: (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)
(Stone-retraction (X,X0)) .: (A /\ B) = M /\ (MaxADSet (A /\ B)) by Def12
.= (M /\ M) /\ ((MaxADSet A) /\ (MaxADSet B)) by A1, TEX_4:65
.= M /\ (M /\ ((MaxADSet A) /\ (MaxADSet B))) by XBOOLE_1:16
.= ((M /\ (MaxADSet A)) /\ (MaxADSet B)) /\ M by XBOOLE_1:16
.= (M /\ (MaxADSet A)) /\ (M /\ (MaxADSet B)) by XBOOLE_1:16
.= ((Stone-retraction (X,X0)) .: A) /\ (M /\ (MaxADSet B)) by Def12
.= ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) by Def12 ;
hence (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) ; ::_thesis: verum
end;
theorem :: TSP_2:33
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A, B being Subset of X st ( A is closed or B is closed ) holds
(Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A, B being Subset of X st ( A is closed or B is closed ) holds
(Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A, B being Subset of X st ( A is closed or B is closed ) holds
(Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set r = Stone-retraction (X,X0);
let A, B be Subset of X; ::_thesis: ( ( A is closed or B is closed ) implies (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) )
assume A1: ( A is closed or B is closed ) ; ::_thesis: (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)
(Stone-retraction (X,X0)) .: (A /\ B) = M /\ (MaxADSet (A /\ B)) by Def12
.= (M /\ M) /\ ((MaxADSet A) /\ (MaxADSet B)) by A1, TEX_4:64
.= M /\ (M /\ ((MaxADSet A) /\ (MaxADSet B))) by XBOOLE_1:16
.= ((M /\ (MaxADSet A)) /\ (MaxADSet B)) /\ M by XBOOLE_1:16
.= (M /\ (MaxADSet A)) /\ (M /\ (MaxADSet B)) by XBOOLE_1:16
.= ((Stone-retraction (X,X0)) .: A) /\ (M /\ (MaxADSet B)) by Def12
.= ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) by Def12 ;
hence (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) ; ::_thesis: verum
end;
theorem :: TSP_2:34
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X st A is open holds
(Stone-retraction (X,X0)) .: A is open
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X st A is open holds
(Stone-retraction (X,X0)) .: A is open
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A being Subset of X st A is open holds
(Stone-retraction (X,X0)) .: A is open
let A be Subset of X; ::_thesis: ( A is open implies (Stone-retraction (X,X0)) .: A is open )
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set B = (Stone-retraction (X,X0)) .: A;
assume A1: A is open ; ::_thesis: (Stone-retraction (X,X0)) .: A is open
then A = MaxADSet A by TEX_4:56;
then A /\ M = (Stone-retraction (X,X0)) .: A by Def12;
hence (Stone-retraction (X,X0)) .: A is open by A1, TSP_1:def_1; ::_thesis: verum
end;
theorem :: TSP_2:35
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X st A is closed holds
(Stone-retraction (X,X0)) .: A is closed
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X st A is closed holds
(Stone-retraction (X,X0)) .: A is closed
let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A being Subset of X st A is closed holds
(Stone-retraction (X,X0)) .: A is closed
let A be Subset of X; ::_thesis: ( A is closed implies (Stone-retraction (X,X0)) .: A is closed )
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set B = (Stone-retraction (X,X0)) .: A;
assume A1: A is closed ; ::_thesis: (Stone-retraction (X,X0)) .: A is closed
then A = MaxADSet A by TEX_4:60;
then A /\ M = (Stone-retraction (X,X0)) .: A by Def12;
hence (Stone-retraction (X,X0)) .: A is closed by A1, TSP_1:def_2; ::_thesis: verum
end;