:: TEX_2 semantic presentation
begin
theorem Th1: :: TEX_2:1
for A being non empty set
for B being 1 -element set st A c= B holds
A = B
proof
let A be non empty set ; ::_thesis: for B being 1 -element set st A c= B holds
A = B
let B be 1 -element set ; ::_thesis: ( A c= B implies A = B )
assume A1: A c= B ; ::_thesis: A = B
ex s being Element of B st B = {s} by SUBSET_1:46;
hence A = B by A1, ZFMISC_1:33; ::_thesis: verum
end;
theorem :: TEX_2:2
for A being 1 -element set
for B being set st not A /\ B is empty holds
A c= B
proof
let A be 1 -element set ; ::_thesis: for B being set st not A /\ B is empty holds
A c= B
let B be set ; ::_thesis: ( not A /\ B is empty implies A c= B )
A1: A /\ B c= B by XBOOLE_1:17;
assume not A /\ B is empty ; ::_thesis: A c= B
then consider a being set such that
A2: a in A /\ B by XBOOLE_0:def_1;
A3: ex s being Element of A st A = {s} by SUBSET_1:46;
A /\ B c= A by XBOOLE_1:17;
then {a} c= A by A2, ZFMISC_1:31;
then {a} = A by A3, ZFMISC_1:18;
hence A c= B by A2, A1, ZFMISC_1:31; ::_thesis: verum
end;
registration
let S be 1 -element set ;
cluster proper -> empty for Element of bool S;
coherence
for b1 being Subset of S st b1 is proper holds
b1 is empty
proof
let A be Subset of S; ::_thesis: ( A is proper implies A is empty )
assume A is proper ; ::_thesis: A is empty
then A1: A <> S by SUBSET_1:def_6;
ex s being Element of S st S = {s} by SUBSET_1:46;
hence A is empty by A1, ZFMISC_1:33; ::_thesis: verum
end;
cluster non empty -> non proper for Element of bool S;
coherence
for b1 being Subset of S st not b1 is empty holds
not b1 is proper ;
end;
theorem :: TEX_2:3
for S being non empty set
for y being Element of S st {y} is proper holds
not S is trivial ;
theorem :: TEX_2:4
for S being non trivial set
for y being Element of S holds {y} is proper by SUBSET_1:def_6;
registration
let S be 1 -element set ;
cluster non empty non proper -> non empty trivial for Element of bool S;
coherence
for b1 being non empty Subset of S st not b1 is proper holds
b1 is trivial ;
end;
registration
let S be non trivial set ;
cluster non empty trivial -> non empty proper for Element of bool S;
coherence
for b1 being non empty Subset of S st b1 is trivial holds
b1 is proper by SUBSET_1:def_6;
cluster non empty non proper -> non empty non trivial for Element of bool S;
coherence
for b1 being non empty Subset of S st not b1 is proper holds
not b1 is trivial ;
end;
registration
let S be non trivial set ;
cluster non empty trivial proper for Element of bool S;
existence
ex b1 being non empty Subset of S st
( b1 is trivial & b1 is proper )
proof
set A = the non empty trivial Subset of S;
take the non empty trivial Subset of S ; ::_thesis: ( the non empty trivial Subset of S is trivial & the non empty trivial Subset of S is proper )
thus ( the non empty trivial Subset of S is trivial & the non empty trivial Subset of S is proper ) ; ::_thesis: verum
end;
cluster non empty non trivial non proper for Element of bool S;
existence
ex b1 being non empty Subset of S st
( not b1 is trivial & not b1 is proper )
proof
take [#] S ; ::_thesis: ( not [#] S is trivial & not [#] S is proper )
thus ( not [#] S is trivial & not [#] S is proper ) ; ::_thesis: verum
end;
end;
theorem :: TEX_2:5
for Y being non empty 1-sorted
for y being Element of Y st {y} is proper holds
not Y is trivial ;
theorem :: TEX_2:6
for Y being non trivial 1-sorted
for y being Element of Y holds {y} is proper ;
registration
let Y be 1 -element 1-sorted ;
cluster non empty -> non empty non proper for Element of bool the carrier of Y;
coherence
for b1 being non empty Subset of Y holds not b1 is proper ;
cluster non empty non proper -> non empty trivial for Element of bool the carrier of Y;
coherence
for b1 being non empty Subset of Y st not b1 is proper holds
b1 is trivial ;
end;
registration
let Y be non trivial 1-sorted ;
cluster non empty trivial -> non empty proper for Element of bool the carrier of Y;
coherence
for b1 being non empty Subset of Y st b1 is trivial holds
b1 is proper ;
cluster non empty non proper -> non empty non trivial for Element of bool the carrier of Y;
coherence
for b1 being non empty Subset of Y st not b1 is proper holds
not b1 is trivial ;
end;
registration
let Y be non trivial 1-sorted ;
cluster non empty trivial proper for Element of bool the carrier of Y;
existence
ex b1 being non empty Subset of Y st
( b1 is trivial & b1 is proper )
proof
set A = the non empty trivial Subset of Y;
take the non empty trivial Subset of Y ; ::_thesis: ( the non empty trivial Subset of Y is trivial & the non empty trivial Subset of Y is proper )
thus ( the non empty trivial Subset of Y is trivial & the non empty trivial Subset of Y is proper ) ; ::_thesis: verum
end;
cluster non empty non trivial non proper for Element of bool the carrier of Y;
existence
ex b1 being non empty Subset of Y st
( not b1 is trivial & not b1 is proper )
proof
take [#] Y ; ::_thesis: ( not [#] Y is trivial & not [#] Y is proper )
thus ( not [#] Y is trivial & not [#] Y is proper ) ; ::_thesis: verum
end;
end;
registration
let Y be non trivial 1-sorted ;
cluster non empty trivial proper for Element of bool the carrier of Y;
existence
ex b1 being Subset of Y st
( not b1 is empty & b1 is trivial & b1 is proper )
proof
set X = the non empty trivial proper Subset of Y;
reconsider X = the non empty trivial proper Subset of Y as Subset of Y ;
take X ; ::_thesis: ( not X is empty & X is trivial & X is proper )
thus ( not X is empty & X is trivial & X is proper ) ; ::_thesis: verum
end;
end;
registration
let X be non empty set ;
let A be proper Subset of X;
clusterA ` -> non empty ;
coherence
not A ` is empty
proof
assume A ` is empty ; ::_thesis: contradiction
then (A `) ` = X ;
hence contradiction by SUBSET_1:def_6; ::_thesis: verum
end;
end;
begin
theorem :: TEX_2:7
for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is TopSpace-like holds
Y1 is TopSpace-like
proof
let Y0, Y1 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is TopSpace-like implies Y1 is TopSpace-like )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not Y0 is TopSpace-like or Y1 is TopSpace-like )
assume A2: Y0 is TopSpace-like ; ::_thesis: Y1 is TopSpace-like
hence the carrier of Y1 in the topology of Y1 by A1, PRE_TOPC:def_1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of Y1) holds
( not b1 c= the topology of Y1 or union b1 in the topology of Y1 ) ) & ( for b1, b2 being Element of bool the carrier of Y1 holds
( not b1 in the topology of Y1 or not b2 in the topology of Y1 or b1 /\ b2 in the topology of Y1 ) ) )
thus ( ( for b1 being Element of bool (bool the carrier of Y1) holds
( not b1 c= the topology of Y1 or union b1 in the topology of Y1 ) ) & ( for b1, b2 being Element of bool the carrier of Y1 holds
( not b1 in the topology of Y1 or not b2 in the topology of Y1 or b1 /\ b2 in the topology of Y1 ) ) ) by A1, A2, PRE_TOPC:def_1; ::_thesis: verum
end;
definition
let Y be TopStruct ;
let IT be SubSpace of Y;
attrIT is proper means :Def1: :: TEX_2:def 1
for A being Subset of Y st A = the carrier of IT holds
A is proper ;
end;
:: deftheorem Def1 defines proper TEX_2:def_1_:_
for Y being TopStruct
for IT being SubSpace of Y holds
( IT is proper iff for A being Subset of Y st A = the carrier of IT holds
A is proper );
theorem Th8: :: TEX_2:8
for Y being TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is proper iff Y0 is proper )
proof
let Y be TopStruct ; ::_thesis: for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is proper iff Y0 is proper )
let Y0 be SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 holds
( A is proper iff Y0 is proper )
let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 implies ( A is proper iff Y0 is proper ) )
assume A1: A = the carrier of Y0 ; ::_thesis: ( A is proper iff Y0 is proper )
hereby ::_thesis: ( Y0 is proper implies A is proper )
assume A is proper ; ::_thesis: Y0 is proper
then for A being Subset of Y st A = the carrier of Y0 holds
A is proper by A1;
hence Y0 is proper by Def1; ::_thesis: verum
end;
thus ( Y0 is proper implies A is proper ) by A1, Def1; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_Z_being_TopStruct_
for_Z0_being_SubSpace_of_Z_holds_the_carrier_of_Z0_is_Subset_of_Z
let Z be TopStruct ; ::_thesis: for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z
let Z0 be SubSpace of Z; ::_thesis: the carrier of Z0 is Subset of Z
[#] Z0 c= [#] Z by PRE_TOPC:def_4;
hence the carrier of Z0 is Subset of Z ; ::_thesis: verum
end;
theorem :: TEX_2:9
for Y being TopStruct
for Y0, Y1 being SubSpace of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is proper holds
Y1 is proper
proof
let Y be TopStruct ; ::_thesis: for Y0, Y1 being SubSpace of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is proper holds
Y1 is proper
let Y0, Y1 be SubSpace of Y; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is proper implies Y1 is proper )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not Y0 is proper or Y1 is proper )
assume Y0 is proper ; ::_thesis: Y1 is proper
then for A being Subset of Y st A = the carrier of Y1 holds
A is proper by A1, Def1;
hence Y1 is proper by Def1; ::_thesis: verum
end;
theorem Th10: :: TEX_2:10
for Y being TopStruct
for Y0 being SubSpace of Y st the carrier of Y0 = the carrier of Y holds
not Y0 is proper
proof
let Y be TopStruct ; ::_thesis: for Y0 being SubSpace of Y st the carrier of Y0 = the carrier of Y holds
not Y0 is proper
let Y0 be SubSpace of Y; ::_thesis: ( the carrier of Y0 = the carrier of Y implies not Y0 is proper )
reconsider A = the carrier of Y0 as Subset of Y by Lm1;
assume A1: the carrier of Y0 = the carrier of Y ; ::_thesis: not Y0 is proper
now__::_thesis:_ex_A_being_Subset_of_Y_st_
(_A_=_the_carrier_of_Y0_&_not_A_is_proper_)
take A = A; ::_thesis: ( A = the carrier of Y0 & not A is proper )
thus ( A = the carrier of Y0 & not A is proper ) by A1, SUBSET_1:def_6; ::_thesis: verum
end;
hence not Y0 is proper by Def1; ::_thesis: verum
end;
registration
let Y be 1 -element TopStruct ;
cluster non empty -> non empty non proper for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y holds not b1 is proper
proof
let Y0 be non empty SubSpace of Y; ::_thesis: not Y0 is proper
reconsider A = the carrier of Y0 as non empty Subset of Y by Lm1;
now__::_thesis:_ex_A_being_non_empty_Subset_of_Y_st_
(_A_=_the_carrier_of_Y0_&_not_A_is_proper_)
take A = A; ::_thesis: ( A = the carrier of Y0 & not A is proper )
thus ( A = the carrier of Y0 & not A is proper ) ; ::_thesis: verum
end;
hence not Y0 is proper by Def1; ::_thesis: verum
end;
cluster non empty non proper -> non empty trivial for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st not b1 is proper holds
b1 is trivial
proof
let Y0 be non empty SubSpace of Y; ::_thesis: ( not Y0 is proper implies Y0 is trivial )
assume not Y0 is proper ; ::_thesis: Y0 is trivial
ex A being Subset of Y st
( A = the carrier of Y0 & not A is proper ) by Def1;
then reconsider A = the carrier of Y0 as non empty Subset of Y ;
A is trivial ;
hence Y0 is trivial ; ::_thesis: verum
end;
end;
registration
let Y be non trivial TopStruct ;
cluster non empty trivial -> non empty proper for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is trivial holds
b1 is proper
proof
let Y0 be non empty SubSpace of Y; ::_thesis: ( Y0 is trivial implies Y0 is proper )
assume Y0 is trivial ; ::_thesis: Y0 is proper
then for A being Subset of Y st A = the carrier of Y0 holds
A is proper ;
hence Y0 is proper by Def1; ::_thesis: verum
end;
cluster non empty non proper -> non empty non trivial for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st not b1 is proper holds
not b1 is trivial ;
end;
registration
let Y be non empty TopStruct ;
cluster non empty strict non proper for SubSpace of Y;
existence
ex b1 being SubSpace of Y st
( not b1 is proper & b1 is strict & not b1 is empty )
proof
[#] Y = the carrier of Y ;
then reconsider A0 = the carrier of Y as non empty Subset of Y ;
set Y0 = Y | A0;
take Y | A0 ; ::_thesis: ( not Y | A0 is proper & Y | A0 is strict & not Y | A0 is empty )
A0 = [#] (Y | A0) by PRE_TOPC:def_5;
hence ( not Y | A0 is proper & Y | A0 is strict & not Y | A0 is empty ) by Th10; ::_thesis: verum
end;
end;
theorem :: TEX_2:11
for Y being non empty TopStruct
for Y0 being non proper SubSpace of Y holds TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #)
proof
let Y be non empty TopStruct ; ::_thesis: for Y0 being non proper SubSpace of Y holds TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #)
let Y0 be non proper SubSpace of Y; ::_thesis: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #)
A1: ex A being Subset of Y st
( A = the carrier of Y0 & not A is proper ) by Def1;
now__::_thesis:_for_D_being_set_st_D_in_the_topology_of_Y_holds_
D_in_the_topology_of_Y0
let D be set ; ::_thesis: ( D in the topology of Y implies D in the topology of Y0 )
assume A2: D in the topology of Y ; ::_thesis: D in the topology of Y0
then reconsider E = D as Subset of Y ;
reconsider C = E as Subset of Y0 by A1, SUBSET_1:def_6;
now__::_thesis:_ex_E_being_Subset_of_Y_st_
(_E_in_the_topology_of_Y_&_C_=_E_/\_([#]_Y0)_)
take E = E; ::_thesis: ( E in the topology of Y & C = E /\ ([#] Y0) )
thus ( E in the topology of Y & C = E /\ ([#] Y0) ) by A2, XBOOLE_1:28; ::_thesis: verum
end;
hence D in the topology of Y0 by PRE_TOPC:def_4; ::_thesis: verum
end;
then A3: the topology of Y c= the topology of Y0 by TARSKI:def_3;
A4: the carrier of Y0 = the carrier of Y by A1, SUBSET_1:def_6;
now__::_thesis:_for_D_being_set_st_D_in_the_topology_of_Y0_holds_
D_in_the_topology_of_Y
let D be set ; ::_thesis: ( D in the topology of Y0 implies D in the topology of Y )
assume A5: D in the topology of Y0 ; ::_thesis: D in the topology of Y
then reconsider C = D as Subset of Y0 ;
ex E being Subset of Y st
( E in the topology of Y & C = E /\ ([#] Y0) ) by A5, PRE_TOPC:def_4;
hence D in the topology of Y by A4, XBOOLE_1:28; ::_thesis: verum
end;
then the topology of Y0 c= the topology of Y by TARSKI:def_3;
then the topology of Y0 = the topology of Y by A3, XBOOLE_0:def_10;
hence TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #) by A1, SUBSET_1:def_6; ::_thesis: verum
end;
registration
let Y be non empty TopStruct ;
cluster discrete -> TopSpace-like for SubSpace of Y;
coherence
for b1 being SubSpace of Y st b1 is discrete holds
b1 is TopSpace-like ;
cluster anti-discrete -> TopSpace-like for SubSpace of Y;
coherence
for b1 being SubSpace of Y st b1 is anti-discrete holds
b1 is TopSpace-like ;
cluster non TopSpace-like -> non discrete for SubSpace of Y;
coherence
for b1 being SubSpace of Y st not b1 is TopSpace-like holds
not b1 is discrete ;
cluster non TopSpace-like -> non anti-discrete for SubSpace of Y;
coherence
for b1 being SubSpace of Y st not b1 is TopSpace-like holds
not b1 is anti-discrete ;
end;
theorem Th12: :: TEX_2:12
for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is discrete holds
Y1 is discrete
proof
let Y0, Y1 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is discrete implies Y1 is discrete )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not Y0 is discrete or Y1 is discrete )
assume Y0 is discrete ; ::_thesis: Y1 is discrete
then the topology of Y0 = bool the carrier of Y0 by TDLAT_3:def_1;
hence Y1 is discrete by A1, TDLAT_3:def_1; ::_thesis: verum
end;
theorem :: TEX_2:13
for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is anti-discrete holds
Y1 is anti-discrete
proof
let Y0, Y1 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is anti-discrete implies Y1 is anti-discrete )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not Y0 is anti-discrete or Y1 is anti-discrete )
assume Y0 is anti-discrete ; ::_thesis: Y1 is anti-discrete
then the topology of Y0 = {{}, the carrier of Y0} by TDLAT_3:def_2;
hence Y1 is anti-discrete by A1, TDLAT_3:def_2; ::_thesis: verum
end;
registration
let Y be non empty TopStruct ;
cluster discrete -> almost_discrete for SubSpace of Y;
coherence
for b1 being SubSpace of Y st b1 is discrete holds
b1 is almost_discrete ;
cluster non almost_discrete -> non discrete for SubSpace of Y;
coherence
for b1 being SubSpace of Y st not b1 is almost_discrete holds
not b1 is discrete ;
cluster anti-discrete -> almost_discrete for SubSpace of Y;
coherence
for b1 being SubSpace of Y st b1 is anti-discrete holds
b1 is almost_discrete ;
cluster non almost_discrete -> non anti-discrete for SubSpace of Y;
coherence
for b1 being SubSpace of Y st not b1 is almost_discrete holds
not b1 is anti-discrete ;
end;
theorem :: TEX_2:14
for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is almost_discrete holds
Y1 is almost_discrete
proof
let Y0, Y1 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is almost_discrete implies Y1 is almost_discrete )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not Y0 is almost_discrete or Y1 is almost_discrete )
assume Y0 is almost_discrete ; ::_thesis: Y1 is almost_discrete
then for A being Subset of Y0 st A in the topology of Y0 holds
the carrier of Y0 \ A in the topology of Y0 by TDLAT_3:def_3;
hence Y1 is almost_discrete by A1, TDLAT_3:def_3; ::_thesis: verum
end;
registration
let Y be non empty TopStruct ;
cluster non empty discrete anti-discrete -> non empty trivial for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is discrete & b1 is anti-discrete holds
b1 is trivial ;
cluster non empty non trivial anti-discrete -> non empty non discrete for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is anti-discrete & not b1 is trivial holds
not b1 is discrete ;
cluster non empty non trivial discrete -> non empty non anti-discrete for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is discrete & not b1 is trivial holds
not b1 is anti-discrete ;
end;
definition
let Y be non empty TopStruct ;
let y be Point of Y;
func Sspace y -> non empty strict SubSpace of Y means :Def2: :: TEX_2:def 2
the carrier of it = {y};
existence
ex b1 being non empty strict SubSpace of Y st the carrier of b1 = {y}
proof
reconsider D = {y} as non empty Subset of Y ;
set Y0 = Y | D;
take Y | D ; ::_thesis: the carrier of (Y | D) = {y}
D = [#] (Y | D) by PRE_TOPC:def_5;
hence the carrier of (Y | D) = {y} ; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict SubSpace of Y st the carrier of b1 = {y} & the carrier of b2 = {y} holds
b1 = b2
proof
let Y1, Y2 be non empty strict SubSpace of Y; ::_thesis: ( the carrier of Y1 = {y} & the carrier of Y2 = {y} implies Y1 = Y2 )
assume that
A1: the carrier of Y1 = {y} and
A2: the carrier of Y2 = {y} ; ::_thesis: Y1 = Y2
set A1 = the carrier of Y1;
set A2 = the carrier of Y2;
A3: the carrier of Y2 = [#] Y2 ;
A4: the carrier of Y1 = [#] Y1 ;
then the carrier of Y1 c= [#] Y by PRE_TOPC:def_4;
then reconsider A1 = the carrier of Y1 as Subset of Y ;
Y1 = Y | A1 by A4, PRE_TOPC:def_5;
hence Y1 = Y2 by A1, A2, A3, PRE_TOPC:def_5; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Sspace TEX_2:def_2_:_
for Y being non empty TopStruct
for y being Point of Y
for b3 being non empty strict SubSpace of Y holds
( b3 = Sspace y iff the carrier of b3 = {y} );
Lm2: now__::_thesis:_for_Y_being_non_empty_TopStruct_
for_y_being_Point_of_Y_holds_Sspace_y_is_1_-element
let Y be non empty TopStruct ; ::_thesis: for y being Point of Y holds Sspace y is 1 -element
let y be Point of Y; ::_thesis: Sspace y is 1 -element
set Y0 = Sspace y;
the carrier of (Sspace y) = {y} by Def2;
then reconsider y0 = y as Point of (Sspace y) by TARSKI:def_1;
the carrier of (Sspace y) = {y0} by Def2;
hence Sspace y is 1 -element by STRUCT_0:def_19; ::_thesis: verum
end;
registration
let Y be non empty TopStruct ;
cluster1 -element strict for SubSpace of Y;
existence
ex b1 being SubSpace of Y st
( b1 is strict & b1 is 1 -element )
proof
set y = the Point of Y;
take Sspace the Point of Y ; ::_thesis: ( Sspace the Point of Y is strict & Sspace the Point of Y is 1 -element )
thus ( Sspace the Point of Y is strict & Sspace the Point of Y is 1 -element ) by Lm2; ::_thesis: verum
end;
end;
registration
let Y be non empty TopStruct ;
let y be Point of Y;
cluster Sspace y -> non empty 1 -element strict ;
coherence
Sspace y is 1 -element by Lm2;
end;
theorem :: TEX_2:15
for Y being non empty TopStruct
for y being Point of Y holds
( Sspace y is proper iff {y} is proper )
proof
let Y be non empty TopStruct ; ::_thesis: for y being Point of Y holds
( Sspace y is proper iff {y} is proper )
let y be Point of Y; ::_thesis: ( Sspace y is proper iff {y} is proper )
hereby ::_thesis: ( {y} is proper implies Sspace y is proper )
reconsider A = the carrier of (Sspace y) as Subset of Y by Lm1;
assume A1: Sspace y is proper ; ::_thesis: {y} is proper
A = {y} by Def2;
hence {y} is proper by A1, Def1; ::_thesis: verum
end;
hereby ::_thesis: verum
assume {y} is proper ; ::_thesis: Sspace y is proper
then for A being Subset of Y st A = the carrier of (Sspace y) holds
A is proper by Def2;
hence Sspace y is proper by Def1; ::_thesis: verum
end;
end;
theorem :: TEX_2:16
for Y being non empty TopStruct
for y being Point of Y st Sspace y is proper holds
not Y is trivial ;
registration
let Y be non trivial TopStruct ;
cluster non empty trivial strict proper for SubSpace of Y;
existence
ex b1 being non empty SubSpace of Y st
( b1 is proper & b1 is trivial & b1 is strict )
proof
set Y0 = the non empty trivial strict SubSpace of Y;
take the non empty trivial strict SubSpace of Y ; ::_thesis: ( the non empty trivial strict SubSpace of Y is proper & the non empty trivial strict SubSpace of Y is trivial & the non empty trivial strict SubSpace of Y is strict )
thus ( the non empty trivial strict SubSpace of Y is proper & the non empty trivial strict SubSpace of Y is trivial & the non empty trivial strict SubSpace of Y is strict ) ; ::_thesis: verum
end;
end;
registration
let Y be non empty TopStruct ;
cluster1 -element for SubSpace of Y;
existence
ex b1 being SubSpace of Y st b1 is 1 -element
proof
take Y0 = the non empty trivial SubSpace of Y; ::_thesis: Y0 is 1 -element
thus Y0 is 1 -element ; ::_thesis: verum
end;
end;
theorem :: TEX_2:17
for Y being non empty TopStruct
for Y0 being 1 -element SubSpace of Y ex y being Point of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #)
proof
let Y be non empty TopStruct ; ::_thesis: for Y0 being 1 -element SubSpace of Y ex y being Point of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #)
let Y0 be 1 -element SubSpace of Y; ::_thesis: ex y being Point of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #)
consider y0 being Element of Y0 such that
A1: the carrier of Y0 = {y0} by TEX_1:def_1;
the carrier of Y0 is Subset of Y by Lm1;
then reconsider y = y0 as Point of Y by A1, ZFMISC_1:31;
take y ; ::_thesis: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #)
the carrier of Y0 = the carrier of (Sspace y) by A1, Def2;
hence TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #) by TSEP_1:5; ::_thesis: verum
end;
theorem :: TEX_2:18
for Y being non empty TopStruct
for y being Point of Y st Sspace y is TopSpace-like holds
( Sspace y is discrete & Sspace y is anti-discrete ) ;
registration
let Y be non empty TopStruct ;
cluster non empty trivial TopSpace-like -> non empty discrete anti-discrete for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is trivial & b1 is TopSpace-like holds
( b1 is discrete & b1 is anti-discrete ) ;
end;
registration
let X be non empty TopSpace;
cluster non empty trivial strict TopSpace-like for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is trivial & b1 is strict & b1 is TopSpace-like & not b1 is empty )
proof
set x = the Point of X;
take Sspace the Point of X ; ::_thesis: ( Sspace the Point of X is trivial & Sspace the Point of X is strict & Sspace the Point of X is TopSpace-like & not Sspace the Point of X is empty )
thus ( Sspace the Point of X is trivial & Sspace the Point of X is strict & Sspace the Point of X is TopSpace-like & not Sspace the Point of X is empty ) ; ::_thesis: verum
end;
end;
registration
let X be non empty TopSpace;
let x be Point of X;
cluster Sspace x -> non empty strict TopSpace-like ;
coherence
Sspace x is TopSpace-like ;
end;
registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like discrete anti-discrete for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is discrete & b1 is anti-discrete & b1 is strict & not b1 is empty )
proof
set x = the Point of X;
take Sspace the Point of X ; ::_thesis: ( Sspace the Point of X is discrete & Sspace the Point of X is anti-discrete & Sspace the Point of X is strict & not Sspace the Point of X is empty )
thus ( Sspace the Point of X is discrete & Sspace the Point of X is anti-discrete & Sspace the Point of X is strict & not Sspace the Point of X is empty ) ; ::_thesis: verum
end;
end;
registration
let X be non empty TopSpace;
let x be Point of X;
cluster Sspace x -> non empty strict discrete anti-discrete ;
coherence
( Sspace x is discrete & Sspace x is anti-discrete ) ;
end;
registration
let X be non empty TopSpace;
cluster non proper -> closed open for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is proper holds
( b1 is open & b1 is closed )
proof
let X0 be SubSpace of X; ::_thesis: ( not X0 is proper implies ( X0 is open & X0 is closed ) )
assume not X0 is proper ; ::_thesis: ( X0 is open & X0 is closed )
then A1: ex A being Subset of X st
( A = the carrier of X0 & not A is proper ) by Def1;
A2: now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_closed
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is closed )
assume A = the carrier of X0 ; ::_thesis: A is closed
then A = [#] X by A1, SUBSET_1:def_6;
hence A is closed ; ::_thesis: verum
end;
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_open
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is open )
assume A = the carrier of X0 ; ::_thesis: A is open
then A = [#] X by A1, SUBSET_1:def_6;
hence A is open ; ::_thesis: verum
end;
hence ( X0 is open & X0 is closed ) by A2, BORSUK_1:def_11, TSEP_1:def_1; ::_thesis: verum
end;
cluster non open -> proper for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is open holds
b1 is proper ;
cluster non closed -> proper for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is closed holds
b1 is proper ;
end;
registration
let X be non empty TopSpace;
cluster strict TopSpace-like closed open for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is open & b1 is closed & b1 is strict )
proof
set X0 = the strict non proper SubSpace of X;
take the strict non proper SubSpace of X ; ::_thesis: ( the strict non proper SubSpace of X is open & the strict non proper SubSpace of X is closed & the strict non proper SubSpace of X is strict )
thus ( the strict non proper SubSpace of X is open & the strict non proper SubSpace of X is closed & the strict non proper SubSpace of X is strict ) ; ::_thesis: verum
end;
end;
registration
let X be non empty discrete TopSpace;
cluster non empty anti-discrete -> non empty trivial for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is anti-discrete holds
b1 is trivial ;
cluster non empty non trivial -> non empty non anti-discrete for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is trivial holds
not b1 is anti-discrete ;
end;
registration
let X be non trivial discrete TopSpace;
cluster strict TopSpace-like closed open discrete almost_discrete proper for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is discrete & b1 is open & b1 is closed & b1 is proper & b1 is strict )
proof
set X0 = the strict proper SubSpace of X;
take the strict proper SubSpace of X ; ::_thesis: ( the strict proper SubSpace of X is discrete & the strict proper SubSpace of X is open & the strict proper SubSpace of X is closed & the strict proper SubSpace of X is proper & the strict proper SubSpace of X is strict )
thus ( the strict proper SubSpace of X is discrete & the strict proper SubSpace of X is open & the strict proper SubSpace of X is closed & the strict proper SubSpace of X is proper & the strict proper SubSpace of X is strict ) ; ::_thesis: verum
end;
end;
registration
let X be non empty anti-discrete TopSpace;
cluster non empty discrete -> non empty trivial for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is discrete holds
b1 is trivial ;
cluster non empty non trivial -> non empty non discrete for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is trivial holds
not b1 is discrete ;
end;
registration
let X be non trivial anti-discrete TopSpace;
cluster non empty proper -> non empty non closed non open proper for SubSpace of X;
coherence
for b1 being non empty proper SubSpace of X holds
( not b1 is open & not b1 is closed )
proof
let X0 be non empty proper SubSpace of X; ::_thesis: ( not X0 is open & not X0 is closed )
assume A1: ( X0 is open or X0 is closed ) ; ::_thesis: contradiction
reconsider A = the carrier of X0 as non empty Subset of X by Lm1;
set B = A ` ;
A2: A ` <> the carrier of X by TOPS_3:1;
A3: A is proper by Def1;
then A4: A <> the carrier of X by SUBSET_1:def_6;
now__::_thesis:_contradiction
percases ( X0 is open or X0 is closed ) by A1;
suppose X0 is open ; ::_thesis: contradiction
then A is open by TSEP_1:def_1;
then A in the topology of X by PRE_TOPC:def_2;
then A in {{}, the carrier of X} by TDLAT_3:def_2;
hence contradiction by A4, TARSKI:def_2; ::_thesis: verum
end;
suppose X0 is closed ; ::_thesis: contradiction
then A is closed by BORSUK_1:def_11;
then A ` in the topology of X by PRE_TOPC:def_2;
then A ` in {{}, the carrier of X} by TDLAT_3:def_2;
hence contradiction by A3, A2, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
cluster non empty discrete -> non empty trivial discrete proper for SubSpace of X;
coherence
for b1 being non empty discrete SubSpace of X holds
( b1 is trivial & b1 is proper ) ;
end;
registration
let X be non trivial anti-discrete TopSpace;
cluster strict TopSpace-like non closed non open anti-discrete almost_discrete proper for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is anti-discrete & not b1 is open & not b1 is closed & b1 is proper & b1 is strict )
proof
set X0 = the non empty strict proper SubSpace of X;
take the non empty strict proper SubSpace of X ; ::_thesis: ( the non empty strict proper SubSpace of X is anti-discrete & not the non empty strict proper SubSpace of X is open & not the non empty strict proper SubSpace of X is closed & the non empty strict proper SubSpace of X is proper & the non empty strict proper SubSpace of X is strict )
thus ( the non empty strict proper SubSpace of X is anti-discrete & not the non empty strict proper SubSpace of X is open & not the non empty strict proper SubSpace of X is closed & the non empty strict proper SubSpace of X is proper & the non empty strict proper SubSpace of X is strict ) ; ::_thesis: verum
end;
end;
registration
let X be non trivial almost_discrete TopSpace;
cluster non empty strict TopSpace-like almost_discrete proper for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is almost_discrete & b1 is proper & b1 is strict & not b1 is empty )
proof
set X0 = the non empty strict proper SubSpace of X;
take the non empty strict proper SubSpace of X ; ::_thesis: ( the non empty strict proper SubSpace of X is almost_discrete & the non empty strict proper SubSpace of X is proper & the non empty strict proper SubSpace of X is strict & not the non empty strict proper SubSpace of X is empty )
thus ( the non empty strict proper SubSpace of X is almost_discrete & the non empty strict proper SubSpace of X is proper & the non empty strict proper SubSpace of X is strict & not the non empty strict proper SubSpace of X is empty ) ; ::_thesis: verum
end;
end;
begin
definition
let Y be TopStruct ;
let IT be Subset of Y;
attrIT is discrete means :Def3: :: TEX_2:def 3
for D being Subset of Y st D c= IT holds
ex G being Subset of Y st
( G is open & IT /\ G = D );
end;
:: deftheorem Def3 defines discrete TEX_2:def_3_:_
for Y being TopStruct
for IT being Subset of Y holds
( IT is discrete iff for D being Subset of Y st D c= IT holds
ex G being Subset of Y st
( G is open & IT /\ G = D ) );
definition
let Y be TopStruct ;
let A be Subset of Y;
redefine attr A is discrete means :Def4: :: TEX_2:def 4
for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D );
compatibility
( A is discrete iff for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D ) )
proof
hereby ::_thesis: ( ( for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D ) ) implies A is discrete )
assume A1: A is discrete ; ::_thesis: for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D )
let D be Subset of Y; ::_thesis: ( D c= A implies ex F being Subset of Y st
( F is closed & A /\ F = D ) )
A \ D c= A by XBOOLE_1:36;
then consider G being Subset of Y such that
A2: G is open and
A3: A /\ G = A \ D by A1, Def3;
assume A4: D c= A ; ::_thesis: ex F being Subset of Y st
( F is closed & A /\ F = D )
now__::_thesis:_ex_F_being_Element_of_bool_the_carrier_of_Y_st_
(_F_is_closed_&_A_/\_F_=_D_)
take F = ([#] Y) \ G; ::_thesis: ( F is closed & A /\ F = D )
G = ([#] Y) \ F by PRE_TOPC:3;
hence F is closed by A2, PRE_TOPC:def_3; ::_thesis: A /\ F = D
A /\ ([#] Y) = A by XBOOLE_1:28;
then A /\ F = A \ G by XBOOLE_1:49;
then A /\ F = A \ (A \ D) by A3, XBOOLE_1:47;
then A /\ F = A /\ D by XBOOLE_1:48;
hence A /\ F = D by A4, XBOOLE_1:28; ::_thesis: verum
end;
hence ex F being Subset of Y st
( F is closed & A /\ F = D ) ; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A5: for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D ) ; ::_thesis: A is discrete
now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_A_holds_
ex_G_being_Subset_of_Y_st_
(_G_is_open_&_A_/\_G_=_D_)
let D be Subset of Y; ::_thesis: ( D c= A implies ex G being Subset of Y st
( G is open & A /\ G = D ) )
consider F being Subset of Y such that
A6: F is closed and
A7: A /\ F = A \ D by A5, XBOOLE_1:36;
assume A8: D c= A ; ::_thesis: ex G being Subset of Y st
( G is open & A /\ G = D )
now__::_thesis:_ex_G_being_Element_of_bool_the_carrier_of_Y_st_
(_G_is_open_&_A_/\_G_=_D_)
take G = ([#] Y) \ F; ::_thesis: ( G is open & A /\ G = D )
thus G is open by A6, PRE_TOPC:def_3; ::_thesis: A /\ G = D
A /\ ([#] Y) = A by XBOOLE_1:28;
then A /\ G = A \ F by XBOOLE_1:49;
then A /\ G = A \ (A \ D) by A7, XBOOLE_1:47;
then A /\ G = A /\ D by XBOOLE_1:48;
hence A /\ G = D by A8, XBOOLE_1:28; ::_thesis: verum
end;
hence ex G being Subset of Y st
( G is open & A /\ G = D ) ; ::_thesis: verum
end;
hence A is discrete by Def3; ::_thesis: verum
end;
end;
end;
:: deftheorem Def4 defines discrete TEX_2:def_4_:_
for Y being TopStruct
for A being Subset of Y holds
( A is discrete iff for D being Subset of Y st D c= A holds
ex F being Subset of Y st
( F is closed & A /\ F = D ) );
theorem Th19: :: TEX_2:19
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 discrete holds
D1 is discrete
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 discrete holds
D1 is discrete
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 discrete holds
D1 is discrete
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 discrete implies D1 is discrete )
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 discrete or D1 is discrete )
assume A2: D0 = D1 ; ::_thesis: ( not D0 is discrete or D1 is discrete )
assume A3: D0 is discrete ; ::_thesis: D1 is discrete
now__::_thesis:_for_D_being_Subset_of_Y1_st_D_c=_D1_holds_
ex_G_being_Subset_of_Y1_st_
(_G_is_open_&_D1_/\_G_=_D_)
let D be Subset of Y1; ::_thesis: ( D c= D1 implies ex G being Subset of Y1 st
( G is open & D1 /\ G = D ) )
reconsider E = D as Subset of Y0 by A1;
assume D c= D1 ; ::_thesis: ex G being Subset of Y1 st
( G is open & D1 /\ G = D )
then consider G0 being Subset of Y0 such that
A4: G0 is open and
A5: D0 /\ G0 = E by A2, A3, Def3;
reconsider G = G0 as Subset of Y1 by A1;
now__::_thesis:_ex_G_being_Subset_of_Y1_st_
(_G_is_open_&_D1_/\_G_=_D_)
take G = G; ::_thesis: ( G is open & D1 /\ G = D )
G in the topology of Y1 by A1, A4, PRE_TOPC:def_2;
hence G is open by PRE_TOPC:def_2; ::_thesis: D1 /\ G = D
thus D1 /\ G = D by A2, A5; ::_thesis: verum
end;
hence ex G being Subset of Y1 st
( G is open & D1 /\ G = D ) ; ::_thesis: verum
end;
hence D1 is discrete by Def3; ::_thesis: verum
end;
theorem Th20: :: TEX_2:20
for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is discrete iff Y0 is discrete )
proof
let Y be non empty TopStruct ; ::_thesis: for Y0 being non empty SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is discrete iff Y0 is discrete )
let Y0 be non empty SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 holds
( A is discrete iff Y0 is discrete )
let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 implies ( A is discrete iff Y0 is discrete ) )
assume A1: A = the carrier of Y0 ; ::_thesis: ( A is discrete iff Y0 is discrete )
A2: [#] Y = the carrier of Y ;
[#] Y0 = the carrier of Y0 ;
then A3: the carrier of Y0 c= the carrier of Y by A2, PRE_TOPC:def_4;
hereby ::_thesis: ( Y0 is discrete implies A is discrete )
assume A4: A is discrete ; ::_thesis: Y0 is discrete
now__::_thesis:_for_C_being_set_st_C_in_bool_the_carrier_of_Y0_holds_
C_in_the_topology_of_Y0
let C be set ; ::_thesis: ( C in bool the carrier of Y0 implies C in the topology of Y0 )
assume C in bool the carrier of Y0 ; ::_thesis: C in the topology of Y0
then reconsider B = C as Subset of Y0 ;
reconsider D = B as Subset of Y by A3, XBOOLE_1:1;
consider G being Subset of Y such that
A5: G is open and
A6: A /\ G = D by A1, A4, Def3;
now__::_thesis:_ex_G_being_Subset_of_Y_st_
(_G_in_the_topology_of_Y_&_B_=_G_/\_([#]_Y0)_)
take G = G; ::_thesis: ( G in the topology of Y & B = G /\ ([#] Y0) )
thus G in the topology of Y by A5, PRE_TOPC:def_2; ::_thesis: B = G /\ ([#] Y0)
thus B = G /\ ([#] Y0) by A1, A6; ::_thesis: verum
end;
hence C in the topology of Y0 by PRE_TOPC:def_4; ::_thesis: verum
end;
then bool the carrier of Y0 c= the topology of Y0 by TARSKI:def_3;
then the topology of Y0 = bool the carrier of Y0 by XBOOLE_0:def_10;
hence Y0 is discrete by TDLAT_3:def_1; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A7: Y0 is discrete ; ::_thesis: A is discrete
now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_A_holds_
ex_G_being_Subset_of_Y_st_
(_G_is_open_&_A_/\_G_=_D_)
let D be Subset of Y; ::_thesis: ( D c= A implies ex G being Subset of Y st
( G is open & A /\ G = D ) )
assume D c= A ; ::_thesis: ex G being Subset of Y st
( G is open & A /\ G = D )
then reconsider B = D as Subset of Y0 by A1;
B is open by A7, TDLAT_3:15;
then B in the topology of Y0 by PRE_TOPC:def_2;
then consider G being Subset of Y such that
A8: G in the topology of Y and
A9: B = G /\ ([#] Y0) by PRE_TOPC:def_4;
reconsider G = G as Subset of Y ;
take G = G; ::_thesis: ( G is open & A /\ G = D )
thus G is open by A8, PRE_TOPC:def_2; ::_thesis: A /\ G = D
thus A /\ G = D by A1, A9; ::_thesis: verum
end;
hence A is discrete by Def3; ::_thesis: verum
end;
end;
theorem Th21: :: TEX_2:21
for Y being non empty TopStruct
for A being Subset of Y st A = the carrier of Y holds
( A is discrete iff Y is discrete )
proof
let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y st A = the carrier of Y holds
( A is discrete iff Y is discrete )
let A be Subset of Y; ::_thesis: ( A = the carrier of Y implies ( A is discrete iff Y is discrete ) )
assume A1: A = the carrier of Y ; ::_thesis: ( A is discrete iff Y is discrete )
hereby ::_thesis: ( Y is discrete implies A is discrete )
assume A2: A is discrete ; ::_thesis: Y is discrete
now__::_thesis:_for_C_being_set_st_C_in_bool_the_carrier_of_Y_holds_
C_in_the_topology_of_Y
let C be set ; ::_thesis: ( C in bool the carrier of Y implies C in the topology of Y )
assume C in bool the carrier of Y ; ::_thesis: C in the topology of Y
then reconsider B = C as Subset of Y ;
consider G being Subset of Y such that
A3: G is open and
A4: A /\ G = B by A1, A2, Def3;
G = B by A1, A4, XBOOLE_1:28;
hence C in the topology of Y by A3, PRE_TOPC:def_2; ::_thesis: verum
end;
then bool the carrier of Y c= the topology of Y by TARSKI:def_3;
then the topology of Y = bool the carrier of Y by XBOOLE_0:def_10;
hence Y is discrete by TDLAT_3:def_1; ::_thesis: verum
end;
hereby ::_thesis: verum
assume Y is discrete ; ::_thesis: A is discrete
then reconsider Y = Y as non empty discrete TopStruct ;
now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_A_holds_
ex_G_being_Subset_of_Y_st_
(_G_is_open_&_A_/\_G_=_D_)
let D be Subset of Y; ::_thesis: ( D c= A implies ex G being Subset of Y st
( G is open & A /\ G = D ) )
assume A5: D c= A ; ::_thesis: ex G being Subset of Y st
( G is open & A /\ G = D )
reconsider G = D as Subset of Y ;
take G = G; ::_thesis: ( G is open & A /\ G = D )
thus G is open by TDLAT_3:15; ::_thesis: A /\ G = D
thus A /\ G = D by A5, XBOOLE_1:28; ::_thesis: verum
end;
hence A is discrete by Def3; ::_thesis: verum
end;
end;
theorem Th22: :: TEX_2:22
for Y being TopStruct
for A, B being Subset of Y st B c= A & A is discrete holds
B is discrete
proof
let Y be TopStruct ; ::_thesis: for A, B being Subset of Y st B c= A & A is discrete holds
B is discrete
let A, B be Subset of Y; ::_thesis: ( B c= A & A is discrete implies B is discrete )
assume A1: B c= A ; ::_thesis: ( not A is discrete or B is discrete )
assume A2: A is discrete ; ::_thesis: B is discrete
now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_B_holds_
ex_G_being_Subset_of_Y_st_
(_G_is_open_&_B_/\_G_=_D_)
let D be Subset of Y; ::_thesis: ( D c= B implies ex G being Subset of Y st
( G is open & B /\ G = D ) )
assume A3: D c= B ; ::_thesis: ex G being Subset of Y st
( G is open & B /\ G = D )
then D c= A by A1, XBOOLE_1:1;
then consider G being Subset of Y such that
A4: G is open and
A5: A /\ G = D by A2, Def3;
hereby ::_thesis: verum
take G = G; ::_thesis: ( G is open & B /\ G = D )
D c= G by A5, XBOOLE_1:17;
then A6: D c= B /\ G by A3, XBOOLE_1:19;
B /\ G c= A /\ G by A1, XBOOLE_1:26;
hence ( G is open & B /\ G = D ) by A4, A5, A6, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
hence B is discrete by Def3; ::_thesis: verum
end;
theorem :: TEX_2:23
for Y being TopStruct
for A, B being Subset of Y st ( A is discrete or B is discrete ) holds
A /\ B is discrete
proof
let Y be TopStruct ; ::_thesis: for A, B being Subset of Y st ( A is discrete or B is discrete ) holds
A /\ B is discrete
let A, B be Subset of Y; ::_thesis: ( ( A is discrete or B is discrete ) implies A /\ B is discrete )
assume A1: ( A is discrete or B is discrete ) ; ::_thesis: A /\ B is discrete
hereby ::_thesis: verum
percases ( A is discrete or B is discrete ) by A1;
suppose A is discrete ; ::_thesis: A /\ B is discrete
hence A /\ B is discrete by Th22, XBOOLE_1:17; ::_thesis: verum
end;
suppose B is discrete ; ::_thesis: A /\ B is discrete
hence A /\ B is discrete by Th22, XBOOLE_1:17; ::_thesis: verum
end;
end;
end;
end;
theorem Th24: :: TEX_2:24
for Y being TopStruct st ( for P, Q being Subset of Y st P is open & Q is open holds
( P /\ Q is open & P \/ Q is open ) ) holds
for A, B being Subset of Y st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete
proof
let Y be TopStruct ; ::_thesis: ( ( for P, Q being Subset of Y st P is open & Q is open holds
( P /\ Q is open & P \/ Q is open ) ) implies for A, B being Subset of Y st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete )
assume A1: for P, Q being Subset of Y st P is open & Q is open holds
( P /\ Q is open & P \/ Q is open ) ; ::_thesis: for A, B being Subset of Y st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete
let A, B be Subset of Y; ::_thesis: ( A is open & B is open & A is discrete & B is discrete implies A \/ B is discrete )
assume that
A2: A is open and
A3: B is open ; ::_thesis: ( not A is discrete or not B is discrete or A \/ B is discrete )
assume that
A4: A is discrete and
A5: B is discrete ; ::_thesis: A \/ B is discrete
now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_A_\/_B_holds_
ex_G_being_Subset_of_Y_st_
(_G_is_open_&_(A_\/_B)_/\_G_=_D_)
let D be Subset of Y; ::_thesis: ( D c= A \/ B implies ex G being Subset of Y st
( G is open & (A \/ B) /\ G = D ) )
D /\ A c= A by XBOOLE_1:17;
then consider G1 being Subset of Y such that
A6: G1 is open and
A7: A /\ G1 = D /\ A by A4, Def3;
D /\ B c= B by XBOOLE_1:17;
then consider G2 being Subset of Y such that
A8: G2 is open and
A9: B /\ G2 = D /\ B by A5, Def3;
assume D c= A \/ B ; ::_thesis: ex G being Subset of Y st
( G is open & (A \/ B) /\ G = D )
then A10: D = D /\ (A \/ B) by XBOOLE_1:28;
now__::_thesis:_ex_G_being_Element_of_bool_the_carrier_of_Y_st_
(_G_is_open_&_(A_\/_B)_/\_G_=_D_)
take G = (A /\ G1) \/ (B /\ G2); ::_thesis: ( G is open & (A \/ B) /\ G = D )
A11: B /\ G2 is open by A1, A3, A8;
A /\ G1 is open by A1, A2, A6;
hence G is open by A1, A11; ::_thesis: (A \/ B) /\ G = D
thus (A \/ B) /\ G = D by A10, A7, A9, XBOOLE_1:23; ::_thesis: verum
end;
hence ex G being Subset of Y st
( G is open & (A \/ B) /\ G = D ) ; ::_thesis: verum
end;
hence A \/ B is discrete by Def3; ::_thesis: verum
end;
theorem Th25: :: TEX_2:25
for Y being TopStruct st ( for P, Q being Subset of Y st P is closed & Q is closed holds
( P /\ Q is closed & P \/ Q is closed ) ) holds
for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete
proof
let Y be TopStruct ; ::_thesis: ( ( for P, Q being Subset of Y st P is closed & Q is closed holds
( P /\ Q is closed & P \/ Q is closed ) ) implies for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete )
assume A1: for P, Q being Subset of Y st P is closed & Q is closed holds
( P /\ Q is closed & P \/ Q is closed ) ; ::_thesis: for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete
let A, B be Subset of Y; ::_thesis: ( A is closed & B is closed & A is discrete & B is discrete implies A \/ B is discrete )
assume that
A2: A is closed and
A3: B is closed ; ::_thesis: ( not A is discrete or not B is discrete or A \/ B is discrete )
assume that
A4: A is discrete and
A5: B is discrete ; ::_thesis: A \/ B is discrete
now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_A_\/_B_holds_
ex_F_being_Subset_of_Y_st_
(_F_is_closed_&_(A_\/_B)_/\_F_=_D_)
let D be Subset of Y; ::_thesis: ( D c= A \/ B implies ex F being Subset of Y st
( F is closed & (A \/ B) /\ F = D ) )
D /\ A c= A by XBOOLE_1:17;
then consider F1 being Subset of Y such that
A6: F1 is closed and
A7: A /\ F1 = D /\ A by A4, Def4;
D /\ B c= B by XBOOLE_1:17;
then consider F2 being Subset of Y such that
A8: F2 is closed and
A9: B /\ F2 = D /\ B by A5, Def4;
assume D c= A \/ B ; ::_thesis: ex F being Subset of Y st
( F is closed & (A \/ B) /\ F = D )
then A10: D = D /\ (A \/ B) by XBOOLE_1:28;
now__::_thesis:_ex_F_being_Element_of_bool_the_carrier_of_Y_st_
(_F_is_closed_&_(A_\/_B)_/\_F_=_D_)
take F = (A /\ F1) \/ (B /\ F2); ::_thesis: ( F is closed & (A \/ B) /\ F = D )
A11: B /\ F2 is closed by A1, A3, A8;
A /\ F1 is closed by A1, A2, A6;
hence F is closed by A1, A11; ::_thesis: (A \/ B) /\ F = D
thus (A \/ B) /\ F = D by A10, A7, A9, XBOOLE_1:23; ::_thesis: verum
end;
hence ex F being Subset of Y st
( F is closed & (A \/ B) /\ F = D ) ; ::_thesis: verum
end;
hence A \/ B is discrete by Def4; ::_thesis: verum
end;
theorem Th26: :: TEX_2:26
for Y being TopStruct
for A being Subset of Y st A is discrete holds
for x being Point of Y st x in A holds
ex G being Subset of Y st
( G is open & A /\ G = {x} )
proof
let Y be TopStruct ; ::_thesis: for A being Subset of Y st A is discrete holds
for x being Point of Y st x in A holds
ex G being Subset of Y st
( G is open & A /\ G = {x} )
let A be Subset of Y; ::_thesis: ( A is discrete implies for x being Point of Y st x in A holds
ex G being Subset of Y st
( G is open & A /\ G = {x} ) )
assume A1: A is discrete ; ::_thesis: for x being Point of Y st x in A holds
ex G being Subset of Y st
( G is open & A /\ G = {x} )
let x be Point of Y; ::_thesis: ( x in A implies ex G being Subset of Y st
( G is open & A /\ G = {x} ) )
assume A2: x in A ; ::_thesis: ex G being Subset of Y st
( G is open & A /\ G = {x} )
then reconsider Y9 = Y as non empty TopStruct ;
reconsider B = {x} as Subset of Y9 by ZFMISC_1:31;
reconsider A9 = A as Subset of Y9 ;
{x} c= A9 by A2, ZFMISC_1:31;
then consider G being Subset of Y9 such that
A3: G is open and
A4: A9 /\ G = B by A1, Def3;
reconsider G = G as Subset of Y ;
take G ; ::_thesis: ( G is open & A /\ G = {x} )
thus ( G is open & A /\ G = {x} ) by A3, A4; ::_thesis: verum
end;
theorem :: TEX_2:27
for Y being TopStruct
for A being Subset of Y st A is discrete holds
for x being Point of Y st x in A holds
ex F being Subset of Y st
( F is closed & A /\ F = {x} )
proof
let Y be TopStruct ; ::_thesis: for A being Subset of Y st A is discrete holds
for x being Point of Y st x in A holds
ex F being Subset of Y st
( F is closed & A /\ F = {x} )
let A be Subset of Y; ::_thesis: ( A is discrete implies for x being Point of Y st x in A holds
ex F being Subset of Y st
( F is closed & A /\ F = {x} ) )
assume A1: A is discrete ; ::_thesis: for x being Point of Y st x in A holds
ex F being Subset of Y st
( F is closed & A /\ F = {x} )
let x be Point of Y; ::_thesis: ( x in A implies ex F being Subset of Y st
( F is closed & A /\ F = {x} ) )
assume A2: x in A ; ::_thesis: ex F being Subset of Y st
( F is closed & A /\ F = {x} )
then reconsider Y9 = Y as non empty TopStruct ;
reconsider B = {x} as Subset of Y9 by ZFMISC_1:31;
reconsider A9 = A as Subset of Y9 ;
{x} c= A9 by A2, ZFMISC_1:31;
then consider F being Subset of Y such that
A3: F is closed and
A4: A9 /\ F = B by A1, Def4;
take F ; ::_thesis: ( F is closed & A /\ F = {x} )
thus ( F is closed & A /\ F = {x} ) by A3, A4; ::_thesis: verum
end;
theorem Th28: :: TEX_2:28
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is discrete holds
ex X0 being non empty strict discrete SubSpace of X st A0 = the carrier of X0
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is discrete holds
ex X0 being non empty strict discrete SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is discrete implies ex X0 being non empty strict discrete SubSpace of X st A0 = the carrier of X0 )
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A0 is discrete ; ::_thesis: ex X0 being non empty strict discrete SubSpace of X st A0 = the carrier of X0
then reconsider X0 = X0 as non empty strict discrete SubSpace of X by A1, Th20;
take X0 ; ::_thesis: A0 = the carrier of X0
thus A0 = the carrier of X0 by A1; ::_thesis: verum
end;
theorem Th29: :: TEX_2:29
for X being non empty TopSpace
for A being empty Subset of X holds A is discrete
proof
let X be non empty TopSpace; ::_thesis: for A being empty Subset of X holds A is discrete
let A be empty Subset of X; ::_thesis: A is discrete
now__::_thesis:_for_D_being_Subset_of_X_st_D_c=_A_holds_
ex_G_being_Subset_of_X_st_
(_G_is_open_&_A_/\_G_=_D_)
let D be Subset of X; ::_thesis: ( D c= A implies ex G being Subset of X st
( G is open & A /\ G = D ) )
assume A1: D c= A ; ::_thesis: ex G being Subset of X st
( G is open & A /\ G = D )
now__::_thesis:_ex_G_being_Element_of_bool_the_carrier_of_X_st_
(_G_is_open_&_A_/\_G_=_D_)
take G = {} X; ::_thesis: ( G is open & A /\ G = D )
thus ( G is open & A /\ G = D ) by A1; ::_thesis: verum
end;
hence ex G being Subset of X st
( G is open & A /\ G = D ) ; ::_thesis: verum
end;
hence A is discrete by Def3; ::_thesis: verum
end;
theorem Th30: :: TEX_2:30
for X being non empty TopSpace
for x being Point of X holds {x} is discrete
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X holds {x} is discrete
let x be Point of X; ::_thesis: {x} is discrete
now__::_thesis:_for_D_being_Subset_of_X_st_D_c=_{x}_holds_
ex_G_being_Subset_of_X_st_
(_G_is_open_&_{x}_/\_G_=_D_)
let D be Subset of X; ::_thesis: ( D c= {x} implies ex G being Subset of X st
( G is open & {x} /\ G = D ) )
A1: now__::_thesis:_(_D_=_{}_implies_ex_G_being_Element_of_bool_the_carrier_of_X_st_
(_G_is_open_&_{x}_/\_G_=_D_)_)
assume A2: D = {} ; ::_thesis: ex G being Element of bool the carrier of X st
( G is open & {x} /\ G = D )
hereby ::_thesis: verum
take G = {} X; ::_thesis: ( G is open & {x} /\ G = D )
thus ( G is open & {x} /\ G = D ) by A2; ::_thesis: verum
end;
end;
A3: now__::_thesis:_(_D_=_{x}_implies_ex_G_being_Element_of_bool_the_carrier_of_X_st_
(_G_is_open_&_{x}_/\_G_=_D_)_)
assume A4: D = {x} ; ::_thesis: ex G being Element of bool the carrier of X st
( G is open & {x} /\ G = D )
hereby ::_thesis: verum
take G = [#] X; ::_thesis: ( G is open & {x} /\ G = D )
thus ( G is open & {x} /\ G = D ) by A4, XBOOLE_1:28; ::_thesis: verum
end;
end;
assume D c= {x} ; ::_thesis: ex G being Subset of X st
( G is open & {x} /\ G = D )
hence ex G being Subset of X st
( G is open & {x} /\ G = D ) by A1, A3, ZFMISC_1:33; ::_thesis: verum
end;
hence {x} is discrete by Def3; ::_thesis: verum
end;
theorem Th31: :: TEX_2:31
for X being non empty TopSpace
for A being Subset of X st ( for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ) holds
A is discrete
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st ( for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ) holds
A is discrete
let A be Subset of X; ::_thesis: ( ( for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ) implies A is discrete )
assume A1: for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ; ::_thesis: A is discrete
hereby ::_thesis: verum
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: A is discrete
hence A is discrete by Th29; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: A is discrete
then consider X0 being non empty strict SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
A3: [#] X = the carrier of X ;
[#] X0 = the carrier of X0 ;
then A4: the carrier of X0 c= the carrier of X by A3, PRE_TOPC:def_4;
now__::_thesis:_for_C_being_Subset_of_X0
for_y_being_Point_of_X0_st_C_=_{y}_holds_
C_is_open
let C be Subset of X0; ::_thesis: for y being Point of X0 st C = {y} holds
C is open
let y be Point of X0; ::_thesis: ( C = {y} implies C is open )
reconsider x = y as Point of X by A4, TARSKI:def_3;
consider G being Subset of X such that
A5: G is open and
A6: A /\ G = {x} by A1, A2;
assume A7: C = {y} ; ::_thesis: C is open
now__::_thesis:_ex_G_being_Subset_of_X_st_
(_G_in_the_topology_of_X_&_G_/\_([#]_X0)_=_C_)
take G = G; ::_thesis: ( G in the topology of X & G /\ ([#] X0) = C )
thus G in the topology of X by A5, PRE_TOPC:def_2; ::_thesis: G /\ ([#] X0) = C
thus G /\ ([#] X0) = C by A2, A7, A6; ::_thesis: verum
end;
then C in the topology of X0 by PRE_TOPC:def_4;
hence C is open by PRE_TOPC:def_2; ::_thesis: verum
end;
then X0 is discrete by TDLAT_3:17;
hence A is discrete by A2, Th20; ::_thesis: verum
end;
end;
end;
end;
theorem :: TEX_2:32
for X being non empty TopSpace
for A, B being Subset of X st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete
let A, B be Subset of X; ::_thesis: ( A is open & B is open & A is discrete & B is discrete implies A \/ B is discrete )
assume that
A1: A is open and
A2: B is open ; ::_thesis: ( not A is discrete or not B is discrete or A \/ B is discrete )
assume that
A3: A is discrete and
A4: B is discrete ; ::_thesis: A \/ B is discrete
for P, Q being Subset of X st P is open & Q is open holds
( P /\ Q is open & P \/ Q is open ) ;
hence A \/ B is discrete by A1, A2, A3, A4, Th24; ::_thesis: verum
end;
theorem :: TEX_2:33
for X being non empty TopSpace
for A, B being Subset of X st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete
let A, B be Subset of X; ::_thesis: ( A is closed & B is closed & A is discrete & B is discrete implies A \/ B is discrete )
assume that
A1: A is closed and
A2: B is closed ; ::_thesis: ( not A is discrete or not B is discrete or A \/ B is discrete )
assume that
A3: A is discrete and
A4: B is discrete ; ::_thesis: A \/ B is discrete
for P, Q being Subset of X st P is closed & Q is closed holds
( P /\ Q is closed & P \/ Q is closed ) ;
hence A \/ B is discrete by A1, A2, A3, A4, Th25; ::_thesis: verum
end;
Lm3: for P, Q being set st P c= Q & P <> Q holds
Q \ P <> {}
proof
let P, Q be set ; ::_thesis: ( P c= Q & P <> Q implies Q \ P <> {} )
assume P c= Q ; ::_thesis: ( not P <> Q or Q \ P <> {} )
then A1: Q = P \/ (Q \ P) by XBOOLE_1:45;
assume A2: P <> Q ; ::_thesis: Q \ P <> {}
assume Q \ P = {} ; ::_thesis: contradiction
hence contradiction by A1, A2; ::_thesis: verum
end;
theorem :: TEX_2:34
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense & A is discrete holds
A is open
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is everywhere_dense & A is discrete holds
A is open
let A be Subset of X; ::_thesis: ( A is everywhere_dense & A is discrete implies A is open )
assume A is everywhere_dense ; ::_thesis: ( not A is discrete or A is open )
then A1: Cl (Int A) = the carrier of X by TOPS_3:def_5;
assume A2: A is discrete ; ::_thesis: A is open
assume not A is open ; ::_thesis: contradiction
then A \ (Int A) <> {} by Lm3, TOPS_1:16;
then consider a being set such that
A3: a in A \ (Int A) by XBOOLE_0:def_1;
reconsider a = a as Point of X by A3;
A \ (Int A) c= A by XBOOLE_1:36;
then consider G being Subset of X such that
A4: G is open and
A5: A /\ G = {a} by A2, A3, Th26;
A6: now__::_thesis:_not_(Int_A)_/\_G_=_{a}
assume (Int A) /\ G = {a} ; ::_thesis: contradiction
then {a} c= Int A by XBOOLE_1:17;
then a in Int A by ZFMISC_1:31;
hence contradiction by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
(Int A) /\ G c= {a} by A5, TOPS_1:16, XBOOLE_1:26;
then ( (Int A) /\ G = {} or (Int A) /\ G = {a} ) by ZFMISC_1:33;
then ( Int A misses G or (Int A) /\ G = {a} ) by XBOOLE_0:def_7;
then Cl (Int A) misses G by A4, A6, TSEP_1:36;
then A7: (Cl (Int A)) /\ G = {} by XBOOLE_0:def_7;
{a} c= G by A5, XBOOLE_1:17;
hence contradiction by A1, A7, XBOOLE_1:3, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th35: :: TEX_2:35
for X being non empty TopSpace
for A being Subset of X holds
( A is discrete iff for D being Subset of X st D c= A holds
A /\ (Cl D) = D )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is discrete iff for D being Subset of X st D c= A holds
A /\ (Cl D) = D )
let A be Subset of X; ::_thesis: ( A is discrete iff for D being Subset of X st D c= A holds
A /\ (Cl D) = D )
thus ( A is discrete implies for D being Subset of X st D c= A holds
A /\ (Cl D) = D ) ::_thesis: ( ( for D being Subset of X st D c= A holds
A /\ (Cl D) = D ) implies A is discrete )
proof
assume A1: A is discrete ; ::_thesis: for D being Subset of X st D c= A holds
A /\ (Cl D) = D
let D be Subset of X; ::_thesis: ( D c= A implies A /\ (Cl D) = D )
assume A2: D c= A ; ::_thesis: A /\ (Cl D) = D
then consider F being Subset of X such that
A3: F is closed and
A4: A /\ F = D by A1, Def4;
Cl D c= F by A3, A4, TOPS_1:5, XBOOLE_1:17;
then A5: A /\ (Cl D) c= D by A4, XBOOLE_1:26;
D c= Cl D by PRE_TOPC:18;
then D c= A /\ (Cl D) by A2, XBOOLE_1:19;
hence A /\ (Cl D) = D by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
assume A6: for D being Subset of X st D c= A holds
A /\ (Cl D) = D ; ::_thesis: A is discrete
now__::_thesis:_for_D_being_Subset_of_X_st_D_c=_A_holds_
ex_F_being_Subset_of_X_st_
(_F_is_closed_&_A_/\_F_=_D_)
let D be Subset of X; ::_thesis: ( D c= A implies ex F being Subset of X st
( F is closed & A /\ F = D ) )
assume A7: D c= A ; ::_thesis: ex F being Subset of X st
( F is closed & A /\ F = D )
now__::_thesis:_ex_F_being_Element_of_bool_the_carrier_of_X_st_
(_F_is_closed_&_A_/\_F_=_D_)
take F = Cl D; ::_thesis: ( F is closed & A /\ F = D )
thus F is closed ; ::_thesis: A /\ F = D
thus A /\ F = D by A6, A7; ::_thesis: verum
end;
hence ex F being Subset of X st
( F is closed & A /\ F = D ) ; ::_thesis: verum
end;
hence A is discrete by Def4; ::_thesis: verum
end;
theorem Th36: :: TEX_2:36
for X being non empty TopSpace
for A being Subset of X st A is discrete holds
for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is discrete holds
for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}
let A be Subset of X; ::_thesis: ( A is discrete implies for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} )
assume A1: A is discrete ; ::_thesis: for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}
let x be Point of X; ::_thesis: ( x in A implies A /\ (Cl {x}) = {x} )
assume x in A ; ::_thesis: A /\ (Cl {x}) = {x}
then {x} c= A by ZFMISC_1:31;
hence A /\ (Cl {x}) = {x} by A1, Th35; ::_thesis: verum
end;
theorem :: TEX_2:37
for X being non empty discrete TopSpace
for A being Subset of X holds A is discrete
proof
let X be non empty discrete TopSpace; ::_thesis: for A being Subset of X holds A is discrete
let A be Subset of X; ::_thesis: A is discrete
hereby ::_thesis: verum
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: A is discrete
hence A is discrete by Th29; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: A is discrete
then ex X0 being non empty strict SubSpace of X st A = the carrier of X0 by TSEP_1:10;
hence A is discrete by Th20; ::_thesis: verum
end;
end;
end;
end;
theorem Th38: :: TEX_2:38
for X being non empty anti-discrete TopSpace
for A being non empty Subset of X holds
( A is discrete iff A is trivial )
proof
let X be non empty anti-discrete TopSpace; ::_thesis: for A being non empty Subset of X holds
( A is discrete iff A is trivial )
let A be non empty Subset of X; ::_thesis: ( A is discrete iff A is trivial )
hereby ::_thesis: ( A is trivial implies A is discrete )
consider a being set such that
A1: a in A by XBOOLE_0:def_1;
reconsider a = a as Point of X by A1;
assume A is discrete ; ::_thesis: A is trivial
then consider G being Subset of X such that
A2: G is open and
A3: A /\ G = {a} by A1, Th26;
G <> {} by A3;
then A4: G = the carrier of X by A2, TDLAT_3:18;
now__::_thesis:_ex_a_being_Point_of_X_st_A_=_{a}
take a = a; ::_thesis: A = {a}
thus A = {a} by A3, A4, XBOOLE_1:28; ::_thesis: verum
end;
hence A is trivial ; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A is trivial ; ::_thesis: A is discrete
then ex a being Element of A st A = {a} by SUBSET_1:46;
hence A is discrete by Th30; ::_thesis: verum
end;
end;
definition
let Y be TopStruct ;
let IT be Subset of Y;
attrIT is maximal_discrete means :Def5: :: TEX_2:def 5
( IT is discrete & ( for D being Subset of Y st D is discrete & IT c= D holds
IT = D ) );
end;
:: deftheorem Def5 defines maximal_discrete TEX_2:def_5_:_
for Y being TopStruct
for IT being Subset of Y holds
( IT is maximal_discrete iff ( IT is discrete & ( for D being Subset of Y st D is discrete & IT c= D holds
IT = D ) ) );
theorem :: TEX_2:39
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_discrete holds
D1 is maximal_discrete
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_discrete holds
D1 is maximal_discrete
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_discrete holds
D1 is maximal_discrete
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_discrete implies D1 is maximal_discrete )
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_discrete or D1 is maximal_discrete )
assume A2: D0 = D1 ; ::_thesis: ( not D0 is maximal_discrete or D1 is maximal_discrete )
assume A3: D0 is maximal_discrete ; ::_thesis: D1 is maximal_discrete
A4: now__::_thesis:_for_D_being_Subset_of_Y1_st_D_is_discrete_&_D1_c=_D_holds_
D1_=_D
let D be Subset of Y1; ::_thesis: ( D is discrete & D1 c= D implies D1 = D )
reconsider E = D as Subset of Y0 by A1;
assume D is discrete ; ::_thesis: ( D1 c= D implies D1 = D )
then A5: E is discrete by A1, Th19;
assume D1 c= D ; ::_thesis: D1 = D
hence D1 = D by A2, A3, A5, Def5; ::_thesis: verum
end;
D0 is discrete by A3, Def5;
then D1 is discrete by A1, A2, Th19;
hence D1 is maximal_discrete by A4, Def5; ::_thesis: verum
end;
theorem Th40: :: TEX_2:40
for X being non empty TopSpace
for A being empty Subset of X holds not A is maximal_discrete
proof
let X be non empty TopSpace; ::_thesis: for A being empty Subset of X holds not A is maximal_discrete
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_discrete
now__::_thesis:_ex_C_being_Element_of_bool_the_carrier_of_X_st_
(_C_is_discrete_&_A_c=_C_&_A_<>_C_)
take C = {a}; ::_thesis: ( C is discrete & A c= C & A <> C )
thus ( C is discrete & A c= C & A <> C ) by Th30, XBOOLE_1:2; ::_thesis: verum
end;
hence not A is maximal_discrete by Def5; ::_thesis: verum
end;
theorem Th41: :: TEX_2:41
for X being non empty TopSpace
for A being Subset of X st A is open & A is maximal_discrete holds
A is dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is open & A is maximal_discrete holds
A is dense
let A be Subset of X; ::_thesis: ( A is open & A is maximal_discrete implies A is dense )
assume A1: A is open ; ::_thesis: ( not A is maximal_discrete or A is dense )
assume A2: A is maximal_discrete ; ::_thesis: A is dense
then A3: A is discrete by Def5;
assume not A is dense ; ::_thesis: contradiction
then Cl A <> the carrier of X by TOPS_3:def_2;
then the carrier of X \ (Cl A) <> {} by Lm3;
then consider a being set such that
A4: a in the carrier of X \ (Cl A) by XBOOLE_0:def_1;
reconsider a = a as Point of X by A4;
set B = A \/ {a};
A5: A c= A \/ {a} by XBOOLE_1:7;
A6: now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_\/_{a}_holds_
ex_G_being_Subset_of_X_st_
(_G_is_open_&_(A_\/_{a})_/\_G_=_{x}_)
let x be Point of X; ::_thesis: ( x in A \/ {a} implies ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} ) )
assume x in A \/ {a} ; ::_thesis: ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} )
then A7: ( x in A or x in {a} ) by XBOOLE_0:def_3;
now__::_thesis:_ex_E_being_Subset_of_X_st_
(_E_is_open_&_(A_\/_{a})_/\_E_=_{x}_)
percases ( x in A or x = a ) by A7, TARSKI:def_1;
supposeA8: x in A ; ::_thesis: ex E being Subset of X st
( E is open & (A \/ {a}) /\ E = {x} )
then A9: ex G being Subset of X st
( G is open & A /\ G = {x} ) by A3, Th26;
now__::_thesis:_ex_E_being_Element_of_bool_the_carrier_of_X_st_
(_E_is_open_&_(A_\/_{a})_/\_E_=_{x}_)
take E = {x}; ::_thesis: ( E is open & (A \/ {a}) /\ E = {x} )
thus E is open by A1, A9; ::_thesis: (A \/ {a}) /\ E = {x}
{x} c= A \/ {a} by A5, A8, ZFMISC_1:31;
hence (A \/ {a}) /\ E = {x} by XBOOLE_1:28; ::_thesis: verum
end;
hence ex E being Subset of X st
( E is open & (A \/ {a}) /\ E = {x} ) ; ::_thesis: verum
end;
supposeA10: x = a ; ::_thesis: ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} )
now__::_thesis:_ex_G_being_Element_of_bool_the_carrier_of_X_st_
(_G_is_open_&_(A_\/_{a})_/\_G_=_{x}_)
take G = ([#] X) \ (Cl A); ::_thesis: ( G is open & (A \/ {a}) /\ G = {x} )
A11: (A \/ {a}) /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23;
A12: G = (Cl A) ` ;
hence G is open ; ::_thesis: (A \/ {a}) /\ G = {x}
A c= Cl A by PRE_TOPC:18;
then A misses G by A12, SUBSET_1:24;
then A13: A /\ G = {} by XBOOLE_0:def_7;
{a} c= G by A4, ZFMISC_1:31;
hence (A \/ {a}) /\ G = {x} by A10, A13, A11, XBOOLE_1:28; ::_thesis: verum
end;
hence ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} ) ; ::_thesis: verum
end;
end;
end;
hence ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} ) ; ::_thesis: verum
end;
A c= Cl A by PRE_TOPC:18;
then A14: not a in A by A4, XBOOLE_0:def_5;
ex D being Subset of X st
( D is discrete & A c= D & A <> D )
proof
take A \/ {a} ; ::_thesis: ( A \/ {a} is discrete & A c= A \/ {a} & A <> A \/ {a} )
thus A \/ {a} is discrete by A6, Th31; ::_thesis: ( A c= A \/ {a} & A <> A \/ {a} )
thus A c= A \/ {a} by XBOOLE_1:7; ::_thesis: A <> A \/ {a}
now__::_thesis:_not_A_=_A_\/_{a}
assume A = A \/ {a} ; ::_thesis: contradiction
then {a} c= A by XBOOLE_1:7;
hence contradiction by A14, ZFMISC_1:31; ::_thesis: verum
end;
hence A <> A \/ {a} ; ::_thesis: verum
end;
hence contradiction by A2, Def5; ::_thesis: verum
end;
theorem :: TEX_2:42
for X being non empty TopSpace
for A being Subset of X st A is dense & A is discrete holds
A is maximal_discrete
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is dense & A is discrete holds
A is maximal_discrete
let A be Subset of X; ::_thesis: ( A is dense & A is discrete implies A is maximal_discrete )
assume A1: A is dense ; ::_thesis: ( not A is discrete or A is maximal_discrete )
assume A2: A is discrete ; ::_thesis: A is maximal_discrete
assume not A is maximal_discrete ; ::_thesis: contradiction
then consider D being Subset of X such that
A3: D is discrete and
A4: A c= D and
A5: A <> D by A2, Def5;
D \ A <> {} by A4, A5, Lm3;
then consider a being set such that
A6: a in D \ A by XBOOLE_0:def_1;
reconsider a = a as Point of X by A6;
a in D by A6, XBOOLE_0:def_5;
then consider G being Subset of X such that
A7: G is open and
A8: D /\ G = {a} by A3, Th26;
A9: now__::_thesis:_not_A_/\_G_=_{a}
assume A /\ G = {a} ; ::_thesis: contradiction
then {a} c= A by XBOOLE_1:17;
then a in A by ZFMISC_1:31;
hence contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
A /\ G c= D /\ G by A4, XBOOLE_1:26;
then ( A /\ G = {} or A /\ G = {a} ) by A8, ZFMISC_1:33;
then ( A misses G or A /\ G = {a} ) by XBOOLE_0:def_7;
then Cl A misses G by A7, A9, TSEP_1:36;
then A10: (Cl A) /\ G = {} by XBOOLE_0:def_7;
now__::_thesis:_not_Cl_A_=_the_carrier_of_X
assume Cl A = the carrier of X ; ::_thesis: contradiction
then G = {} by A10, XBOOLE_1:28;
hence contradiction by A8; ::_thesis: verum
end;
hence contradiction by A1, TOPS_3:def_2; ::_thesis: verum
end;
theorem Th43: :: TEX_2:43
for X being non empty discrete TopSpace
for A being Subset of X holds
( A is maximal_discrete iff not A is proper )
proof
let X be non empty discrete TopSpace; ::_thesis: for A being Subset of X holds
( A is maximal_discrete iff not A is proper )
let A be Subset of X; ::_thesis: ( A is maximal_discrete iff not A is proper )
hereby ::_thesis: ( not A is proper implies A is maximal_discrete )
X is SubSpace of X by TSEP_1:2;
then reconsider C = the carrier of X as Subset of X by TSEP_1:1;
assume A1: A is maximal_discrete ; ::_thesis: not A is proper
C is discrete by Th21;
then A = C by A1, Def5;
hence not A is proper by SUBSET_1:def_6; ::_thesis: verum
end;
hereby ::_thesis: verum
assume not A is proper ; ::_thesis: A is maximal_discrete
then A2: A = the carrier of X by SUBSET_1:def_6;
then A3: for D being Subset of X st D is discrete & A c= D holds
A = D by XBOOLE_0:def_10;
A is discrete by A2, Th21;
hence A is maximal_discrete by A3, Def5; ::_thesis: verum
end;
end;
theorem Th44: :: TEX_2:44
for X being non empty anti-discrete TopSpace
for A being non empty Subset of X holds
( A is maximal_discrete iff A is trivial )
proof
let X be non empty anti-discrete TopSpace; ::_thesis: for A being non empty Subset of X holds
( A is maximal_discrete iff A is trivial )
let A be non empty Subset of X; ::_thesis: ( A is maximal_discrete iff A is trivial )
hereby ::_thesis: ( A is trivial implies A is maximal_discrete )
assume A is maximal_discrete ; ::_thesis: A is trivial
then A is discrete by Def5;
hence A is trivial by Th38; ::_thesis: verum
end;
hereby ::_thesis: verum
A1: now__::_thesis:_for_D_being_Subset_of_X_st_D_is_discrete_&_A_c=_D_holds_
A_=_D
let D be Subset of X; ::_thesis: ( D is discrete & A c= D implies A = D )
assume A2: D is discrete ; ::_thesis: ( A c= D implies A = D )
assume A3: A c= D ; ::_thesis: A = D
then reconsider E = D as non empty Subset of X ;
E is trivial by A2, Th38;
hence A = D by A3, Th1; ::_thesis: verum
end;
assume A is trivial ; ::_thesis: A is maximal_discrete
then A is discrete by Th38;
hence A is maximal_discrete by A1, Def5; ::_thesis: verum
end;
end;
definition
let Y be non empty TopStruct ;
let IT be SubSpace of Y;
attrIT is maximal_discrete means :Def6: :: TEX_2:def 6
for A being Subset of Y st A = the carrier of IT holds
A is maximal_discrete ;
end;
:: deftheorem Def6 defines maximal_discrete TEX_2:def_6_:_
for Y being non empty TopStruct
for IT being SubSpace of Y holds
( IT is maximal_discrete iff for A being Subset of Y st A = the carrier of IT holds
A is maximal_discrete );
theorem Th45: :: TEX_2:45
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_discrete iff Y0 is maximal_discrete )
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_discrete iff Y0 is maximal_discrete )
let Y0 be SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 holds
( A is maximal_discrete iff Y0 is maximal_discrete )
let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 implies ( A is maximal_discrete iff Y0 is maximal_discrete ) )
assume A1: A = the carrier of Y0 ; ::_thesis: ( A is maximal_discrete iff Y0 is maximal_discrete )
hereby ::_thesis: ( Y0 is maximal_discrete implies A is maximal_discrete )
assume A is maximal_discrete ; ::_thesis: Y0 is maximal_discrete
then for A being Subset of Y st A = the carrier of Y0 holds
A is maximal_discrete by A1;
hence Y0 is maximal_discrete by Def6; ::_thesis: verum
end;
thus ( Y0 is maximal_discrete implies A is maximal_discrete ) by A1, Def6; ::_thesis: verum
end;
registration
let Y be non empty TopStruct ;
cluster non empty maximal_discrete -> non empty discrete for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is maximal_discrete holds
b1 is discrete
proof
let Y0 be non empty SubSpace of Y; ::_thesis: ( Y0 is maximal_discrete implies Y0 is discrete )
reconsider A = the carrier of Y0 as Subset of Y by Lm1;
assume Y0 is maximal_discrete ; ::_thesis: Y0 is discrete
then A is maximal_discrete by Def6;
then A is discrete by Def5;
hence Y0 is discrete by Th20; ::_thesis: verum
end;
cluster non empty non discrete -> non empty non maximal_discrete for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st not b1 is discrete holds
not b1 is maximal_discrete ;
end;
theorem :: TEX_2:46
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is maximal_discrete iff ( X0 is discrete & ( for Y0 being non empty discrete 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
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X holds
( X0 is maximal_discrete iff ( X0 is discrete & ( for Y0 being non empty discrete 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 #) ) ) )
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is maximal_discrete iff ( X0 is discrete & ( for Y0 being non empty discrete 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 #) ) ) )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
hereby ::_thesis: ( X0 is discrete & ( for Y0 being non empty discrete 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_discrete )
assume X0 is maximal_discrete ; ::_thesis: ( X0 is discrete & ( for Y0 being non empty discrete 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_discrete by Th45;
then A is discrete by Def5;
hence X0 is discrete by Th20; ::_thesis: for Y0 being non empty discrete 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 discrete 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 discrete 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 discrete by Th20;
then A = D by A1, A2, Def5;
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;
hereby ::_thesis: verum
assume X0 is discrete ; ::_thesis: ( ( for Y0 being non empty discrete 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_discrete )
then A3: A is discrete by Th20;
assume A4: for Y0 being non empty discrete 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_discrete
now__::_thesis:_for_D_being_Subset_of_X_st_D_is_discrete_&_A_c=_D_holds_
A_=_D
let D be Subset of X; ::_thesis: ( D is discrete & A c= D implies A = D )
assume A5: D is discrete ; ::_thesis: ( A c= D implies A = D )
assume A6: A c= D ; ::_thesis: A = D
then D <> {} ;
then consider Y0 being non empty strict discrete SubSpace of X such that
A7: D = the carrier of Y0 by A5, Th28;
X0 is SubSpace of Y0 by A6, A7, TSEP_1:4;
hence A = D by A4, A7; ::_thesis: verum
end;
then A is maximal_discrete by A3, Def5;
hence X0 is maximal_discrete by Th45; ::_thesis: verum
end;
end;
theorem Th47: :: TEX_2:47
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is maximal_discrete holds
ex X0 being non empty strict SubSpace of X st
( X0 is maximal_discrete & 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_discrete holds
ex X0 being non empty strict SubSpace of X st
( X0 is maximal_discrete & A0 = the carrier of X0 )
let A0 be non empty Subset of X; ::_thesis: ( A0 is maximal_discrete implies ex X0 being non empty strict SubSpace of X st
( X0 is maximal_discrete & A0 = the carrier of X0 ) )
assume A1: A0 is maximal_discrete ; ::_thesis: ex X0 being non empty strict SubSpace of X st
( X0 is maximal_discrete & 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_discrete & A0 = the carrier of X0 )
thus ( X0 is maximal_discrete & A0 = the carrier of X0 ) by A1, A2, Th45; ::_thesis: verum
end;
registration
let X be non empty discrete TopSpace;
cluster maximal_discrete -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is maximal_discrete holds
not b1 is proper
proof
let Y0 be SubSpace of X; ::_thesis: ( Y0 is maximal_discrete implies not Y0 is proper )
reconsider A = the carrier of Y0 as Subset of X by Lm1;
assume Y0 is maximal_discrete ; ::_thesis: not Y0 is proper
then A1: A is maximal_discrete by Def6;
now__::_thesis:_ex_A_being_Subset_of_X_st_
(_A_=_the_carrier_of_Y0_&_not_A_is_proper_)
take A = A; ::_thesis: ( A = the carrier of Y0 & not A is proper )
thus A = the carrier of Y0 ; ::_thesis: not A is proper
thus not A is proper by A1, Th43; ::_thesis: verum
end;
hence not Y0 is proper by Def1; ::_thesis: verum
end;
cluster proper -> non maximal_discrete for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper holds
not b1 is maximal_discrete ;
cluster non proper -> maximal_discrete for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is proper holds
b1 is maximal_discrete
proof
let Y0 be SubSpace of X; ::_thesis: ( not Y0 is proper implies Y0 is maximal_discrete )
reconsider A = the carrier of Y0 as Subset of X by Lm1;
assume not Y0 is proper ; ::_thesis: Y0 is maximal_discrete
then not A is proper by Th8;
then for A being Subset of X st A = the carrier of Y0 holds
A is maximal_discrete by Th43;
hence Y0 is maximal_discrete by Def6; ::_thesis: verum
end;
cluster non maximal_discrete -> proper for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is maximal_discrete holds
b1 is proper ;
end;
registration
let X be non empty anti-discrete TopSpace;
cluster non empty maximal_discrete -> non empty trivial for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is maximal_discrete holds
b1 is trivial ;
cluster non empty non trivial -> non empty non maximal_discrete for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is trivial holds
not b1 is maximal_discrete ;
cluster non empty trivial -> non empty maximal_discrete for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is trivial holds
b1 is maximal_discrete
proof
let Y0 be non empty SubSpace of X; ::_thesis: ( Y0 is trivial implies Y0 is maximal_discrete )
assume Y0 is trivial ; ::_thesis: Y0 is maximal_discrete
then for A being Subset of X st A = the carrier of Y0 holds
A is maximal_discrete by Th44;
hence Y0 is maximal_discrete by Def6; ::_thesis: verum
end;
cluster non empty non maximal_discrete -> non empty non trivial for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is maximal_discrete holds
not b1 is trivial ;
end;
begin
scheme :: TEX_2:sch 1
ExChoiceFCol{ F1() -> non empty TopStruct , F2() -> Subset-Family of F1(), P1[ set , set ] } :
ex f being Function of F2(), the carrier of F1() st
for S being Subset of F1() st S in F2() holds
P1[S,f . S]
provided
A1: for S being Subset of F1() st S in F2() holds
ex x being Point of F1() st P1[S,x]
proof
defpred S1[ set , set ] means ( $2 in the carrier of F1() & P1[$1,$2] );
A2: for S being set st S in F2() holds
ex x being set st
( x in the carrier of F1() & S1[S,x] )
proof
let S be set ; ::_thesis: ( S in F2() implies ex x being set st
( x in the carrier of F1() & S1[S,x] ) )
assume A3: S in F2() ; ::_thesis: ex x being set st
( x in the carrier of F1() & S1[S,x] )
then reconsider Q = S as Subset of F1() ;
consider x being Point of F1() such that
A4: P1[Q,x] by A1, A3;
take x ; ::_thesis: ( x in the carrier of F1() & S1[S,x] )
thus ( x in the carrier of F1() & S1[S,x] ) by A4; ::_thesis: verum
end;
consider f being Function such that
A5: dom f = F2() and
A6: rng f c= the carrier of F1() and
A7: for S being set st S in F2() holds
S1[S,f . S] from FUNCT_1:sch_5(A2);
reconsider f = f as Function of F2(), the carrier of F1() by A5, A6, FUNCT_2:def_1, RELSET_1:4;
take f ; ::_thesis: for S being Subset of F1() st S in F2() holds
P1[S,f . S]
thus for S being Subset of F1() st S in F2() holds
P1[S,f . S] by A7; ::_thesis: verum
end;
theorem Th48: :: TEX_2:48
for X being non empty almost_discrete TopSpace
for A being Subset of X holds Cl A = union { (Cl {a}) where a is Point of X : a in A }
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X holds Cl A = union { (Cl {a}) where a is Point of X : a in A }
let A be Subset of X; ::_thesis: Cl A = union { (Cl {a}) where a is Point of X : a in A }
set F = { (Cl {a}) where a is Point of X : a in A } ;
now__::_thesis:_for_C_being_set_st_C_in__{__(Cl_{a})_where_a_is_Point_of_X_:_a_in_A__}__holds_
C_in_bool_the_carrier_of_X
let C be set ; ::_thesis: ( C in { (Cl {a}) where a is Point of X : a in A } implies C in bool the carrier of X )
assume C in { (Cl {a}) where a is Point of X : a in A } ; ::_thesis: C in bool the carrier of X
then ex a being Point of X st
( C = Cl {a} & a in A ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
then reconsider F = { (Cl {a}) where a is Point of X : a in A } as Subset-Family of X by TARSKI:def_3;
reconsider F = F as Subset-Family of X ;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_in_union_F
let x be set ; ::_thesis: ( x in A implies x in union F )
assume A1: x in A ; ::_thesis: x in union F
then reconsider a = x as Point of X ;
Cl {a} in F by A1;
then A2: Cl {a} c= union F by ZFMISC_1:74;
A3: {a} c= Cl {a} by PRE_TOPC:18;
a in {a} by TARSKI:def_1;
then a in Cl {a} by A3;
hence x in union F by A2; ::_thesis: verum
end;
then A4: A c= union F by TARSKI:def_3;
now__::_thesis:_for_C_being_set_st_C_in_F_holds_
C_c=_Cl_A
let C be set ; ::_thesis: ( C in F implies C c= Cl A )
assume C in F ; ::_thesis: C c= Cl A
then consider a being Point of X such that
A5: C = Cl {a} and
A6: a in A ;
{a} c= A by A6, ZFMISC_1:31;
hence C c= Cl A by A5, PRE_TOPC:19; ::_thesis: verum
end;
then A7: union F c= Cl A by ZFMISC_1:76;
now__::_thesis:_for_G_being_Subset_of_X_st_G_in_F_holds_
G_is_open
let G be Subset of X; ::_thesis: ( G in F implies G is open )
assume G in F ; ::_thesis: G is open
then ex a being Point of X st
( G = Cl {a} & a in A ) ;
hence G is open by TDLAT_3:22; ::_thesis: verum
end;
then F is open by TOPS_2:def_1;
then union F is open by TOPS_2:19;
then union F is closed by TDLAT_3:21;
then Cl A c= union F by A4, TOPS_1:5;
hence Cl A = union { (Cl {a}) where a is Point of X : a in A } by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th49: :: TEX_2:49
for X being non empty almost_discrete TopSpace
for a, b being Point of X st a in Cl {b} holds
Cl {a} = Cl {b}
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for a, b being Point of X st a in Cl {b} holds
Cl {a} = Cl {b}
let a, b be Point of X; ::_thesis: ( a in Cl {b} implies Cl {a} = Cl {b} )
assume a in Cl {b} ; ::_thesis: Cl {a} = Cl {b}
then A1: {a} c= Cl {b} by ZFMISC_1:31;
b in Cl {a}
proof
assume not b in Cl {a} ; ::_thesis: contradiction
then A2: {b} misses Cl {a} by ZFMISC_1:50;
Cl {a} is open by TDLAT_3:22;
then Cl {b} misses Cl {a} by A2, TSEP_1:36;
then (Cl {b}) /\ (Cl {a}) = {} by XBOOLE_0:def_7;
then Cl {a} = {} by A1, TOPS_1:5, XBOOLE_1:28;
hence contradiction by PRE_TOPC:18, XBOOLE_1:3; ::_thesis: verum
end;
then {b} c= Cl {a} by ZFMISC_1:31;
then A3: Cl {b} c= Cl {a} by TOPS_1:5;
Cl {a} c= Cl {b} by A1, TOPS_1:5;
hence Cl {a} = Cl {b} by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th50: :: TEX_2:50
for X being non empty almost_discrete TopSpace
for a, b being Point of X holds
( Cl {a} misses Cl {b} or Cl {a} = Cl {b} )
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for a, b being Point of X holds
( Cl {a} misses Cl {b} or Cl {a} = Cl {b} )
let a, b be Point of X; ::_thesis: ( Cl {a} misses Cl {b} or Cl {a} = Cl {b} )
assume (Cl {a}) /\ (Cl {b}) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: Cl {a} = Cl {b}
then consider x being set such that
A1: x in (Cl {a}) /\ (Cl {b}) by XBOOLE_0:def_1;
reconsider x = x as Point of X by A1;
x in Cl {a} by A1, XBOOLE_0:def_4;
then A2: Cl {x} = Cl {a} by Th49;
x in Cl {b} by A1, XBOOLE_0:def_4;
hence Cl {a} = Cl {b} by A2, Th49; ::_thesis: verum
end;
theorem Th51: :: TEX_2:51
for X being non empty almost_discrete TopSpace
for A being Subset of X st ( for x being Point of X st x in A holds
ex F being Subset of X st
( F is closed & A /\ F = {x} ) ) holds
A is discrete
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st ( for x being Point of X st x in A holds
ex F being Subset of X st
( F is closed & A /\ F = {x} ) ) holds
A is discrete
let A be Subset of X; ::_thesis: ( ( for x being Point of X st x in A holds
ex F being Subset of X st
( F is closed & A /\ F = {x} ) ) implies A is discrete )
assume A1: for x being Point of X st x in A holds
ex F being Subset of X st
( F is closed & A /\ F = {x} ) ; ::_thesis: A is discrete
now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_holds_
ex_G_being_Subset_of_X_st_
(_G_is_open_&_A_/\_G_=_{x}_)
let x be Point of X; ::_thesis: ( x in A implies ex G being Subset of X st
( G is open & A /\ G = {x} ) )
assume A2: x in A ; ::_thesis: ex G being Subset of X st
( G is open & A /\ G = {x} )
now__::_thesis:_ex_F_being_Subset_of_X_st_
(_F_is_open_&_A_/\_F_=_{x}_)
consider F being Subset of X such that
A3: F is closed and
A4: A /\ F = {x} by A1, A2;
take F = F; ::_thesis: ( F is open & A /\ F = {x} )
thus F is open by A3, TDLAT_3:22; ::_thesis: A /\ F = {x}
thus A /\ F = {x} by A4; ::_thesis: verum
end;
hence ex G being Subset of X st
( G is open & A /\ G = {x} ) ; ::_thesis: verum
end;
hence A is discrete by Th31; ::_thesis: verum
end;
theorem Th52: :: TEX_2:52
for X being non empty almost_discrete TopSpace
for A being Subset of X st ( for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} ) holds
A is discrete
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st ( for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} ) holds
A is discrete
let A be Subset of X; ::_thesis: ( ( for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} ) implies A is discrete )
assume A1: for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} ; ::_thesis: A is discrete
now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_holds_
ex_F_being_Subset_of_X_st_
(_F_is_closed_&_A_/\_F_=_{x}_)
let x be Point of X; ::_thesis: ( x in A implies ex F being Subset of X st
( F is closed & A /\ F = {x} ) )
assume A2: x in A ; ::_thesis: ex F being Subset of X st
( F is closed & A /\ F = {x} )
now__::_thesis:_ex_F_being_Element_of_bool_the_carrier_of_X_st_
(_F_is_closed_&_A_/\_F_=_{x}_)
take F = Cl {x}; ::_thesis: ( F is closed & A /\ F = {x} )
thus F is closed ; ::_thesis: A /\ F = {x}
thus A /\ F = {x} by A1, A2; ::_thesis: verum
end;
hence ex F being Subset of X st
( F is closed & A /\ F = {x} ) ; ::_thesis: verum
end;
hence A is discrete by Th51; ::_thesis: verum
end;
theorem :: TEX_2:53
for X being non empty almost_discrete TopSpace
for A being Subset of X holds
( A is discrete iff for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} )
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X holds
( A is discrete iff for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} )
let A be Subset of X; ::_thesis: ( A is discrete iff for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} )
thus ( A is discrete implies for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} ) ::_thesis: ( ( for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} ) implies A is discrete )
proof
assume A1: A is discrete ; ::_thesis: for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b}
let a, b be Point of X; ::_thesis: ( a in A & b in A & a <> b implies Cl {a} misses Cl {b} )
assume that
A2: a in A and
A3: b in A ; ::_thesis: ( not a <> b or Cl {a} misses Cl {b} )
A4: A /\ (Cl {b}) = {b} by A1, A3, Th36;
assume A5: a <> b ; ::_thesis: Cl {a} misses Cl {b}
assume (Cl {a}) /\ (Cl {b}) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then A6: Cl {a} meets Cl {b} by XBOOLE_0:def_7;
A /\ (Cl {a}) = {a} by A1, A2, Th36;
then {a} = {b} by A4, A6, Th50;
hence contradiction by A5, ZFMISC_1:3; ::_thesis: verum
end;
assume A7: for a, b being Point of X st a in A & b in A & a <> b holds
Cl {a} misses Cl {b} ; ::_thesis: A is discrete
now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_holds_
not_A_/\_(Cl_{x})_<>_{x}
let x be Point of X; ::_thesis: ( x in A implies not A /\ (Cl {x}) <> {x} )
assume A8: x in A ; ::_thesis: not A /\ (Cl {x}) <> {x}
assume A9: A /\ (Cl {x}) <> {x} ; ::_thesis: contradiction
A10: {x} c= Cl {x} by PRE_TOPC:18;
{x} c= A by A8, ZFMISC_1:31;
then (A /\ (Cl {x})) \ {x} <> {} by A10, A9, Lm3, XBOOLE_1:19;
then consider y being set such that
A11: y in (A /\ (Cl {x})) \ {x} by XBOOLE_0:def_1;
reconsider y = y as Point of X by A11;
not y in {x} by A11, XBOOLE_0:def_5;
then A12: y <> x by TARSKI:def_1;
A13: y in A /\ (Cl {x}) by A11, XBOOLE_0:def_5;
then y in A by XBOOLE_0:def_4;
then Cl {y} misses Cl {x} by A7, A8, A12;
then A14: (Cl {y}) /\ (Cl {x}) = {} by XBOOLE_0:def_7;
y in Cl {x} by A13, XBOOLE_0:def_4;
then Cl {y} = Cl {x} by Th49;
hence contradiction by A14, PRE_TOPC:18, XBOOLE_1:3; ::_thesis: verum
end;
hence A is discrete by Th52; ::_thesis: verum
end;
theorem Th54: :: TEX_2:54
for X being non empty almost_discrete TopSpace
for A being Subset of X holds
( A is discrete iff for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X holds
( A is discrete iff for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )
let A be Subset of X; ::_thesis: ( A is discrete iff for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )
thus ( A is discrete implies for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ) ::_thesis: ( ( for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ) implies A is discrete )
proof
assume A1: A is discrete ; ::_thesis: for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} )
let x be Point of X; ::_thesis: ( x in Cl A implies ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )
A2: Cl A = union { (Cl {a}) where a is Point of X : a in A } by Th48;
assume x in Cl A ; ::_thesis: ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} )
then consider C being set such that
A3: x in C and
A4: C in { (Cl {a}) where a is Point of X : a in A } by A2, TARSKI:def_4;
consider a being Point of X such that
A5: C = Cl {a} and
A6: a in A by A4;
now__::_thesis:_ex_a_being_Point_of_X_st_
(_a_in_A_&_A_/\_(Cl_{x})_=_{a}_)
take a = a; ::_thesis: ( a in A & A /\ (Cl {x}) = {a} )
thus a in A by A6; ::_thesis: A /\ (Cl {x}) = {a}
Cl {x} = Cl {a} by A3, A5, Th49;
hence A /\ (Cl {x}) = {a} by A1, A6, Th36; ::_thesis: verum
end;
hence ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ; ::_thesis: verum
end;
assume A7: for x being Point of X st x in Cl A holds
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ; ::_thesis: A is discrete
for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}
proof
let x be Point of X; ::_thesis: ( x in A implies A /\ (Cl {x}) = {x} )
assume A8: x in A ; ::_thesis: A /\ (Cl {x}) = {x}
A c= Cl A by PRE_TOPC:18;
then A9: ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) by A7, A8;
A10: {x} c= Cl {x} by PRE_TOPC:18;
{x} c= A by A8, ZFMISC_1:31;
hence A /\ (Cl {x}) = {x} by A9, A10, XBOOLE_1:19, ZFMISC_1:18; ::_thesis: verum
end;
hence A is discrete by Th52; ::_thesis: verum
end;
theorem :: TEX_2:55
for X being non empty almost_discrete TopSpace
for A being Subset of X st ( A is open or A is closed ) & A is maximal_discrete holds
not A is proper
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st ( A is open or A is closed ) & A is maximal_discrete holds
not A is proper
let A be Subset of X; ::_thesis: ( ( A is open or A is closed ) & A is maximal_discrete implies not A is proper )
assume A1: ( A is open or A is closed ) ; ::_thesis: ( not A is maximal_discrete or not A is proper )
then A is closed by TDLAT_3:21;
then A2: A = Cl A by PRE_TOPC:22;
assume A3: A is maximal_discrete ; ::_thesis: not A is proper
A is open by A1, TDLAT_3:22;
then A is dense by A3, Th41;
then A = the carrier of X by A2, TOPS_3:def_2;
hence not A is proper by SUBSET_1:def_6; ::_thesis: verum
end;
theorem Th56: :: TEX_2:56
for X being non empty almost_discrete TopSpace
for A being Subset of X st A is maximal_discrete holds
A is dense
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st A is maximal_discrete holds
A is dense
let A be Subset of X; ::_thesis: ( A is maximal_discrete implies A is dense )
assume A1: A is maximal_discrete ; ::_thesis: A is dense
then A2: A is discrete by Def5;
assume not A is dense ; ::_thesis: contradiction
then Cl A <> the carrier of X by TOPS_3:def_2;
then the carrier of X \ (Cl A) <> {} by Lm3;
then consider a being set such that
A3: a in the carrier of X \ (Cl A) by XBOOLE_0:def_1;
reconsider a = a as Point of X by A3;
set B = A \/ {a};
A4: A c= A \/ {a} by XBOOLE_1:7;
A5: now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_\/_{a}_holds_
ex_G_being_Subset_of_X_st_
(_G_is_open_&_(A_\/_{a})_/\_G_=_{x}_)
let x be Point of X; ::_thesis: ( x in A \/ {a} implies ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} ) )
assume x in A \/ {a} ; ::_thesis: ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} )
then A6: ( x in A or x in {a} ) by XBOOLE_0:def_3;
now__::_thesis:_ex_E_being_Subset_of_X_st_
(_E_is_open_&_(A_\/_{a})_/\_E_=_{x}_)
percases ( x in A or x = a ) by A6, TARSKI:def_1;
supposeA7: x in A ; ::_thesis: ex E being Subset of X st
( E is open & (A \/ {a}) /\ E = {x} )
then consider G being Subset of X such that
A8: G is open and
A9: A /\ G = {x} by A2, Th26;
now__::_thesis:_ex_E_being_Element_of_bool_the_carrier_of_X_st_
(_E_is_open_&_(A_\/_{a})_/\_E_=_{x}_)
take E = (Cl A) /\ G; ::_thesis: ( E is open & (A \/ {a}) /\ E = {x} )
A10: (A \/ {a}) /\ E = (A /\ E) \/ ({a} /\ E) by XBOOLE_1:23;
Cl A is open by TDLAT_3:22;
hence E is open by A8; ::_thesis: (A \/ {a}) /\ E = {x}
A11: {x} c= E by A9, PRE_TOPC:18, XBOOLE_1:26;
E c= Cl A by XBOOLE_1:17;
then not a in E by A3, XBOOLE_0:def_5;
then {a} misses E by ZFMISC_1:50;
then A12: {a} /\ E = {} by XBOOLE_0:def_7;
{x} c= A \/ {a} by A4, A7, ZFMISC_1:31;
then A13: {x} c= (A \/ {a}) /\ E by A11, XBOOLE_1:19;
A /\ E c= A /\ G by XBOOLE_1:17, XBOOLE_1:26;
hence (A \/ {a}) /\ E = {x} by A9, A13, A12, A10, XBOOLE_0:def_10; ::_thesis: verum
end;
hence ex E being Subset of X st
( E is open & (A \/ {a}) /\ E = {x} ) ; ::_thesis: verum
end;
supposeA14: x = a ; ::_thesis: ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} )
now__::_thesis:_ex_G_being_Element_of_bool_the_carrier_of_X_st_
(_G_is_open_&_(A_\/_{a})_/\_G_=_{x}_)
take G = ([#] X) \ (Cl A); ::_thesis: ( G is open & (A \/ {a}) /\ G = {x} )
A15: (A \/ {a}) /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23;
A16: G = (Cl A) ` ;
hence G is open ; ::_thesis: (A \/ {a}) /\ G = {x}
A c= Cl A by PRE_TOPC:18;
then A misses G by A16, SUBSET_1:24;
then A17: A /\ G = {} by XBOOLE_0:def_7;
{a} c= G by A3, ZFMISC_1:31;
hence (A \/ {a}) /\ G = {x} by A14, A17, A15, XBOOLE_1:28; ::_thesis: verum
end;
hence ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} ) ; ::_thesis: verum
end;
end;
end;
hence ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} ) ; ::_thesis: verum
end;
A c= Cl A by PRE_TOPC:18;
then A18: not a in A by A3, XBOOLE_0:def_5;
ex D being Subset of X st
( D is discrete & A c= D & A <> D )
proof
take A \/ {a} ; ::_thesis: ( A \/ {a} is discrete & A c= A \/ {a} & A <> A \/ {a} )
thus A \/ {a} is discrete by A5, Th31; ::_thesis: ( A c= A \/ {a} & A <> A \/ {a} )
thus A c= A \/ {a} by XBOOLE_1:7; ::_thesis: A <> A \/ {a}
now__::_thesis:_not_A_=_A_\/_{a}
assume A = A \/ {a} ; ::_thesis: contradiction
then {a} c= A by XBOOLE_1:7;
hence contradiction by A18, ZFMISC_1:31; ::_thesis: verum
end;
hence A <> A \/ {a} ; ::_thesis: verum
end;
hence contradiction by A1, Def5; ::_thesis: verum
end;
theorem Th57: :: TEX_2:57
for X being non empty almost_discrete TopSpace
for A being Subset of X st A is maximal_discrete holds
union { (Cl {a}) where a is Point of X : a in A } = the carrier of X
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st A is maximal_discrete holds
union { (Cl {a}) where a is Point of X : a in A } = the carrier of X
let A be Subset of X; ::_thesis: ( A is maximal_discrete implies union { (Cl {a}) where a is Point of X : a in A } = the carrier of X )
assume A is maximal_discrete ; ::_thesis: union { (Cl {a}) where a is Point of X : a in A } = the carrier of X
then A is dense by Th56;
then Cl A = the carrier of X by TOPS_3:def_2;
hence union { (Cl {a}) where a is Point of X : a in A } = the carrier of X by Th48; ::_thesis: verum
end;
theorem Th58: :: TEX_2:58
for X being non empty almost_discrete TopSpace
for A being Subset of X holds
( A is maximal_discrete iff for x being Point of X ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X holds
( A is maximal_discrete iff for x being Point of X ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )
let A be Subset of X; ::_thesis: ( A is maximal_discrete iff for x being Point of X ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) )
thus ( A is maximal_discrete implies for x being Point of X ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ) ::_thesis: ( ( for x being Point of X ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ) implies A is maximal_discrete )
proof
assume A1: A is maximal_discrete ; ::_thesis: for x being Point of X ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} )
let x be Point of X; ::_thesis: ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} )
the carrier of X = union { (Cl {a}) where a is Point of X : a in A } by A1, Th57;
then consider C being set such that
A2: x in C and
A3: C in { (Cl {a}) where a is Point of X : a in A } by TARSKI:def_4;
consider a being Point of X such that
A4: C = Cl {a} and
A5: a in A by A3;
A6: A is discrete by A1, Def5;
now__::_thesis:_ex_a_being_Point_of_X_st_
(_a_in_A_&_A_/\_(Cl_{x})_=_{a}_)
take a = a; ::_thesis: ( a in A & A /\ (Cl {x}) = {a} )
thus a in A by A5; ::_thesis: A /\ (Cl {x}) = {a}
Cl {x} = Cl {a} by A2, A4, Th49;
hence A /\ (Cl {x}) = {a} by A6, A5, Th36; ::_thesis: verum
end;
hence ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ; ::_thesis: verum
end;
assume A7: for x being Point of X ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) ; ::_thesis: A is maximal_discrete
A8: for D being Subset of X st D is discrete & A c= D holds
A = D
proof
let D be Subset of X; ::_thesis: ( D is discrete & A c= D implies A = D )
assume A9: D is discrete ; ::_thesis: ( not A c= D or A = D )
assume A10: A c= D ; ::_thesis: A = D
now__::_thesis:_for_x_being_set_st_x_in_D_holds_
x_in_A
let x be set ; ::_thesis: ( x in D implies x in A )
assume A11: x in D ; ::_thesis: x in A
then reconsider y = x as Point of X ;
A12: ex a being Point of X st
( a in A & A /\ (Cl {y}) = {a} ) by A7;
D /\ (Cl {y}) = {y} by A9, A11, Th36;
hence x in A by A10, A12, XBOOLE_1:26, ZFMISC_1:18; ::_thesis: verum
end;
then D c= A by TARSKI:def_3;
hence A = D by A10, XBOOLE_0:def_10; ::_thesis: verum
end;
for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}
proof
let x be Point of X; ::_thesis: ( x in A implies A /\ (Cl {x}) = {x} )
A13: {x} c= Cl {x} by PRE_TOPC:18;
assume x in A ; ::_thesis: A /\ (Cl {x}) = {x}
then A14: {x} c= A by ZFMISC_1:31;
ex a being Point of X st
( a in A & A /\ (Cl {x}) = {a} ) by A7;
hence A /\ (Cl {x}) = {x} by A14, A13, XBOOLE_1:19, ZFMISC_1:18; ::_thesis: verum
end;
then A is discrete by Th52;
hence A is maximal_discrete by A8, Def5; ::_thesis: verum
end;
theorem Th59: :: TEX_2:59
for X being non empty almost_discrete TopSpace
for A being Subset of X st A is discrete holds
ex M being Subset of X st
( A c= M & M is maximal_discrete )
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st A is discrete holds
ex M being Subset of X st
( A c= M & M is maximal_discrete )
let A be Subset of X; ::_thesis: ( A is discrete implies ex M being Subset of X st
( A c= M & M is maximal_discrete ) )
set D = ([#] X) \ (Cl A);
set F = { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } ;
now__::_thesis:_for_C_being_set_st_C_in__{__(Cl_{d})_where_d_is_Point_of_X_:_d_in_([#]_X)_\_(Cl_A)__}__holds_
C_in_bool_the_carrier_of_X
let C be set ; ::_thesis: ( C in { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } implies C in bool the carrier of X )
assume C in { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } ; ::_thesis: C in bool the carrier of X
then ex a being Point of X st
( C = Cl {a} & a in ([#] X) \ (Cl A) ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
then reconsider F = { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } as Subset-Family of X by TARSKI:def_3;
assume A1: A is discrete ; ::_thesis: ex M being Subset of X st
( A c= M & M is maximal_discrete )
defpred S1[ set , set ] means ( $2 in ([#] X) \ (Cl A) & $2 in $1 );
A2: ([#] X) \ (Cl A) = (Cl A) ` ;
then ([#] X) \ (Cl A) is closed by TDLAT_3:21;
then A3: ([#] X) \ (Cl A) = Cl (([#] X) \ (Cl A)) by PRE_TOPC:22;
A c= Cl A by PRE_TOPC:18;
then A misses ([#] X) \ (Cl A) by A2, SUBSET_1:24;
then A4: A /\ (([#] X) \ (Cl 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 = Cl {d} and
A7: d in ([#] X) \ (Cl A) ;
take d ; ::_thesis: S1[S,d]
{d} c= Cl {d} by PRE_TOPC: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)_\_(Cl_A)
let x be set ; ::_thesis: ( x in f .: F implies x in ([#] X) \ (Cl A) )
assume x in f .: F ; ::_thesis: x in ([#] X) \ (Cl A)
then ex S being set st
( S in F & S in F & x = f . S ) by FUNCT_2:64;
hence x in ([#] X) \ (Cl A) by A8; ::_thesis: verum
end;
then A9: f .: F c= ([#] X) \ (Cl A) by TARSKI:def_3;
([#] X) \ (Cl A) misses Cl A by A2, SUBSET_1:24;
then A10: Cl A misses f .: F by A9, XBOOLE_1:63;
thus ex M being Subset of X st
( A c= M & M is maximal_discrete ) ::_thesis: verum
proof
take A \/ (f .: F) ; ::_thesis: ( A c= A \/ (f .: F) & A \/ (f .: F) is maximal_discrete )
thus A11: A c= A \/ (f .: F) by XBOOLE_1:7; ::_thesis: A \/ (f .: F) is maximal_discrete
for x being Point of X ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {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)) /\ (Cl {x}) = {a} )
A12: [#] X = (Cl A) \/ (([#] X) \ (Cl A)) by XBOOLE_1:45;
now__::_thesis:_ex_a_being_Point_of_X_st_
(_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(Cl_{x})_=_{a}_)
percases ( x in Cl A or x in ([#] X) \ (Cl A) ) by A12, XBOOLE_0:def_3;
supposeA13: x in Cl A ; ::_thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
now__::_thesis:_ex_a_being_Point_of_X_st_
(_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(Cl_{x})_=_{a}_)
consider a being Point of X such that
A14: a in A and
A15: A /\ (Cl {x}) = {a} by A1, A13, Th54;
take a = a; ::_thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
thus a in A \/ (f .: F) by A11, A14; ::_thesis: (A \/ (f .: F)) /\ (Cl {x}) = {a}
{x} c= Cl A by A13, ZFMISC_1:31;
then f .: F misses Cl {x} by A10, TOPS_1:5, XBOOLE_1:63;
then (f .: F) /\ (Cl {x}) = {} by XBOOLE_0:def_7;
then (A \/ (f .: F)) /\ (Cl {x}) = (A /\ (Cl {x})) \/ {} by XBOOLE_1:23;
hence (A \/ (f .: F)) /\ (Cl {x}) = {a} by A15; ::_thesis: verum
end;
hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) ; ::_thesis: verum
end;
supposeA16: x in ([#] X) \ (Cl A) ; ::_thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
then A17: Cl {x} in F ;
now__::_thesis:_ex_a_being_Point_of_X_st_
(_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(Cl_{x})_=_{a}_)
reconsider a = f . (Cl {x}) as Point of X by A17, FUNCT_2:5;
take a = a; ::_thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
A18: f .: F c= A \/ (f .: F) by XBOOLE_1:7;
now__::_thesis:_for_y_being_set_st_y_in_(A_\/_(f_.:_F))_/\_(Cl_{x})_holds_
y_in_{a}
let y be set ; ::_thesis: ( y in (A \/ (f .: F)) /\ (Cl {x}) implies y in {a} )
assume A19: y in (A \/ (f .: F)) /\ (Cl {x}) ; ::_thesis: y in {a}
then reconsider z = y as Point of X ;
A20: z in Cl {x} by A19, XBOOLE_0:def_4;
A21: z in A \/ (f .: F) by A19, XBOOLE_0:def_4;
{x} c= ([#] X) \ (Cl A) by A16, ZFMISC_1:31;
then Cl {x} c= ([#] X) \ (Cl A) by A3, PRE_TOPC:19;
then not z in A by A4, A20, XBOOLE_0:def_4;
then z in f .: F by A21, XBOOLE_0:def_3;
then consider C being set such that
A22: C in F and
C in F and
A23: z = f . C by FUNCT_2:64;
reconsider C = C as Subset of X by A22;
consider w being Point of X such that
A24: C = Cl {w} and
w in ([#] X) \ (Cl A) by A22;
Cl {z} = Cl {x} by A20, Th49;
then f . (Cl {w}) = a by A8, A22, A23, A24, Th49;
hence y in {a} by A23, A24, TARSKI:def_1; ::_thesis: verum
end;
then A25: (A \/ (f .: F)) /\ (Cl {x}) c= {a} by TARSKI:def_3;
A26: a in f .: F by A17, FUNCT_2:35;
hence a in A \/ (f .: F) by A18; ::_thesis: (A \/ (f .: F)) /\ (Cl {x}) = {a}
a in Cl {x} by A8, A17;
then A27: {a} c= Cl {x} by ZFMISC_1:31;
{a} c= A \/ (f .: F) by A18, A26, ZFMISC_1:31;
then {a} c= (A \/ (f .: F)) /\ (Cl {x}) by A27, XBOOLE_1:19;
hence (A \/ (f .: F)) /\ (Cl {x}) = {a} by A25, XBOOLE_0:def_10; ::_thesis: verum
end;
hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) ; ::_thesis: verum
end;
end;
end;
hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) ; ::_thesis: verum
end;
hence A \/ (f .: F) is maximal_discrete by Th58; ::_thesis: verum
end;
end;
theorem Th60: :: TEX_2:60
for X being non empty almost_discrete TopSpace ex M being Subset of X st M is maximal_discrete
proof
let X be non empty almost_discrete TopSpace; ::_thesis: ex M being Subset of X st M is maximal_discrete
set A = {} X;
{} X is discrete by Th29;
then consider M being Subset of X such that
{} X c= M and
A1: M is maximal_discrete by Th59;
take M ; ::_thesis: M is maximal_discrete
thus M is maximal_discrete by A1; ::_thesis: verum
end;
theorem Th61: :: TEX_2:61
for X being non empty almost_discrete TopSpace
for Y0 being non empty discrete SubSpace of X ex X0 being non empty strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_discrete )
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for Y0 being non empty discrete SubSpace of X ex X0 being non empty strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_discrete )
let Y0 be non empty discrete SubSpace of X; ::_thesis: ex X0 being non empty strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_discrete )
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
A is discrete by Th20;
then consider M being Subset of X such that
A1: A c= M and
A2: M is maximal_discrete by Th59;
not M is empty by A2, Th40;
then consider X0 being non empty strict SubSpace of X such that
A3: X0 is maximal_discrete and
A4: M = the carrier of X0 by A2, Th47;
take X0 ; ::_thesis: ( Y0 is SubSpace of X0 & X0 is maximal_discrete )
thus ( Y0 is SubSpace of X0 & X0 is maximal_discrete ) by A1, A3, A4, TSEP_1:4; ::_thesis: verum
end;
registration
let X be non empty non discrete almost_discrete TopSpace;
cluster non empty maximal_discrete -> non empty proper for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is maximal_discrete holds
b1 is proper
proof
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is maximal_discrete implies X0 is proper )
reconsider A = the carrier of X0 as Subset of X by Lm1;
assume X0 is maximal_discrete ; ::_thesis: X0 is proper
then A is maximal_discrete by Def6;
then A is discrete by Def5;
then A1: X0 is discrete by Th20;
X0 is proper
proof
assume not X0 is proper ; ::_thesis: contradiction
then not A is proper by Th8;
then A2: A = the carrier of X by SUBSET_1:def_6;
X is SubSpace of X by TSEP_1:2;
then TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) by A2, TSEP_1:5;
hence contradiction by A1, Th12; ::_thesis: verum
end;
hence X0 is proper ; ::_thesis: verum
end;
cluster non empty non proper -> non empty non maximal_discrete for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is proper holds
not b1 is maximal_discrete ;
end;
registration
let X be non empty non anti-discrete almost_discrete TopSpace;
cluster non empty maximal_discrete -> non empty non trivial for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is maximal_discrete holds
not b1 is trivial
proof
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is maximal_discrete implies not X0 is trivial )
reconsider A = the carrier of X0 as non empty Subset of X by Lm1;
assume X0 is maximal_discrete ; ::_thesis: not X0 is trivial
then A is maximal_discrete by Def6;
then A is dense by Th56;
then A1: Cl A = the carrier of X by TOPS_3:def_2;
assume X0 is trivial ; ::_thesis: contradiction
then consider s being Element of X0 such that
A2: the carrier of X0 = {s} by SUBSET_1:46;
s in A ;
then reconsider a = s as Point of X ;
A = {a} by A2;
then for C being Subset of X
for x being Point of X st C = {x} holds
Cl C = the carrier of X by A1, Th49;
hence contradiction by TDLAT_3:20; ::_thesis: verum
end;
cluster non empty trivial -> non empty non maximal_discrete for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is trivial holds
not b1 is maximal_discrete ;
end;
registration
let X be non empty almost_discrete TopSpace;
cluster non empty strict TopSpace-like maximal_discrete for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is maximal_discrete & b1 is strict & not b1 is empty & not b1 is empty )
proof
consider M being Subset of X such that
A1: M is maximal_discrete by Th60;
not M is empty by A1, Th40;
then consider X0 being non empty strict SubSpace of X such that
A2: X0 is maximal_discrete and
M = the carrier of X0 by A1, Th47;
take X0 ; ::_thesis: ( X0 is maximal_discrete & X0 is strict & not X0 is empty & not X0 is empty )
thus ( X0 is maximal_discrete & X0 is strict & not X0 is empty & not X0 is empty ) by A2; ::_thesis: verum
end;
end;
begin
theorem Th62: :: TEX_2:62
for X being discrete TopSpace
for Y being TopSpace
for f being Function of X,Y holds f is continuous
proof
let X be discrete TopSpace; ::_thesis: for Y being TopSpace
for f being Function of X,Y holds f is continuous
let Y be TopSpace; ::_thesis: for f being Function of X,Y holds f is continuous
let f be Function of X,Y; ::_thesis: f is continuous
for B being Subset of Y st B is closed holds
f " B is closed by TDLAT_3:16;
hence f is continuous by PRE_TOPC:def_6; ::_thesis: verum
end;
theorem :: TEX_2:63
for X being non empty TopSpace st ( for Y being non empty TopSpace
for f being Function of X,Y holds f is continuous ) holds
X is discrete
proof
let X be non empty TopSpace; ::_thesis: ( ( for Y being non empty TopSpace
for f being Function of X,Y holds f is continuous ) implies X is discrete )
set Y = 1TopSp the carrier of X;
reconsider f = id the carrier of X as Function of X,(1TopSp the carrier of X) ;
assume for Y being non empty TopSpace
for f being Function of X,Y holds f is continuous ; ::_thesis: X is discrete
then A1: f is continuous ;
for A being Subset of X holds A is closed
proof
let A be Subset of X; ::_thesis: A is closed
reconsider B = A as Subset of (1TopSp the carrier of X) ;
A2: f " B = A by FUNCT_2:94;
B is closed by TDLAT_3:16;
hence A is closed by A1, A2, PRE_TOPC:def_6; ::_thesis: verum
end;
hence X is discrete by TDLAT_3:16; ::_thesis: verum
end;
theorem :: TEX_2:64
for X being non empty TopSpace
for Y being non empty anti-discrete TopSpace
for f being Function of X,Y holds f is continuous
proof
let X be non empty TopSpace; ::_thesis: for Y being non empty anti-discrete TopSpace
for f being Function of X,Y holds f is continuous
let Y be non empty anti-discrete TopSpace; ::_thesis: for f being Function of X,Y holds f is continuous
let f be Function of X,Y; ::_thesis: f is continuous
now__::_thesis:_for_B_being_Subset_of_Y_st_B_is_closed_holds_
f_"_B_is_closed
let B be Subset of Y; ::_thesis: ( B is closed implies f " B is closed )
assume A1: B is closed ; ::_thesis: f " B is closed
now__::_thesis:_f_"_B_is_closed
percases ( B = {} or B = the carrier of Y ) by A1, TDLAT_3:19;
suppose B = {} ; ::_thesis: f " B is closed
then f " B = {} X ;
hence f " B is closed ; ::_thesis: verum
end;
suppose B = the carrier of Y ; ::_thesis: f " B is closed
then B = [#] Y ;
then f " B = [#] X by TOPS_2:41;
hence f " B is closed ; ::_thesis: verum
end;
end;
end;
hence f " B is closed ; ::_thesis: verum
end;
hence f is continuous by PRE_TOPC:def_6; ::_thesis: verum
end;
theorem :: TEX_2:65
for Y being non empty TopSpace st ( for X being non empty TopSpace
for f being Function of X,Y holds f is continuous ) holds
Y is anti-discrete
proof
let Y be non empty TopSpace; ::_thesis: ( ( for X being non empty TopSpace
for f being Function of X,Y holds f is continuous ) implies Y is anti-discrete )
set X = ADTS the carrier of Y;
A1: ADTS the carrier of Y = TopStruct(# the carrier of Y,(cobool the carrier of Y) #) by TEX_1:def_3;
then reconsider f = id the carrier of Y as Function of (ADTS the carrier of Y),Y ;
assume for X being non empty TopSpace
for f being Function of X,Y holds f is continuous ; ::_thesis: Y is anti-discrete
then A2: f is continuous ;
for A being Subset of Y holds
( not A is closed or A = {} or A = the carrier of Y )
proof
let A be Subset of Y; ::_thesis: ( not A is closed or A = {} or A = the carrier of Y )
reconsider B = A as Subset of (ADTS the carrier of Y) by A1;
A3: f " A = B by FUNCT_2:94;
assume A is closed ; ::_thesis: ( A = {} or A = the carrier of Y )
then B is closed by A2, A3, PRE_TOPC:def_6;
hence ( A = {} or A = the carrier of Y ) by A1, TDLAT_3:19; ::_thesis: verum
end;
hence Y is anti-discrete by TDLAT_3:19; ::_thesis: verum
end;
theorem Th66: :: TEX_2:66
for X being non empty discrete TopSpace
for X0 being non empty SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
proof
let X be non empty discrete TopSpace; ::_thesis: for X0 being non empty SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
let X0 be non empty SubSpace of X; ::_thesis: ex r being continuous Function of X,X0 st r is being_a_retraction
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
defpred S1[ set , set ] means ( $1 in A implies $2 = $1 );
A1: for x being Point of X ex a being Point of X0 st S1[x,a] ;
consider r being Function of X,X0 such that
A2: for x being Point of X holds S1[x,r . x] from FUNCT_2:sch_3(A1);
reconsider r = r as continuous Function of X,X0 by Th62;
take r ; ::_thesis: r is being_a_retraction
thus r is being_a_retraction by A2, BORSUK_1:def_16; ::_thesis: verum
end;
theorem :: TEX_2:67
for X being non empty discrete TopSpace
for X0 being non empty SubSpace of X holds X0 is_a_retract_of X
proof
let X be non empty discrete TopSpace; ::_thesis: for X0 being non empty SubSpace of X holds X0 is_a_retract_of X
let X0 be non empty 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 Th66;
hence X0 is_a_retract_of X by BORSUK_1:def_17; ::_thesis: verum
end;
theorem Th68: :: TEX_2:68
for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty maximal_discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
let X0 be non empty maximal_discrete SubSpace of X; ::_thesis: ex r being continuous Function of X,X0 st r is being_a_retraction
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
defpred S1[ Point of X, Point of X0] means A /\ (Cl {$1}) = {$2};
A1: A is maximal_discrete by Th45;
then A2: A is discrete by Def5;
A3: 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
A4: a in A and
A5: A /\ (Cl {x}) = {a} by A1, Th58;
reconsider a = a as Point of X0 by A4;
take a ; ::_thesis: S1[x,a]
thus S1[x,a] by A5; ::_thesis: verum
end;
consider r being Function of X,X0 such that
A6: for x being Point of X holds S1[x,r . x] from FUNCT_2:sch_3(A3);
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 )
assume F is closed ; ::_thesis: r " F is closed
F c= A ;
then reconsider E = F as Subset of X by XBOOLE_1:1;
set R = { (Cl {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__{__(Cl_{a})_where_a_is_Point_of_X_:_a_in_E__}_
let x be set ; ::_thesis: ( x in r " F implies x in union { (Cl {a}) where a is Point of X : a in E } )
assume A7: x in r " F ; ::_thesis: x in union { (Cl {a}) where a is Point of X : a in E }
then reconsider b = x as Point of X ;
A8: r . b in F by A7, FUNCT_2:38;
E c= the carrier of X ;
then reconsider a = r . b as Point of X by A8;
Cl {a} in { (Cl {a}) where a is Point of X : a in E } by A8;
then A9: Cl {a} c= union { (Cl {a}) where a is Point of X : a in E } by ZFMISC_1:74;
A /\ (Cl {b}) = {a} by A6;
then a in A /\ (Cl {b}) by ZFMISC_1:31;
then a in Cl {b} by XBOOLE_0:def_4;
then A10: Cl {a} = Cl {b} by Th49;
A11: {b} c= Cl {b} by PRE_TOPC:18;
b in {b} by TARSKI:def_1;
then b in Cl {a} by A10, A11;
hence x in union { (Cl {a}) where a is Point of X : a in E } by A9; ::_thesis: verum
end;
then A12: r " F c= union { (Cl {a}) where a is Point of X : a in E } by TARSKI:def_3;
now__::_thesis:_for_C_being_set_st_C_in__{__(Cl_{a})_where_a_is_Point_of_X_:_a_in_E__}__holds_
C_c=_r_"_F
let C be set ; ::_thesis: ( C in { (Cl {a}) where a is Point of X : a in E } implies C c= r " F )
assume C in { (Cl {a}) where a is Point of X : a in E } ; ::_thesis: C c= r " F
then consider a being Point of X such that
A13: C = Cl {a} and
A14: 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 A15: x in C ; ::_thesis: x in r " F
then reconsider b = x as Point of X by A13;
A16: A /\ (Cl {b}) = {(r . b)} by A6;
A17: A /\ (Cl {a}) = {a} by A2, A14, Th36;
Cl {a} = Cl {b} by A13, A15, Th49;
then a = r . x by A17, A16, ZFMISC_1:3;
hence x in r " F by A13, A14, A15, FUNCT_2:38; ::_thesis: verum
end;
hence C c= r " F by TARSKI:def_3; ::_thesis: verum
end;
then A18: union { (Cl {a}) where a is Point of X : a in E } c= r " F by ZFMISC_1:76;
Cl E = union { (Cl {a}) where a is Point of X : a in E } by Th48;
hence r " F is closed by A18, A12, XBOOLE_0:def_10; ::_thesis: verum
end;
then reconsider r = r as continuous Function of X,X0 by PRE_TOPC:def_6;
take r ; ::_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 A19: A /\ (Cl {x}) = {x} by A2, Th36;
A /\ (Cl {x}) = {(r . x)} by A6;
hence r . x = x by A19, ZFMISC_1:3; ::_thesis: verum
end;
hence r is being_a_retraction by BORSUK_1:def_16; ::_thesis: verum
end;
theorem :: TEX_2:69
for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X holds X0 is_a_retract_of X
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty maximal_discrete SubSpace of X holds X0 is_a_retract_of X
let X0 be non empty maximal_discrete 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 Th68;
hence X0 is_a_retract_of X by BORSUK_1:def_17; ::_thesis: verum
end;
Lm4: for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}
let X0 be non empty maximal_discrete SubSpace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}
let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a} )
assume A1: r is being_a_retraction ; ::_thesis: for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}
let a be Point of X0; ::_thesis: for b being Point of X st a = b holds
Cl {b} c= r " {a}
let b be Point of X; ::_thesis: ( a = b implies Cl {b} c= r " {a} )
assume a = b ; ::_thesis: Cl {b} c= r " {a}
then A2: r . b = a by A1, BORSUK_1:def_16;
a in {a} by TARSKI:def_1;
then b in r " {a} by A2, FUNCT_2:38;
then A3: {b} c= r " {a} by ZFMISC_1:31;
{a} is closed by TDLAT_3:16;
then r " {a} is closed by PRE_TOPC:def_6;
hence Cl {b} c= r " {a} by A3, TOPS_1:5; ::_thesis: verum
end;
theorem Th70: :: TEX_2:70
for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E
let X0 be non empty maximal_discrete SubSpace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds
for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E
let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: A is maximal_discrete by Th45;
assume A2: r is being_a_retraction ; ::_thesis: for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E
A3: for a being Point of X holds A /\ (Cl {a}) = {(r . a)}
proof
let a be Point of X; ::_thesis: A /\ (Cl {a}) = {(r . a)}
A4: {a} c= Cl {a} by PRE_TOPC:18;
consider c being Point of X such that
A5: c in A and
A6: A /\ (Cl {a}) = {c} by A1, Th58;
reconsider b = c as Point of X0 by A5;
{c} c= Cl {a} by A6, XBOOLE_1:17;
then A7: c in Cl {a} by ZFMISC_1:31;
Cl {c} c= r " {b} by A2, Lm4;
then Cl {a} c= r " {b} by A7, Th49;
then {a} c= r " {b} by A4, XBOOLE_1:1;
then a in r " {b} by ZFMISC_1:31;
then r . a in {b} by FUNCT_2:38;
hence A /\ (Cl {a}) = {(r . a)} by A6, TARSKI:def_1; ::_thesis: verum
end;
let F be Subset of X0; ::_thesis: for E being Subset of X st F = E holds
r " F = Cl E
let E be Subset of X; ::_thesis: ( F = E implies r " F = Cl E )
set R = { (Cl {a}) where a is Point of X : a in E } ;
assume A8: F = E ; ::_thesis: r " F = Cl E
now__::_thesis:_for_x_being_set_st_x_in_r_"_F_holds_
x_in_union__{__(Cl_{a})_where_a_is_Point_of_X_:_a_in_E__}_
let x be set ; ::_thesis: ( x in r " F implies x in union { (Cl {a}) where a is Point of X : a in E } )
assume A9: x in r " F ; ::_thesis: x in union { (Cl {a}) where a is Point of X : a in E }
then reconsider b = x as Point of X ;
A10: r . b in F by A9, FUNCT_2:38;
then reconsider a = r . b as Point of X by A8;
Cl {a} in { (Cl {a}) where a is Point of X : a in E } by A8, A10;
then A11: Cl {a} c= union { (Cl {a}) where a is Point of X : a in E } by ZFMISC_1:74;
A12: {b} c= Cl {b} by PRE_TOPC:18;
A /\ (Cl {b}) = {a} by A3;
then a in A /\ (Cl {b}) by ZFMISC_1:31;
then a in Cl {b} by XBOOLE_0:def_4;
then A13: Cl {a} = Cl {b} by Th49;
b in {b} by TARSKI:def_1;
then b in Cl {a} by A13, A12;
hence x in union { (Cl {a}) where a is Point of X : a in E } by A11; ::_thesis: verum
end;
then A14: r " F c= union { (Cl {a}) where a is Point of X : a in E } by TARSKI:def_3;
A15: A is discrete by A1, Def5;
now__::_thesis:_for_C_being_set_st_C_in__{__(Cl_{a})_where_a_is_Point_of_X_:_a_in_E__}__holds_
C_c=_r_"_F
let C be set ; ::_thesis: ( C in { (Cl {a}) where a is Point of X : a in E } implies C c= r " F )
assume C in { (Cl {a}) where a is Point of X : a in E } ; ::_thesis: C c= r " F
then consider a being Point of X such that
A16: C = Cl {a} and
A17: 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 A18: x in C ; ::_thesis: x in r " F
then reconsider b = x as Point of X by A16;
A19: A /\ (Cl {b}) = {(r . b)} by A3;
A20: A /\ (Cl {a}) = {a} by A8, A15, A17, Th36;
Cl {a} = Cl {b} by A16, A18, Th49;
then a = r . x by A20, A19, ZFMISC_1:3;
hence x in r " F by A8, A16, A17, A18, FUNCT_2:38; ::_thesis: verum
end;
hence C c= r " F by TARSKI:def_3; ::_thesis: verum
end;
then A21: union { (Cl {a}) where a is Point of X : a in E } c= r " F by ZFMISC_1:76;
Cl E = union { (Cl {a}) where a is Point of X : a in E } by Th48;
hence r " F = Cl E by A21, A14, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TEX_2:71
for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
r " {a} = Cl {b} by Th70;
theorem Th72: :: TEX_2:72
for X being non empty almost_discrete TopSpace
for X0 being non empty discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
let X0 be non empty discrete SubSpace of X; ::_thesis: ex r being continuous Function of X,X0 st r is being_a_retraction
consider Z0 being non empty strict SubSpace of X such that
A1: X0 is SubSpace of Z0 and
A2: Z0 is maximal_discrete by Th61;
reconsider Z0 = Z0 as non empty strict maximal_discrete SubSpace of X by A2;
reconsider Z1 = Z0 as non empty TopSpace ;
reconsider Z1 = Z1 as non empty discrete TopSpace ;
reconsider X1 = X0 as non empty SubSpace of Z1 by A1;
consider g being continuous Function of Z1,X1 such that
A3: g is being_a_retraction by Th66;
reconsider g = g as continuous Function of Z0,X0 ;
consider h being continuous Function of X,Z0 such that
A4: h is being_a_retraction by Th68;
reconsider r = g * h as continuous Function of X,X0 ;
take r ; ::_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 A5: x in the carrier of X0 ; ::_thesis: r . x = x
the carrier of X1 c= the carrier of Z1 by BORSUK_1:1;
then reconsider y = x as Point of Z1 by A5;
g . y = y by A3, A5, BORSUK_1:def_16;
then g . (h . x) = x by A4, BORSUK_1:def_16;
hence r . x = x by FUNCT_2:15; ::_thesis: verum
end;
hence r is being_a_retraction by BORSUK_1:def_16; ::_thesis: verum
end;
theorem :: TEX_2:73
for X being non empty almost_discrete TopSpace
for X0 being non empty discrete SubSpace of X holds X0 is_a_retract_of X
proof
let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty discrete SubSpace of X holds X0 is_a_retract_of X
let X0 be non empty discrete 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 Th72;
hence X0 is_a_retract_of X by BORSUK_1:def_17; ::_thesis: verum
end;