:: TEX_3 semantic presentation
begin
theorem Th1: :: TEX_3:1
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( not A is empty iff B is proper )
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A,B constitute_a_decomposition holds
( not A is empty iff B is proper )
let A, B be Subset of X; ::_thesis: ( A,B constitute_a_decomposition implies ( not A is empty iff B is proper ) )
assume A1: A,B constitute_a_decomposition ; ::_thesis: ( not A is empty iff B is proper )
then A2: B = A ` by TSEP_2:3;
thus ( not A is empty implies B is proper ) ::_thesis: ( B is proper implies not A is empty )
proof
assume not A is empty ; ::_thesis: B is proper
then B <> the carrier of X by A2, TOPS_3:1;
hence B is proper by SUBSET_1:def_6; ::_thesis: verum
end;
assume A3: B is proper ; ::_thesis: not A is empty
A = B ` by A1, TSEP_2:3;
hence not A is empty by A3; ::_thesis: verum
end;
Lm1: for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A meets B
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A meets B
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & B is everywhere_dense implies A meets B )
assume ( A is everywhere_dense & B is everywhere_dense ) ; ::_thesis: A meets B
then A /\ B <> {} by TOPS_3:34, TOPS_3:44;
hence A meets B by XBOOLE_0:def_7; ::_thesis: verum
end;
Lm2: for X being non empty TopSpace
for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds
A meets B
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds
A meets B
let A, B be Subset of X; ::_thesis: ( ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) implies A meets B )
assume ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) ; ::_thesis: A meets B
then A /\ B <> {} by TOPS_3:17, TOPS_3:45;
hence A meets B by XBOOLE_0:def_7; ::_thesis: verum
end;
theorem Th2: :: TEX_3:2
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is dense iff B is boundary )
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is dense iff B is boundary )
let A, B be Subset of X; ::_thesis: ( A,B constitute_a_decomposition implies ( A is dense iff B is boundary ) )
assume A1: A,B constitute_a_decomposition ; ::_thesis: ( A is dense iff B is boundary )
then B = A ` by TSEP_2:3;
hence ( A is dense implies B is boundary ) by TOPS_3:18; ::_thesis: ( B is boundary implies A is dense )
assume A2: B is boundary ; ::_thesis: A is dense
A = B ` by A1, TSEP_2:3;
hence A is dense by A2, TOPS_1:def_4; ::_thesis: verum
end;
theorem :: TEX_3:3
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is boundary iff B is dense ) by Th2;
theorem Th4: :: TEX_3:4
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is everywhere_dense iff B is nowhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is everywhere_dense iff B is nowhere_dense )
let A, B be Subset of X; ::_thesis: ( A,B constitute_a_decomposition implies ( A is everywhere_dense iff B is nowhere_dense ) )
assume A1: A,B constitute_a_decomposition ; ::_thesis: ( A is everywhere_dense iff B is nowhere_dense )
then B = A ` by TSEP_2:3;
hence ( A is everywhere_dense implies B is nowhere_dense ) by TOPS_3:39; ::_thesis: ( B is nowhere_dense implies A is everywhere_dense )
assume A2: B is nowhere_dense ; ::_thesis: A is everywhere_dense
A = B ` by A1, TSEP_2:3;
hence A is everywhere_dense by A2, TOPS_3:40; ::_thesis: verum
end;
theorem :: TEX_3:5
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is nowhere_dense iff B is everywhere_dense ) by Th4;
theorem Th6: :: TEX_3:6
for X being non empty TopSpace
for Y1, Y2 being non empty SubSpace of X st Y1,Y2 constitute_a_decomposition holds
( Y1 is proper & Y2 is proper )
proof
let X be non empty TopSpace; ::_thesis: for Y1, Y2 being non empty SubSpace of X st Y1,Y2 constitute_a_decomposition holds
( Y1 is proper & Y2 is proper )
let Y1, Y2 be non empty SubSpace of X; ::_thesis: ( Y1,Y2 constitute_a_decomposition implies ( Y1 is proper & Y2 is proper ) )
reconsider A1 = the carrier of Y1, A2 = the carrier of Y2 as Subset of X by TSEP_1:1;
assume Y1,Y2 constitute_a_decomposition ; ::_thesis: ( Y1 is proper & Y2 is proper )
then A1,A2 constitute_a_decomposition by TSEP_2:def_2;
then ( A1 is proper & A2 is proper ) by Th1;
hence ( Y1 is proper & Y2 is proper ) by TEX_2:8; ::_thesis: verum
end;
theorem :: TEX_3:7
for X being non trivial TopSpace
for D being non empty proper Subset of X ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0
proof
let X be non trivial TopSpace; ::_thesis: for D being non empty proper Subset of X ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0
let D be non empty proper Subset of X; ::_thesis: ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0
consider Y0 being non empty strict SubSpace of X such that
A1: D = the carrier of Y0 by TSEP_1:10;
reconsider Y0 = Y0 as non empty strict proper SubSpace of X by A1, TEX_2:8;
take Y0 ; ::_thesis: D = the carrier of Y0
thus D = the carrier of Y0 by A1; ::_thesis: verum
end;
theorem Th8: :: TEX_3:8
for X being non trivial TopSpace
for Y1 being non empty proper SubSpace of X ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition
proof
let X be non trivial TopSpace; ::_thesis: for Y1 being non empty proper SubSpace of X ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition
let Y1 be non empty proper SubSpace of X; ::_thesis: ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition
reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1:1;
A1 is proper by TEX_2:8;
then consider Y2 being non empty strict SubSpace of X such that
A1: A1 ` = the carrier of Y2 by TSEP_1:10;
A2: for P, Q being Subset of X st P = the carrier of Y1 & Q = the carrier of Y2 holds
P,Q constitute_a_decomposition by A1, TSEP_2:5;
then Y1,Y2 constitute_a_decomposition by TSEP_2:def_2;
then reconsider Y2 = Y2 as non empty strict proper SubSpace of X by Th6;
take Y2 ; ::_thesis: Y1,Y2 constitute_a_decomposition
thus Y1,Y2 constitute_a_decomposition by A2, TSEP_2:def_2; ::_thesis: verum
end;
begin
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT is dense means :Def1: :: TEX_3:def 1
for A being Subset of X st A = the carrier of IT holds
A is dense ;
end;
:: deftheorem Def1 defines dense TEX_3:def_1_:_
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is dense iff for A being Subset of X st A = the carrier of IT holds
A is dense );
theorem Th9: :: TEX_3:9
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is dense iff A is dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is dense iff A is dense )
let X0 be SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is dense iff A is dense )
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies ( X0 is dense iff A is dense ) )
assume A1: A = the carrier of X0 ; ::_thesis: ( X0 is dense iff A is dense )
hence ( X0 is dense implies A is dense ) by Def1; ::_thesis: ( A is dense implies X0 is dense )
assume A is dense ; ::_thesis: X0 is dense
then for B being Subset of X st B = the carrier of X0 holds
B is dense by A1;
hence X0 is dense by Def1; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster closed dense -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is closed holds
not b1 is proper
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is dense & X0 is closed implies not X0 is proper )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume A1: ( X0 is dense & X0 is closed ) ; ::_thesis: not X0 is proper
then A is closed by TSEP_1:11;
then A2: Cl A = A by PRE_TOPC:22;
A is dense by A1, Th9;
then Cl A = the carrier of X by TOPS_3:def_2;
then not A is proper by A2, SUBSET_1:def_6;
hence not X0 is proper by TEX_2:8; ::_thesis: verum
end;
cluster proper dense -> non closed for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is proper holds
not b1 is closed ;
cluster closed proper -> non dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper & b1 is closed holds
not b1 is dense ;
end;
registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is strict & not b1 is empty )
proof
X is SubSpace of X by TSEP_1:2;
then reconsider A0 = the carrier of X as Subset of X by TSEP_1:1;
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
take X0 ; ::_thesis: ( X0 is dense & X0 is strict & not X0 is empty )
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is dense )
assume A = the carrier of X0 ; ::_thesis: A is dense
then A = [#] X by A1;
hence A is dense ; ::_thesis: verum
end;
hence ( X0 is dense & X0 is strict & not X0 is empty ) by Def1; ::_thesis: verum
end;
end;
theorem Th10: :: TEX_3:10
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is dense holds
ex X0 being non empty strict dense 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 dense holds
ex X0 being non empty strict dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is dense implies ex X0 being non empty strict dense 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 dense ; ::_thesis: ex X0 being non empty strict dense SubSpace of X st A0 = the carrier of X0
then reconsider Y0 = X0 as non empty strict dense SubSpace of X by A1, Th9;
take Y0 ; ::_thesis: A0 = the carrier of Y0
thus A0 = the carrier of Y0 by A1; ::_thesis: verum
end;
theorem :: TEX_3:11
for X being non empty TopSpace
for X0 being non empty dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is dense iff A is dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is dense iff A is dense )
let X0 be non empty dense SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A = B holds
( B is dense iff A is dense )
let A be Subset of X; ::_thesis: for B being Subset of X0 st A = B holds
( B is dense iff A is dense )
let B be Subset of X0; ::_thesis: ( A = B implies ( B is dense iff A is dense ) )
assume A1: A = B ; ::_thesis: ( B is dense iff A is dense )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
C is dense by Th9;
hence ( B is dense iff A is dense ) by A1, TOPS_3:60; ::_thesis: verum
end;
theorem :: TEX_3:12
for X being non empty TopSpace
for X1 being dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is dense
proof
let X be non empty TopSpace; ::_thesis: for X1 being dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is dense
let X1 be dense SubSpace of X; ::_thesis: for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is dense
let X2 be SubSpace of X; ::_thesis: ( X1 is SubSpace of X2 implies X2 is dense )
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
assume X1 is SubSpace of X2 ; ::_thesis: X2 is dense
then A1: the carrier of X1 c= the carrier of X2 by TSEP_1:4;
C is dense by Def1;
then for A being Subset of X st A = the carrier of X2 holds
A is dense by A1, TOPS_1:44;
hence X2 is dense by Def1; ::_thesis: verum
end;
theorem :: TEX_3:13
for X being non empty TopSpace
for X1 being non empty dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is dense SubSpace of X2
proof
let X be non empty TopSpace; ::_thesis: for X1 being non empty dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is dense SubSpace of X2
let X1 be non empty dense SubSpace of X; ::_thesis: for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is dense SubSpace of X2
let X2 be non empty SubSpace of X; ::_thesis: ( X1 is SubSpace of X2 implies X1 is dense SubSpace of X2 )
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
C is dense by Def1;
then A1: for A being Subset of X2 st A = the carrier of X1 holds
A is dense by TOPS_3:59;
assume X1 is SubSpace of X2 ; ::_thesis: X1 is dense SubSpace of X2
hence X1 is dense SubSpace of X2 by A1, Def1; ::_thesis: verum
end;
theorem :: TEX_3:14
for X being non empty TopSpace
for X1 being non empty dense SubSpace of X
for X2 being non empty dense SubSpace of X1 holds X2 is non empty dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1 being non empty dense SubSpace of X
for X2 being non empty dense SubSpace of X1 holds X2 is non empty dense SubSpace of X
let X1 be non empty dense SubSpace of X; ::_thesis: for X2 being non empty dense SubSpace of X1 holds X2 is non empty dense SubSpace of X
let X2 be non empty dense SubSpace of X1; ::_thesis: X2 is non empty dense SubSpace of X
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X2_holds_
A_is_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X2 implies A is dense )
assume A1: A = the carrier of X2 ; ::_thesis: A is dense
then reconsider B = A as Subset of X1 by BORSUK_1:1;
A2: C is dense by Def1;
B is dense by A1, Def1;
hence A is dense by A2, TOPS_3:60; ::_thesis: verum
end;
hence X2 is non empty dense SubSpace of X by Def1, TSEP_1:7; ::_thesis: verum
end;
theorem :: TEX_3:15
for X, Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X )
proof
let X be non empty TopSpace; ::_thesis: for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X )
let X1, X2 be non empty TopSpace; ::_thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is dense SubSpace of X iff X2 is dense SubSpace of X ) )
assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; ::_thesis: ( X1 is dense SubSpace of X iff X2 is dense SubSpace of X )
thus ( X1 is dense SubSpace of X implies X2 is dense SubSpace of X ) ::_thesis: ( X2 is dense SubSpace of X implies X1 is dense SubSpace of X )
proof
assume A2: X1 is dense SubSpace of X ; ::_thesis: X2 is dense SubSpace of X
then reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1:7;
for A2 being Subset of X st A2 = the carrier of Y2 holds
A2 is dense by A1, A2, Def1;
hence X2 is dense SubSpace of X by Def1; ::_thesis: verum
end;
assume A3: X2 is dense SubSpace of X ; ::_thesis: X1 is dense SubSpace of X
then reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1:7;
for A1 being Subset of X st A1 = the carrier of Y1 holds
A1 is dense by A1, A3, Def1;
hence X1 is dense SubSpace of X by Def1; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT is everywhere_dense means :Def2: :: TEX_3:def 2
for A being Subset of X st A = the carrier of IT holds
A is everywhere_dense ;
end;
:: deftheorem Def2 defines everywhere_dense TEX_3:def_2_:_
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is everywhere_dense iff for A being Subset of X st A = the carrier of IT holds
A is everywhere_dense );
theorem Th16: :: TEX_3:16
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense )
let X0 be SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense )
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies ( X0 is everywhere_dense iff A is everywhere_dense ) )
assume A1: A = the carrier of X0 ; ::_thesis: ( X0 is everywhere_dense iff A is everywhere_dense )
hence ( X0 is everywhere_dense implies A is everywhere_dense ) by Def2; ::_thesis: ( A is everywhere_dense implies X0 is everywhere_dense )
assume A is everywhere_dense ; ::_thesis: X0 is everywhere_dense
then for B being Subset of X st B = the carrier of X0 holds
B is everywhere_dense by A1;
hence X0 is everywhere_dense by Def2; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster everywhere_dense -> dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is everywhere_dense holds
b1 is dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is everywhere_dense implies X0 is dense )
assume A1: X0 is everywhere_dense ; ::_thesis: X0 is dense
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is dense )
assume A = the carrier of X0 ; ::_thesis: A is dense
then A is everywhere_dense by A1, Def2;
hence A is dense by TOPS_3:33; ::_thesis: verum
end;
hence X0 is dense by Def1; ::_thesis: verum
end;
cluster non dense -> non everywhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is dense holds
not b1 is everywhere_dense ;
cluster non proper -> everywhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is proper holds
b1 is everywhere_dense
proof
let X0 be SubSpace of X; ::_thesis: ( not X0 is proper implies X0 is everywhere_dense )
assume A2: not X0 is proper ; ::_thesis: X0 is everywhere_dense
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_everywhere_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is everywhere_dense )
assume A = the carrier of X0 ; ::_thesis: A is everywhere_dense
then not A is proper by A2, TEX_2:8;
then A = [#] X by SUBSET_1:def_6;
hence A is everywhere_dense by TOPS_3:31; ::_thesis: verum
end;
hence X0 is everywhere_dense by Def2; ::_thesis: verum
end;
cluster non everywhere_dense -> proper for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is everywhere_dense holds
b1 is proper ;
end;
registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like everywhere_dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is everywhere_dense & b1 is strict & not b1 is empty )
proof
X is SubSpace of X by TSEP_1:2;
then reconsider A0 = the carrier of X as Subset of X by TSEP_1:1;
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
take X0 ; ::_thesis: ( X0 is everywhere_dense & X0 is strict & not X0 is empty )
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_everywhere_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is everywhere_dense )
assume A = the carrier of X0 ; ::_thesis: A is everywhere_dense
then A = [#] X by A1;
hence A is everywhere_dense by TOPS_3:31; ::_thesis: verum
end;
hence ( X0 is everywhere_dense & X0 is strict & not X0 is empty ) by Def2; ::_thesis: verum
end;
end;
theorem Th17: :: TEX_3:17
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is everywhere_dense holds
ex X0 being non empty strict everywhere_dense 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 everywhere_dense holds
ex X0 being non empty strict everywhere_dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is everywhere_dense implies ex X0 being non empty strict everywhere_dense 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 everywhere_dense ; ::_thesis: ex X0 being non empty strict everywhere_dense SubSpace of X st A0 = the carrier of X0
then reconsider Y0 = X0 as non empty strict everywhere_dense SubSpace of X by A1, Th16;
take Y0 ; ::_thesis: A0 = the carrier of Y0
thus A0 = the carrier of Y0 by A1; ::_thesis: verum
end;
theorem :: TEX_3:18
for X being non empty TopSpace
for X0 being non empty everywhere_dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is everywhere_dense iff A is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty everywhere_dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is everywhere_dense iff A is everywhere_dense )
let X0 be non empty everywhere_dense SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A = B holds
( B is everywhere_dense iff A is everywhere_dense )
let A be Subset of X; ::_thesis: for B being Subset of X0 st A = B holds
( B is everywhere_dense iff A is everywhere_dense )
let B be Subset of X0; ::_thesis: ( A = B implies ( B is everywhere_dense iff A is everywhere_dense ) )
assume A1: A = B ; ::_thesis: ( B is everywhere_dense iff A is everywhere_dense )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
C is everywhere_dense by Th16;
hence ( B is everywhere_dense iff A is everywhere_dense ) by A1, TOPS_3:64; ::_thesis: verum
end;
theorem :: TEX_3:19
for X being non empty TopSpace
for X1 being everywhere_dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X1 being everywhere_dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is everywhere_dense
let X1 be everywhere_dense SubSpace of X; ::_thesis: for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is everywhere_dense
let X2 be SubSpace of X; ::_thesis: ( X1 is SubSpace of X2 implies X2 is everywhere_dense )
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
assume X1 is SubSpace of X2 ; ::_thesis: X2 is everywhere_dense
then A1: the carrier of X1 c= the carrier of X2 by TSEP_1:4;
C is everywhere_dense by Def2;
then for A being Subset of X st A = the carrier of X2 holds
A is everywhere_dense by A1, TOPS_3:38;
hence X2 is everywhere_dense by Def2; ::_thesis: verum
end;
theorem :: TEX_3:20
for X being non empty TopSpace
for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is everywhere_dense SubSpace of X2
proof
let X be non empty TopSpace; ::_thesis: for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is everywhere_dense SubSpace of X2
let X1 be non empty everywhere_dense SubSpace of X; ::_thesis: for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is everywhere_dense SubSpace of X2
let X2 be non empty SubSpace of X; ::_thesis: ( X1 is SubSpace of X2 implies X1 is everywhere_dense SubSpace of X2 )
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
C is everywhere_dense by Def2;
then A1: for A being Subset of X2 st A = the carrier of X1 holds
A is everywhere_dense by TOPS_3:61;
assume X1 is SubSpace of X2 ; ::_thesis: X1 is everywhere_dense SubSpace of X2
hence X1 is everywhere_dense SubSpace of X2 by A1, Def2; ::_thesis: verum
end;
theorem :: TEX_3:21
for X being non empty TopSpace
for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X
let X1 be non empty everywhere_dense SubSpace of X; ::_thesis: for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X
let X2 be non empty everywhere_dense SubSpace of X1; ::_thesis: X2 is everywhere_dense SubSpace of X
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X2_holds_
A_is_everywhere_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X2 implies A is everywhere_dense )
assume A1: A = the carrier of X2 ; ::_thesis: A is everywhere_dense
then reconsider B = A as Subset of X1 by BORSUK_1:1;
A2: C is everywhere_dense by Def2;
B is everywhere_dense by A1, Def2;
hence A is everywhere_dense by A2, TOPS_3:64; ::_thesis: verum
end;
hence X2 is everywhere_dense SubSpace of X by Def2, TSEP_1:7; ::_thesis: verum
end;
theorem :: TEX_3:22
for X, Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X )
proof
let X be non empty TopSpace; ::_thesis: for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X )
let X1, X2 be non empty TopSpace; ::_thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is everywhere_dense SubSpace of X iff X2 is everywhere_dense SubSpace of X ) )
assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; ::_thesis: ( X1 is everywhere_dense SubSpace of X iff X2 is everywhere_dense SubSpace of X )
thus ( X1 is everywhere_dense SubSpace of X implies X2 is everywhere_dense SubSpace of X ) ::_thesis: ( X2 is everywhere_dense SubSpace of X implies X1 is everywhere_dense SubSpace of X )
proof
assume A2: X1 is everywhere_dense SubSpace of X ; ::_thesis: X2 is everywhere_dense SubSpace of X
then reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1:7;
for A2 being Subset of X st A2 = the carrier of Y2 holds
A2 is everywhere_dense by A1, A2, Def2;
hence X2 is everywhere_dense SubSpace of X by Def2; ::_thesis: verum
end;
assume A3: X2 is everywhere_dense SubSpace of X ; ::_thesis: X1 is everywhere_dense SubSpace of X
then reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1:7;
for A1 being Subset of X st A1 = the carrier of Y1 holds
A1 is everywhere_dense by A1, A3, Def2;
hence X1 is everywhere_dense SubSpace of X by Def2; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster open dense -> everywhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is open holds
b1 is everywhere_dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is dense & X0 is open implies X0 is everywhere_dense )
assume A1: ( X0 is dense & X0 is open ) ; ::_thesis: X0 is everywhere_dense
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_everywhere_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is everywhere_dense )
assume A = the carrier of X0 ; ::_thesis: A is everywhere_dense
then ( A is dense & A is open ) by A1, Th9, TSEP_1:16;
hence A is everywhere_dense by TOPS_3:36; ::_thesis: verum
end;
hence X0 is everywhere_dense by Def2; ::_thesis: verum
end;
cluster dense non everywhere_dense -> non open for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & not b1 is everywhere_dense holds
not b1 is open ;
cluster open non everywhere_dense -> non dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is open & not b1 is everywhere_dense holds
not b1 is dense ;
end;
registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like open dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is open & b1 is strict & not b1 is empty )
proof
X is SubSpace of X by TSEP_1:2;
then reconsider A0 = the carrier of X as Subset of X by TSEP_1:1;
A0 = [#] X ;
then A0 is dense ;
then consider X0 being non empty strict dense SubSpace of X such that
A1: A0 = the carrier of X0 by Th10;
take X0 ; ::_thesis: ( X0 is dense & X0 is open & X0 is strict & not X0 is empty )
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;
hence A is open ; ::_thesis: verum
end;
hence ( X0 is dense & X0 is open & X0 is strict & not X0 is empty ) by TSEP_1:def_1; ::_thesis: verum
end;
end;
theorem Th23: :: TEX_3:23
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is dense & A0 is open holds
ex X0 being non empty strict open dense 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 dense & A0 is open holds
ex X0 being non empty strict open dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is dense & A0 is open implies ex X0 being non empty strict open dense 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 dense & A0 is open ) ; ::_thesis: ex X0 being non empty strict open dense SubSpace of X st A0 = the carrier of X0
then reconsider Y0 = X0 as non empty strict open dense SubSpace of X by A1, Th9, TSEP_1:16;
take Y0 ; ::_thesis: A0 = the carrier of Y0
thus A0 = the carrier of Y0 by A1; ::_thesis: verum
end;
theorem :: TEX_3:24
for X being non empty TopSpace
for X0 being SubSpace of X holds
( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X holds
( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )
let X0 be SubSpace of X; ::_thesis: ( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus ( X0 is everywhere_dense implies ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 ) ::_thesis: ( ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 implies X0 is everywhere_dense )
proof
assume X0 is everywhere_dense ; ::_thesis: ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0
then A is everywhere_dense by Def2;
then consider C being Subset of X such that
A1: C c= A and
A2: C is open and
A3: C is dense by TOPS_3:41;
not C is empty by A3, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A4: C = the carrier of X1 by A2, A3, Th23;
take X1 ; ::_thesis: X1 is SubSpace of X0
thus X1 is SubSpace of X0 by A1, A4, TSEP_1:4; ::_thesis: verum
end;
given X1 being strict open dense SubSpace of X such that A5: X1 is SubSpace of X0 ; ::_thesis: X0 is everywhere_dense
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;
now__::_thesis:_ex_C_being_Subset_of_X_st_
(_C_c=_A_&_C_is_open_&_C_is_dense_)
take C = C; ::_thesis: ( C c= A & C is open & C is dense )
thus ( C c= A & C is open & C is dense ) by A5, Def1, TSEP_1:4, TSEP_1:16; ::_thesis: verum
end;
then for A being Subset of X st A = the carrier of X0 holds
A is everywhere_dense by TOPS_3:41;
hence X0 is everywhere_dense by Def2; ::_thesis: verum
end;
theorem :: TEX_3:25
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is dense or X2 is dense ) holds
X1 union X2 is dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( X1 is dense or X2 is dense ) holds
X1 union X2 is dense SubSpace of X
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( X1 is dense or X2 is dense ) implies X1 union X2 is dense SubSpace of X )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of (X1 union X2) as Subset of X by TSEP_1:1;
assume ( X1 is dense or X2 is dense ) ; ::_thesis: X1 union X2 is dense SubSpace of X
then ( A1 is dense or A2 is dense ) by Def1;
then A1 \/ A2 is dense by TOPS_3:21;
then A is dense by TSEP_1:def_2;
hence X1 union X2 is dense SubSpace of X by Th9; ::_thesis: verum
end;
theorem :: TEX_3:26
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is everywhere_dense or X2 is everywhere_dense ) holds
X1 union X2 is everywhere_dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( X1 is everywhere_dense or X2 is everywhere_dense ) holds
X1 union X2 is everywhere_dense SubSpace of X
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( X1 is everywhere_dense or X2 is everywhere_dense ) implies X1 union X2 is everywhere_dense SubSpace of X )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of (X1 union X2) as Subset of X by TSEP_1:1;
assume ( X1 is everywhere_dense or X2 is everywhere_dense ) ; ::_thesis: X1 union X2 is everywhere_dense SubSpace of X
then ( A1 is everywhere_dense or A2 is everywhere_dense ) by Def2;
then A1 \/ A2 is everywhere_dense by TOPS_3:43;
then A is everywhere_dense by TSEP_1:def_2;
hence X1 union X2 is everywhere_dense SubSpace of X by Th16; ::_thesis: verum
end;
theorem :: TEX_3:27
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 is everywhere_dense & X2 is everywhere_dense holds
X1 meet X2 is everywhere_dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st X1 is everywhere_dense & X2 is everywhere_dense holds
X1 meet X2 is everywhere_dense SubSpace of X
let X1, X2 be non empty SubSpace of X; ::_thesis: ( X1 is everywhere_dense & X2 is everywhere_dense implies X1 meet X2 is everywhere_dense SubSpace of X )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of (X1 meet X2) as Subset of X by TSEP_1:1;
assume ( X1 is everywhere_dense & X2 is everywhere_dense ) ; ::_thesis: X1 meet X2 is everywhere_dense SubSpace of X
then A1: ( A1 is everywhere_dense & A2 is everywhere_dense ) by Th16;
then A1 meets A2 by Lm1;
then A2: X1 meets X2 by TSEP_1:def_3;
A1 /\ A2 is everywhere_dense by A1, TOPS_3:44;
then A is everywhere_dense by A2, TSEP_1:def_4;
hence X1 meet X2 is everywhere_dense SubSpace of X by Th16; ::_thesis: verum
end;
theorem :: TEX_3:28
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) holds
X1 meet X2 is dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) holds
X1 meet X2 is dense SubSpace of X
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) implies X1 meet X2 is dense SubSpace of X )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of (X1 meet X2) as Subset of X by TSEP_1:1;
assume ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) ; ::_thesis: X1 meet X2 is dense SubSpace of X
then A1: ( ( A1 is everywhere_dense & A2 is dense ) or ( A1 is dense & A2 is everywhere_dense ) ) by Th9, Th16;
then A1 meets A2 by Lm2;
then A2: X1 meets X2 by TSEP_1:def_3;
A1 /\ A2 is dense by A1, TOPS_3:45;
then A is dense by A2, TSEP_1:def_4;
hence X1 meet X2 is dense SubSpace of X by Th9; ::_thesis: verum
end;
begin
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT is boundary means :Def3: :: TEX_3:def 3
for A being Subset of X st A = the carrier of IT holds
A is boundary ;
end;
:: deftheorem Def3 defines boundary TEX_3:def_3_:_
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is boundary iff for A being Subset of X st A = the carrier of IT holds
A is boundary );
theorem Th29: :: TEX_3:29
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is boundary iff A is boundary )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is boundary iff A is boundary )
let X0 be SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is boundary iff A is boundary )
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies ( X0 is boundary iff A is boundary ) )
assume A1: A = the carrier of X0 ; ::_thesis: ( X0 is boundary iff A is boundary )
hence ( X0 is boundary implies A is boundary ) by Def3; ::_thesis: ( A is boundary implies X0 is boundary )
assume A is boundary ; ::_thesis: X0 is boundary
then for B being Subset of X st B = the carrier of X0 holds
B is boundary by A1;
hence X0 is boundary by Def3; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster non empty open -> non empty non boundary for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is open holds
not b1 is boundary
proof
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is open implies not X0 is boundary )
assume A1: X0 is open ; ::_thesis: not X0 is boundary
now__::_thesis:_not_X0_is_boundary
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is boundary ; ::_thesis: contradiction
then A is boundary by Def3;
then A2: Int A = {} ;
A is open by A1, TSEP_1:16;
hence contradiction by A2, TOPS_1:23; ::_thesis: verum
end;
hence not X0 is boundary ; ::_thesis: verum
end;
cluster non empty boundary -> non empty non open for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is boundary holds
not b1 is open ;
cluster everywhere_dense -> non boundary for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is everywhere_dense holds
not b1 is boundary
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is everywhere_dense implies not X0 is boundary )
assume A3: X0 is everywhere_dense ; ::_thesis: not X0 is boundary
now__::_thesis:_not_X0_is_boundary
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A is everywhere_dense by A3, Def2;
then A4: not A is boundary by TOPS_3:37;
assume X0 is boundary ; ::_thesis: contradiction
hence contradiction by A4, Def3; ::_thesis: verum
end;
hence not X0 is boundary ; ::_thesis: verum
end;
cluster boundary -> non everywhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is boundary holds
not b1 is everywhere_dense ;
end;
theorem Th30: :: TEX_3:30
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
let A0 be non empty Subset of X; ::_thesis: ( A0 is boundary implies ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 ) )
assume A1: A0 is boundary ; ::_thesis: ex X0 being strict SubSpace of X st
( X0 is boundary & 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 boundary & A0 = the carrier of X0 )
thus ( X0 is boundary & A0 = the carrier of X0 ) by A1, A2, Th29; ::_thesis: verum
end;
theorem Th31: :: TEX_3:31
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is dense iff X2 is boundary )
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is dense iff X2 is boundary )
let X1, X2 be SubSpace of X; ::_thesis: ( X1,X2 constitute_a_decomposition implies ( X1 is dense iff X2 is boundary ) )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume A1: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: ( X1 is dense iff X2 is boundary )
thus ( X1 is dense implies X2 is boundary ) ::_thesis: ( X2 is boundary implies X1 is dense )
proof
assume A2: for A1 being Subset of X st A1 = the carrier of X1 holds
A1 is dense ; :: according to TEX_3:def_1 ::_thesis: X2 is boundary
now__::_thesis:_for_A2_being_Subset_of_X_st_A2_=_the_carrier_of_X2_holds_
A2_is_boundary
let A2 be Subset of X; ::_thesis: ( A2 = the carrier of X2 implies A2 is boundary )
assume A2 = the carrier of X2 ; ::_thesis: A2 is boundary
then A3: A1,A2 constitute_a_decomposition by A1;
A1 is dense by A2;
hence A2 is boundary by A3, Th2; ::_thesis: verum
end;
hence X2 is boundary by Def3; ::_thesis: verum
end;
assume A4: for A2 being Subset of X st A2 = the carrier of X2 holds
A2 is boundary ; :: according to TEX_3:def_3 ::_thesis: X1 is dense
now__::_thesis:_for_A1_being_Subset_of_X_st_A1_=_the_carrier_of_X1_holds_
A1_is_dense
let A1 be Subset of X; ::_thesis: ( A1 = the carrier of X1 implies A1 is dense )
assume A1 = the carrier of X1 ; ::_thesis: A1 is dense
then A5: A1,A2 constitute_a_decomposition by A1;
A2 is boundary by A4;
hence A1 is dense by A5, Th2; ::_thesis: verum
end;
hence X1 is dense by Def1; ::_thesis: verum
end;
theorem :: TEX_3:32
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is boundary iff X2 is dense ) by Th31;
theorem Th33: :: TEX_3:33
for X being non empty TopSpace
for X0 being SubSpace of X st X0 is boundary holds
for A being Subset of X st A c= the carrier of X0 holds
A is boundary
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X st X0 is boundary holds
for A being Subset of X st A c= the carrier of X0 holds
A is boundary
let X0 be SubSpace of X; ::_thesis: ( X0 is boundary implies for A being Subset of X st A c= the carrier of X0 holds
A is boundary )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is boundary ; ::_thesis: for A being Subset of X st A c= the carrier of X0 holds
A is boundary
then A1: C is boundary by Def3;
let A be Subset of X; ::_thesis: ( A c= the carrier of X0 implies A is boundary )
assume A c= the carrier of X0 ; ::_thesis: A is boundary
hence A is boundary by A1, TOPS_3:11; ::_thesis: verum
end;
theorem Th34: :: TEX_3:34
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1 is boundary & X2 is SubSpace of X1 holds
X2 is boundary
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being SubSpace of X st X1 is boundary & X2 is SubSpace of X1 holds
X2 is boundary
let X1, X2 be SubSpace of X; ::_thesis: ( X1 is boundary & X2 is SubSpace of X1 implies X2 is boundary )
assume A1: X1 is boundary ; ::_thesis: ( not X2 is SubSpace of X1 or X2 is boundary )
assume X2 is SubSpace of X1 ; ::_thesis: X2 is boundary
then the carrier of X2 c= the carrier of X1 by TSEP_1:4;
then for A being Subset of X st A = the carrier of X2 holds
A is boundary by A1, Th33;
hence X2 is boundary by Def3; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT is nowhere_dense means :Def4: :: TEX_3:def 4
for A being Subset of X st A = the carrier of IT holds
A is nowhere_dense ;
end;
:: deftheorem Def4 defines nowhere_dense TEX_3:def_4_:_
for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is nowhere_dense iff for A being Subset of X st A = the carrier of IT holds
A is nowhere_dense );
theorem Th35: :: TEX_3:35
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is nowhere_dense iff A is nowhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is nowhere_dense iff A is nowhere_dense )
let X0 be SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is nowhere_dense iff A is nowhere_dense )
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies ( X0 is nowhere_dense iff A is nowhere_dense ) )
assume A1: A = the carrier of X0 ; ::_thesis: ( X0 is nowhere_dense iff A is nowhere_dense )
hence ( X0 is nowhere_dense implies A is nowhere_dense ) by Def4; ::_thesis: ( A is nowhere_dense implies X0 is nowhere_dense )
assume A is nowhere_dense ; ::_thesis: X0 is nowhere_dense
then for B being Subset of X st B = the carrier of X0 holds
B is nowhere_dense by A1;
hence X0 is nowhere_dense by Def4; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster nowhere_dense -> boundary for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is nowhere_dense holds
b1 is boundary
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is nowhere_dense implies X0 is boundary )
assume A1: X0 is nowhere_dense ; ::_thesis: X0 is boundary
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_boundary
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is boundary )
assume A = the carrier of X0 ; ::_thesis: A is boundary
then A is nowhere_dense by A1, Def4;
hence A is boundary ; ::_thesis: verum
end;
hence X0 is boundary by Def3; ::_thesis: verum
end;
cluster non boundary -> non nowhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st not b1 is boundary holds
not b1 is nowhere_dense ;
cluster nowhere_dense -> non dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is nowhere_dense holds
not b1 is dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is nowhere_dense implies not X0 is dense )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is nowhere_dense ; ::_thesis: not X0 is dense
then A is nowhere_dense by Def4;
then A2: not A is dense by TOPS_3:25;
assume X0 is dense ; ::_thesis: contradiction
hence contradiction by A2, Def1; ::_thesis: verum
end;
cluster dense -> non nowhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense holds
not b1 is nowhere_dense ;
end;
theorem :: TEX_3:36
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being strict SubSpace of X st
( X0 is nowhere_dense & A0 = the carrier of X0 )
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being strict SubSpace of X st
( X0 is nowhere_dense & A0 = the carrier of X0 )
let A0 be non empty Subset of X; ::_thesis: ( A0 is nowhere_dense implies ex X0 being strict SubSpace of X st
( X0 is nowhere_dense & A0 = the carrier of X0 ) )
assume A1: A0 is nowhere_dense ; ::_thesis: ex X0 being strict SubSpace of X st
( X0 is nowhere_dense & 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 nowhere_dense & A0 = the carrier of X0 )
thus ( X0 is nowhere_dense & A0 = the carrier of X0 ) by A1, A2, Th35; ::_thesis: verum
end;
theorem Th37: :: TEX_3:37
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is everywhere_dense iff X2 is nowhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is everywhere_dense iff X2 is nowhere_dense )
let X1, X2 be SubSpace of X; ::_thesis: ( X1,X2 constitute_a_decomposition implies ( X1 is everywhere_dense iff X2 is nowhere_dense ) )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume A1: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: ( X1 is everywhere_dense iff X2 is nowhere_dense )
thus ( X1 is everywhere_dense implies X2 is nowhere_dense ) ::_thesis: ( X2 is nowhere_dense implies X1 is everywhere_dense )
proof
assume A2: for A1 being Subset of X st A1 = the carrier of X1 holds
A1 is everywhere_dense ; :: according to TEX_3:def_2 ::_thesis: X2 is nowhere_dense
now__::_thesis:_for_A2_being_Subset_of_X_st_A2_=_the_carrier_of_X2_holds_
A2_is_nowhere_dense
let A2 be Subset of X; ::_thesis: ( A2 = the carrier of X2 implies A2 is nowhere_dense )
assume A2 = the carrier of X2 ; ::_thesis: A2 is nowhere_dense
then A3: A1,A2 constitute_a_decomposition by A1;
A1 is everywhere_dense by A2;
hence A2 is nowhere_dense by A3, Th4; ::_thesis: verum
end;
hence X2 is nowhere_dense by Def4; ::_thesis: verum
end;
assume A4: for A2 being Subset of X st A2 = the carrier of X2 holds
A2 is nowhere_dense ; :: according to TEX_3:def_4 ::_thesis: X1 is everywhere_dense
now__::_thesis:_for_A1_being_Subset_of_X_st_A1_=_the_carrier_of_X1_holds_
A1_is_everywhere_dense
let A1 be Subset of X; ::_thesis: ( A1 = the carrier of X1 implies A1 is everywhere_dense )
assume A1 = the carrier of X1 ; ::_thesis: A1 is everywhere_dense
then A5: A1,A2 constitute_a_decomposition by A1;
A2 is nowhere_dense by A4;
hence A1 is everywhere_dense by A5, Th4; ::_thesis: verum
end;
hence X1 is everywhere_dense by Def2; ::_thesis: verum
end;
theorem :: TEX_3:38
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is nowhere_dense iff X2 is everywhere_dense ) by Th37;
theorem Th39: :: TEX_3:39
for X being non empty TopSpace
for X0 being SubSpace of X st X0 is nowhere_dense holds
for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X st X0 is nowhere_dense holds
for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense
let X0 be SubSpace of X; ::_thesis: ( X0 is nowhere_dense implies for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is nowhere_dense ; ::_thesis: for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense
then A1: C is nowhere_dense by Def4;
let A be Subset of X; ::_thesis: ( A c= the carrier of X0 implies A is nowhere_dense )
assume A c= the carrier of X0 ; ::_thesis: A is nowhere_dense
hence A is nowhere_dense by A1, TOPS_3:26; ::_thesis: verum
end;
theorem Th40: :: TEX_3:40
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1 is nowhere_dense & X2 is SubSpace of X1 holds
X2 is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being SubSpace of X st X1 is nowhere_dense & X2 is SubSpace of X1 holds
X2 is nowhere_dense
let X1, X2 be SubSpace of X; ::_thesis: ( X1 is nowhere_dense & X2 is SubSpace of X1 implies X2 is nowhere_dense )
assume A1: X1 is nowhere_dense ; ::_thesis: ( not X2 is SubSpace of X1 or X2 is nowhere_dense )
assume X2 is SubSpace of X1 ; ::_thesis: X2 is nowhere_dense
then the carrier of X2 c= the carrier of X1 by TSEP_1:4;
then for A being Subset of X st A = the carrier of X2 holds
A is nowhere_dense by A1, Th39;
hence X2 is nowhere_dense by Def4; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster closed boundary -> nowhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is boundary & b1 is closed holds
b1 is nowhere_dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is boundary & X0 is closed implies X0 is nowhere_dense )
assume A1: ( X0 is boundary & X0 is closed ) ; ::_thesis: X0 is nowhere_dense
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_nowhere_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is nowhere_dense )
assume A = the carrier of X0 ; ::_thesis: A is nowhere_dense
then ( A is boundary & A is closed ) by A1, Th29, TSEP_1:11;
hence A is nowhere_dense ; ::_thesis: verum
end;
hence X0 is nowhere_dense by Def4; ::_thesis: verum
end;
cluster boundary non nowhere_dense -> non closed for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is boundary & not b1 is nowhere_dense holds
not b1 is closed ;
cluster closed non nowhere_dense -> non boundary for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is closed & not b1 is nowhere_dense holds
not b1 is boundary ;
end;
theorem Th41: :: TEX_3:41
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
let A0 be non empty Subset of X; ::_thesis: ( A0 is boundary & A0 is closed implies ex X0 being non empty strict closed SubSpace of X st
( X0 is boundary & 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 A2: ( A0 is boundary & A0 is closed ) ; ::_thesis: ex X0 being non empty strict closed SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
then reconsider Y0 = X0 as non empty strict closed SubSpace of X by A1, TSEP_1:11;
take Y0 ; ::_thesis: ( Y0 is boundary & A0 = the carrier of Y0 )
thus ( Y0 is boundary & A0 = the carrier of Y0 ) by A2, A1, Th29; ::_thesis: verum
end;
theorem :: TEX_3:42
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) )
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus ( X0 is nowhere_dense implies ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) ) ::_thesis: ( ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) implies X0 is nowhere_dense )
proof
assume X0 is nowhere_dense ; ::_thesis: ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 )
then A is nowhere_dense by Def4;
then consider C being Subset of X such that
A1: A c= C and
A2: ( C is closed & C is boundary ) by TOPS_3:27;
not C is empty by A1, XBOOLE_1:3;
then consider X1 being non empty strict closed SubSpace of X such that
A3: ( X1 is boundary & C = the carrier of X1 ) by A2, Th41;
take X1 ; ::_thesis: ( X1 is boundary & X0 is SubSpace of X1 )
thus ( X1 is boundary & X0 is SubSpace of X1 ) by A1, A3, TSEP_1:4; ::_thesis: verum
end;
given X1 being non empty strict closed SubSpace of X such that A4: ( X1 is boundary & X0 is SubSpace of X1 ) ; ::_thesis: X0 is nowhere_dense
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;
now__::_thesis:_ex_C_being_Subset_of_X_st_
(_A_c=_C_&_C_is_boundary_&_C_is_closed_)
take C = C; ::_thesis: ( A c= C & C is boundary & C is closed )
thus ( A c= C & C is boundary & C is closed ) by A4, Def3, TSEP_1:4, TSEP_1:11; ::_thesis: verum
end;
then for A being Subset of X st A = the carrier of X0 holds
A is nowhere_dense by TOPS_3:27;
hence X0 is nowhere_dense by Def4; ::_thesis: verum
end;
theorem :: TEX_3:43
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is boundary or X2 is boundary ) & X1 meets X2 holds
X1 meet X2 is boundary
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( X1 is boundary or X2 is boundary ) & X1 meets X2 holds
X1 meet X2 is boundary
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( X1 is boundary or X2 is boundary ) & X1 meets X2 implies X1 meet X2 is boundary )
assume A1: ( X1 is boundary or X2 is boundary ) ; ::_thesis: ( not X1 meets X2 or X1 meet X2 is boundary )
assume A2: X1 meets X2 ; ::_thesis: X1 meet X2 is boundary
hereby ::_thesis: verum
percases ( X1 is boundary or X2 is boundary ) by A1;
supposeA3: X1 is boundary ; ::_thesis: X1 meet X2 is boundary
X1 meet X2 is SubSpace of X1 by A2, TSEP_1:27;
hence X1 meet X2 is boundary by A3, Th34; ::_thesis: verum
end;
supposeA4: X2 is boundary ; ::_thesis: X1 meet X2 is boundary
X1 meet X2 is SubSpace of X2 by A2, TSEP_1:27;
hence X1 meet X2 is boundary by A4, Th34; ::_thesis: verum
end;
end;
end;
end;
theorem :: TEX_3:44
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 is nowhere_dense & X2 is nowhere_dense holds
X1 union X2 is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st X1 is nowhere_dense & X2 is nowhere_dense holds
X1 union X2 is nowhere_dense
let X1, X2 be non empty SubSpace of X; ::_thesis: ( X1 is nowhere_dense & X2 is nowhere_dense implies X1 union X2 is nowhere_dense )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume ( X1 is nowhere_dense & X2 is nowhere_dense ) ; ::_thesis: X1 union X2 is nowhere_dense
then ( A1 is nowhere_dense & A2 is nowhere_dense ) by Def4;
then A1 \/ A2 is nowhere_dense by TOPS_1:53;
then for A being Subset of X st A = the carrier of (X1 union X2) holds
A is nowhere_dense by TSEP_1:def_2;
hence X1 union X2 is nowhere_dense by Def4; ::_thesis: verum
end;
theorem :: TEX_3:45
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) holds
X1 union X2 is boundary
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) holds
X1 union X2 is boundary
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) implies X1 union X2 is boundary )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) ; ::_thesis: X1 union X2 is boundary
then ( ( A1 is nowhere_dense & A2 is boundary ) or ( A1 is boundary & A2 is nowhere_dense ) ) by Def3, Def4;
then A1 \/ A2 is boundary by TOPS_3:30;
then for A being Subset of X st A = the carrier of (X1 union X2) holds
A is boundary by TSEP_1:def_2;
hence X1 union X2 is boundary by Def3; ::_thesis: verum
end;
theorem :: TEX_3:46
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is nowhere_dense or X2 is nowhere_dense ) & X1 meets X2 holds
X1 meet X2 is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( X1 is nowhere_dense or X2 is nowhere_dense ) & X1 meets X2 holds
X1 meet X2 is nowhere_dense
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( X1 is nowhere_dense or X2 is nowhere_dense ) & X1 meets X2 implies X1 meet X2 is nowhere_dense )
assume A1: ( X1 is nowhere_dense or X2 is nowhere_dense ) ; ::_thesis: ( not X1 meets X2 or X1 meet X2 is nowhere_dense )
assume A2: X1 meets X2 ; ::_thesis: X1 meet X2 is nowhere_dense
hereby ::_thesis: verum
percases ( X1 is nowhere_dense or X2 is nowhere_dense ) by A1;
supposeA3: X1 is nowhere_dense ; ::_thesis: X1 meet X2 is nowhere_dense
X1 meet X2 is SubSpace of X1 by A2, TSEP_1:27;
hence X1 meet X2 is nowhere_dense by A3, Th40; ::_thesis: verum
end;
supposeA4: X2 is nowhere_dense ; ::_thesis: X1 meet X2 is nowhere_dense
X1 meet X2 is SubSpace of X2 by A2, TSEP_1:27;
hence X1 meet X2 is nowhere_dense by A4, Th40; ::_thesis: verum
end;
end;
end;
end;
begin
theorem :: TEX_3:47
for X being non empty TopSpace st ( for X0 being SubSpace of X holds not X0 is boundary ) holds
X is discrete
proof
let X be non empty TopSpace; ::_thesis: ( ( for X0 being SubSpace of X holds not X0 is boundary ) implies X is discrete )
assume A1: for X0 being SubSpace of X holds not X0 is boundary ; ::_thesis: X is discrete
now__::_thesis:_for_A_being_non_empty_Subset_of_X_holds_not_A_is_boundary
let A be non empty Subset of X; ::_thesis: not A is boundary
consider X0 being non empty strict SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
not X0 is boundary by A1;
hence not A is boundary by A2, Th29; ::_thesis: verum
end;
hence X is discrete by TEX_1:def_5; ::_thesis: verum
end;
theorem :: TEX_3:48
for X being non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is dense ) holds
X is discrete
proof
let X be non trivial TopSpace; ::_thesis: ( ( for X0 being proper SubSpace of X holds not X0 is dense ) implies X is discrete )
assume A1: for X0 being proper SubSpace of X holds not X0 is dense ; ::_thesis: X is discrete
now__::_thesis:_for_A_being_Subset_of_X_st_A_<>_the_carrier_of_X_holds_
not_A_is_dense
let A be Subset of X; ::_thesis: ( A <> the carrier of X implies not A is dense )
assume A2: A <> the carrier of X ; ::_thesis: not A is dense
now__::_thesis:_not_A_is_dense
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: not A is dense
hence not A is dense by TOPS_3:17; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: not A is dense
then consider X0 being non empty strict SubSpace of X such that
A3: A = the carrier of X0 by TSEP_1:10;
A is proper by A2, SUBSET_1:def_6;
then reconsider X0 = X0 as strict proper SubSpace of X by A3, TEX_2:8;
not X0 is dense by A1;
hence not A is dense by A3, Th9; ::_thesis: verum
end;
end;
end;
hence not A is dense ; ::_thesis: verum
end;
hence X is discrete by TEX_1:31; ::_thesis: verum
end;
registration
let X be non empty discrete TopSpace;
cluster non empty -> non empty non boundary for SubSpace of X;
coherence
for b1 being non empty SubSpace of X holds not b1 is boundary ;
cluster proper -> non dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper holds
not b1 is dense ;
cluster dense -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense holds
not b1 is proper ;
end;
registration
let X be non empty discrete TopSpace;
cluster non empty strict TopSpace-like closed open discrete almost_discrete non boundary for SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is boundary & b1 is strict & not b1 is empty )
proof
set X0 = the non empty strict SubSpace of X;
take the non empty strict SubSpace of X ; ::_thesis: ( not the non empty strict SubSpace of X is boundary & the non empty strict SubSpace of X is strict & not the non empty strict SubSpace of X is empty )
thus ( not the non empty strict SubSpace of X is boundary & the non empty strict SubSpace of X is strict & not the non empty strict SubSpace of X is empty ) ; ::_thesis: verum
end;
end;
registration
let X be non trivial discrete TopSpace;
cluster strict TopSpace-like closed open discrete almost_discrete non dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is dense & b1 is strict )
proof
set X0 = the strict proper SubSpace of X;
take the strict proper SubSpace of X ; ::_thesis: ( not the strict proper SubSpace of X is dense & the strict proper SubSpace of X is strict )
thus ( not the strict proper SubSpace of X is dense & the strict proper SubSpace of X is strict ) ; ::_thesis: verum
end;
end;
theorem :: TEX_3:49
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st X0 is boundary holds
not X is discrete ;
theorem :: TEX_3:50
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is dense & X0 is proper ) holds
not X is discrete ;
registration
let X be non empty non discrete TopSpace;
cluster non empty strict TopSpace-like boundary for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is boundary & b1 is strict & not b1 is empty )
proof
consider A0 being non empty Subset of X such that
A1: A0 is boundary by TEX_1:def_5;
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 boundary & X0 is strict & not X0 is empty )
for A being Subset of X st A = the carrier of X0 holds
A is boundary by A1, A2;
hence ( X0 is boundary & X0 is strict & not X0 is empty ) by Def3; ::_thesis: verum
end;
cluster non empty strict TopSpace-like proper dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is proper & b1 is strict & not b1 is empty )
proof
consider A0 being Subset of X such that
A3: A0 <> the carrier of X and
A4: A0 is dense by TEX_1:31;
not A0 is empty by A4, TOPS_3:17;
then consider X0 being non empty strict dense SubSpace of X such that
A5: A0 = the carrier of X0 by A4, Th10;
take X0 ; ::_thesis: ( X0 is dense & X0 is proper & X0 is strict & not X0 is empty )
A0 is proper by A3, SUBSET_1:def_6;
hence ( X0 is dense & X0 is proper & X0 is strict & not X0 is empty ) by A5, TEX_2:8; ::_thesis: verum
end;
end;
theorem :: TEX_3:51
for X being non empty non discrete TopSpace
for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non discrete TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is boundary implies ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0 )
assume A0 is boundary ; ::_thesis: ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0
then ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 ) by Th30;
hence ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0 ; ::_thesis: verum
end;
theorem :: TEX_3:52
for X being non empty non discrete TopSpace
for A0 being non empty proper Subset of X st A0 is dense holds
ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non discrete TopSpace; ::_thesis: for A0 being non empty proper Subset of X st A0 is dense holds
ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty proper Subset of X; ::_thesis: ( A0 is dense implies ex X0 being strict proper dense 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 dense ; ::_thesis: ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0
then reconsider X0 = X0 as strict proper dense SubSpace of X by A1, Th9, TEX_2:8;
take X0 ; ::_thesis: A0 = the carrier of X0
thus A0 = the carrier of X0 by A1; ::_thesis: verum
end;
theorem :: TEX_3:53
for X being non empty non discrete TopSpace
for X1 being non empty boundary SubSpace of X ex X2 being non empty strict proper dense SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non discrete TopSpace; ::_thesis: for X1 being non empty boundary SubSpace of X ex X2 being non empty strict proper dense SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty boundary SubSpace of X; ::_thesis: ex X2 being non empty strict proper dense SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict proper dense SubSpace of X by A1, Th31;
take X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;
theorem :: TEX_3:54
for X being non empty non discrete TopSpace
for X1 being non empty proper dense SubSpace of X ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non discrete TopSpace; ::_thesis: for X1 being non empty proper dense SubSpace of X ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty proper dense SubSpace of X; ::_thesis: ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict boundary SubSpace of X by A1, Th31;
take X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;
theorem :: TEX_3:55
for X being non empty non discrete TopSpace
for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X )
proof
let X be non empty non discrete TopSpace; ::_thesis: for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X )
let X1, X2 be non empty TopSpace; ::_thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is boundary SubSpace of X iff X2 is boundary SubSpace of X ) )
assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; ::_thesis: ( X1 is boundary SubSpace of X iff X2 is boundary SubSpace of X )
thus ( X1 is boundary SubSpace of X implies X2 is boundary SubSpace of X ) ::_thesis: ( X2 is boundary SubSpace of X implies X1 is boundary SubSpace of X )
proof
assume A2: X1 is boundary SubSpace of X ; ::_thesis: X2 is boundary SubSpace of X
then reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1:7;
for A2 being Subset of X st A2 = the carrier of Y2 holds
A2 is boundary by A1, A2, Def3;
hence X2 is boundary SubSpace of X by Def3; ::_thesis: verum
end;
assume A3: X2 is boundary SubSpace of X ; ::_thesis: X1 is boundary SubSpace of X
then reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1:7;
for A1 being Subset of X st A1 = the carrier of Y1 holds
A1 is boundary by A1, A3, Def3;
hence X1 is boundary SubSpace of X by Def3; ::_thesis: verum
end;
begin
theorem :: TEX_3:56
for X being non empty TopSpace st ( for X0 being SubSpace of X holds not X0 is nowhere_dense ) holds
X is almost_discrete
proof
let X be non empty TopSpace; ::_thesis: ( ( for X0 being SubSpace of X holds not X0 is nowhere_dense ) implies X is almost_discrete )
assume A1: for X0 being SubSpace of X holds not X0 is nowhere_dense ; ::_thesis: X is almost_discrete
now__::_thesis:_for_A_being_non_empty_Subset_of_X_holds_not_A_is_nowhere_dense
let A be non empty Subset of X; ::_thesis: not A is nowhere_dense
consider X0 being non empty strict SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
not X0 is nowhere_dense by A1;
hence not A is nowhere_dense by A2, Th35; ::_thesis: verum
end;
hence X is almost_discrete by TEX_1:def_6; ::_thesis: verum
end;
theorem :: TEX_3:57
for X being non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is everywhere_dense ) holds
X is almost_discrete
proof
let X be non trivial TopSpace; ::_thesis: ( ( for X0 being proper SubSpace of X holds not X0 is everywhere_dense ) implies X is almost_discrete )
assume A1: for X0 being proper SubSpace of X holds not X0 is everywhere_dense ; ::_thesis: X is almost_discrete
now__::_thesis:_for_A_being_Subset_of_X_st_A_<>_the_carrier_of_X_holds_
not_A_is_everywhere_dense
let A be Subset of X; ::_thesis: ( A <> the carrier of X implies not A is everywhere_dense )
assume A2: A <> the carrier of X ; ::_thesis: not A is everywhere_dense
now__::_thesis:_not_A_is_everywhere_dense
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: not A is everywhere_dense
hence not A is everywhere_dense by TOPS_3:34; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: not A is everywhere_dense
then consider X0 being non empty strict SubSpace of X such that
A3: A = the carrier of X0 by TSEP_1:10;
A is proper by A2, SUBSET_1:def_6;
then reconsider X0 = X0 as strict proper SubSpace of X by A3, TEX_2:8;
not X0 is everywhere_dense by A1;
hence not A is everywhere_dense by A3, Th16; ::_thesis: verum
end;
end;
end;
hence not A is everywhere_dense ; ::_thesis: verum
end;
hence X is almost_discrete by TEX_1:32; ::_thesis: verum
end;
registration
let X be non empty almost_discrete TopSpace;
cluster non empty -> non empty non nowhere_dense for SubSpace of X;
coherence
for b1 being non empty SubSpace of X holds not b1 is nowhere_dense
proof
let X0 be non empty SubSpace of X; ::_thesis: not X0 is nowhere_dense
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
not A is nowhere_dense by TEX_1:def_6;
hence not X0 is nowhere_dense by Th35; ::_thesis: verum
end;
cluster proper -> non everywhere_dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is proper holds
not b1 is everywhere_dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is proper implies not X0 is everywhere_dense )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is proper ; ::_thesis: not X0 is everywhere_dense
then A is proper by TEX_2:8;
then A <> the carrier of X by SUBSET_1:def_6;
then not A is everywhere_dense by TEX_1:32;
hence not X0 is everywhere_dense by Th16; ::_thesis: verum
end;
cluster everywhere_dense -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is everywhere_dense holds
not b1 is proper ;
cluster non empty boundary -> non empty non closed for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is boundary holds
not b1 is closed ;
cluster non empty closed -> non empty non boundary for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is closed holds
not b1 is boundary ;
cluster proper dense -> non open for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is proper holds
not b1 is open ;
cluster open dense -> non proper for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is dense & b1 is open holds
not b1 is proper ;
cluster open proper -> non dense for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is open & b1 is proper holds
not b1 is dense ;
end;
registration
let X be non empty almost_discrete TopSpace;
cluster non empty strict TopSpace-like non nowhere_dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is nowhere_dense & b1 is strict & not b1 is empty )
proof
set X0 = the non empty strict SubSpace of X;
take the non empty strict SubSpace of X ; ::_thesis: ( not the non empty strict SubSpace of X is nowhere_dense & the non empty strict SubSpace of X is strict & not the non empty strict SubSpace of X is empty )
thus ( not the non empty strict SubSpace of X is nowhere_dense & the non empty strict SubSpace of X is strict & not the non empty strict SubSpace of X is empty ) ; ::_thesis: verum
end;
end;
registration
let X be non trivial almost_discrete TopSpace;
cluster strict TopSpace-like non everywhere_dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( not b1 is everywhere_dense & b1 is strict )
proof
set X0 = the strict proper SubSpace of X;
take the strict proper SubSpace of X ; ::_thesis: ( not the strict proper SubSpace of X is everywhere_dense & the strict proper SubSpace of X is strict )
thus ( not the strict proper SubSpace of X is everywhere_dense & the strict proper SubSpace of X is strict ) ; ::_thesis: verum
end;
end;
theorem :: TEX_3:58
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st X0 is nowhere_dense holds
not X is almost_discrete ;
theorem :: TEX_3:59
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is boundary & X0 is closed ) holds
not X is almost_discrete ;
theorem :: TEX_3:60
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is everywhere_dense & X0 is proper ) holds
not X is almost_discrete ;
theorem :: TEX_3:61
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is dense & X0 is open & X0 is proper ) holds
not X is almost_discrete ;
registration
let X be non empty non almost_discrete TopSpace;
cluster non empty strict TopSpace-like nowhere_dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is nowhere_dense & b1 is strict & not b1 is empty )
proof
consider A0 being non empty Subset of X such that
A1: A0 is nowhere_dense by TEX_1:def_6;
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 nowhere_dense & X0 is strict & not X0 is empty )
for A being Subset of X st A = the carrier of X0 holds
A is nowhere_dense by A1, A2;
hence ( X0 is nowhere_dense & X0 is strict & not X0 is empty ) by Def4; ::_thesis: verum
end;
cluster non empty strict TopSpace-like proper everywhere_dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is everywhere_dense & b1 is proper & b1 is strict & not b1 is empty )
proof
consider A0 being Subset of X such that
A3: A0 <> the carrier of X and
A4: A0 is everywhere_dense by TEX_1:32;
not A0 is empty by A4, TOPS_3:34;
then consider X0 being non empty strict everywhere_dense SubSpace of X such that
A5: A0 = the carrier of X0 by A4, Th17;
take X0 ; ::_thesis: ( X0 is everywhere_dense & X0 is proper & X0 is strict & not X0 is empty )
A0 is proper by A3, SUBSET_1:def_6;
hence ( X0 is everywhere_dense & X0 is proper & X0 is strict & not X0 is empty ) by A5, TEX_2:8; ::_thesis: verum
end;
end;
theorem Th62: :: TEX_3:62
for X being non empty non almost_discrete TopSpace
for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is nowhere_dense implies ex X0 being non empty strict nowhere_dense 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 nowhere_dense ; ::_thesis: ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0
then reconsider Y0 = X0 as non empty strict nowhere_dense SubSpace of X by A1, Th35;
take Y0 ; ::_thesis: A0 = the carrier of Y0
thus A0 = the carrier of Y0 by A1; ::_thesis: verum
end;
theorem :: TEX_3:63
for X being non empty non almost_discrete TopSpace
for A0 being non empty proper Subset of X st A0 is everywhere_dense holds
ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for A0 being non empty proper Subset of X st A0 is everywhere_dense holds
ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty proper Subset of X; ::_thesis: ( A0 is everywhere_dense implies ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0 )
assume A0 is everywhere_dense ; ::_thesis: ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0
then consider X0 being non empty strict everywhere_dense SubSpace of X such that
A1: A0 = the carrier of X0 by Th17;
reconsider X0 = X0 as strict proper everywhere_dense SubSpace of X by A1, TEX_2:8;
take X0 ; ::_thesis: A0 = the carrier of X0
thus A0 = the carrier of X0 by A1; ::_thesis: verum
end;
theorem :: TEX_3:64
for X being non empty non almost_discrete TopSpace
for X1 being non empty nowhere_dense SubSpace of X ex X2 being non empty strict proper everywhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X1 being non empty nowhere_dense SubSpace of X ex X2 being non empty strict proper everywhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty nowhere_dense SubSpace of X; ::_thesis: ex X2 being non empty strict proper everywhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict proper everywhere_dense SubSpace of X by A1, Th37;
take X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;
theorem :: TEX_3:65
for X being non empty non almost_discrete TopSpace
for X1 being non empty proper everywhere_dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X1 being non empty proper everywhere_dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty proper everywhere_dense SubSpace of X; ::_thesis: ex X2 being non empty strict nowhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict nowhere_dense SubSpace of X by A1, Th37;
take X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;
theorem :: TEX_3:66
for X being non empty non almost_discrete TopSpace
for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X )
let X1, X2 be non empty TopSpace; ::_thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is nowhere_dense SubSpace of X iff X2 is nowhere_dense SubSpace of X ) )
assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; ::_thesis: ( X1 is nowhere_dense SubSpace of X iff X2 is nowhere_dense SubSpace of X )
thus ( X1 is nowhere_dense SubSpace of X implies X2 is nowhere_dense SubSpace of X ) ::_thesis: ( X2 is nowhere_dense SubSpace of X implies X1 is nowhere_dense SubSpace of X )
proof
assume A2: X1 is nowhere_dense SubSpace of X ; ::_thesis: X2 is nowhere_dense SubSpace of X
then reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1:7;
for A2 being Subset of X st A2 = the carrier of Y2 holds
A2 is nowhere_dense by A1, A2, Def4;
hence X2 is nowhere_dense SubSpace of X by Def4; ::_thesis: verum
end;
assume A3: X2 is nowhere_dense SubSpace of X ; ::_thesis: X1 is nowhere_dense SubSpace of X
then reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1:7;
for A1 being Subset of X st A1 = the carrier of Y1 holds
A1 is nowhere_dense by A1, A3, Def4;
hence X1 is nowhere_dense SubSpace of X by Def4; ::_thesis: verum
end;
registration
let X be non empty non almost_discrete TopSpace;
cluster non empty strict TopSpace-like closed boundary for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is boundary & b1 is closed & b1 is strict & not b1 is empty )
proof
consider A being non empty Subset of X such that
A1: A is nowhere_dense by TEX_1:def_6;
consider C being Subset of X such that
A2: A c= C and
A3: ( C is closed & C is boundary ) by A1, TOPS_3:27;
not C is empty by A2, XBOOLE_1:3;
then consider X0 being non empty strict SubSpace of X such that
A4: C = the carrier of X0 by TSEP_1:10;
take X0 ; ::_thesis: ( X0 is boundary & X0 is closed & X0 is strict & not X0 is empty )
( ( for C being Subset of X st C = the carrier of X0 holds
C is boundary ) & ( for C being Subset of X st C = the carrier of X0 holds
C is closed ) ) by A3, A4;
hence ( X0 is boundary & X0 is closed & X0 is strict & not X0 is empty ) by Def3, BORSUK_1:def_11; ::_thesis: verum
end;
cluster non empty strict TopSpace-like open proper dense for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is dense & b1 is open & b1 is proper & b1 is strict & not b1 is empty )
proof
consider A0 being Subset of X such that
A5: A0 <> the carrier of X and
A6: ( A0 is dense & A0 is open ) by TEX_1:34;
not A0 is empty by A6, TOPS_3:17;
then consider X0 being non empty strict open dense SubSpace of X such that
A7: A0 = the carrier of X0 by A6, Th23;
take X0 ; ::_thesis: ( X0 is dense & X0 is open & X0 is proper & X0 is strict & not X0 is empty )
A0 is proper by A5, SUBSET_1:def_6;
hence ( X0 is dense & X0 is open & X0 is proper & X0 is strict & not X0 is empty ) by A7, TEX_2:8; ::_thesis: verum
end;
end;
theorem Th67: :: TEX_3:67
for X being non empty non almost_discrete TopSpace
for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is boundary & A0 is closed implies ex X0 being non empty strict closed boundary 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 boundary & A0 is closed ) ; ::_thesis: ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0
then reconsider Y0 = X0 as non empty strict closed boundary SubSpace of X by A1, Th29, TSEP_1:11;
take Y0 ; ::_thesis: A0 = the carrier of Y0
thus A0 = the carrier of Y0 by A1; ::_thesis: verum
end;
theorem :: TEX_3:68
for X being non empty non almost_discrete TopSpace
for A0 being non empty proper Subset of X st A0 is dense & A0 is open holds
ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for A0 being non empty proper Subset of X st A0 is dense & A0 is open holds
ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty proper Subset of X; ::_thesis: ( A0 is dense & A0 is open implies ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0 )
assume ( A0 is dense & A0 is open ) ; ::_thesis: ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0
then consider X0 being non empty strict open dense SubSpace of X such that
A1: A0 = the carrier of X0 by Th23;
reconsider X0 = X0 as strict open proper dense SubSpace of X by A1, TEX_2:8;
take X0 ; ::_thesis: A0 = the carrier of X0
thus A0 = the carrier of X0 by A1; ::_thesis: verum
end;
theorem :: TEX_3:69
for X being non empty non almost_discrete TopSpace
for X1 being non empty closed boundary SubSpace of X ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X1 being non empty closed boundary SubSpace of X ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty closed boundary SubSpace of X; ::_thesis: ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict open proper dense SubSpace of X by A1, Th31, TSEP_2:34;
take X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;
theorem :: TEX_3:70
for X being non empty non almost_discrete TopSpace
for X1 being non empty open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X1 being non empty open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty open proper dense SubSpace of X; ::_thesis: ex X2 being non empty strict closed boundary SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict closed boundary SubSpace of X by A1, Th31, TSEP_2:33;
take X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;
theorem :: TEX_3:71
for X being non empty non almost_discrete TopSpace
for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus ( X0 is nowhere_dense implies ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 ) ::_thesis: ( ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 implies X0 is nowhere_dense )
proof
assume X0 is nowhere_dense ; ::_thesis: ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1
then A is nowhere_dense by Def4;
then consider C being Subset of X such that
A1: A c= C and
A2: ( C is closed & C is boundary ) by TOPS_3:27;
not C is empty by A1, XBOOLE_1:3;
then consider X1 being non empty strict closed boundary SubSpace of X such that
A3: C = the carrier of X1 by A2, Th67;
take X1 ; ::_thesis: X0 is SubSpace of X1
thus X0 is SubSpace of X1 by A1, A3, TSEP_1:4; ::_thesis: verum
end;
given X1 being non empty strict closed boundary SubSpace of X such that A4: X0 is SubSpace of X1 ; ::_thesis: X0 is nowhere_dense
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;
now__::_thesis:_ex_C_being_Subset_of_X_st_
(_A_c=_C_&_C_is_boundary_&_C_is_closed_)
take C = C; ::_thesis: ( A c= C & C is boundary & C is closed )
thus ( A c= C & C is boundary & C is closed ) by A4, Def3, TSEP_1:4, TSEP_1:11; ::_thesis: verum
end;
then for A being Subset of X st A = the carrier of X0 holds
A is nowhere_dense by TOPS_3:27;
hence X0 is nowhere_dense by Def4; ::_thesis: verum
end;
theorem :: TEX_3:72
for X being non empty non almost_discrete TopSpace
for X0 being non empty nowhere_dense SubSpace of X holds
( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X0 being non empty nowhere_dense SubSpace of X holds
( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )
let X0 be non empty nowhere_dense SubSpace of X; ::_thesis: ( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
A1: X is SubSpace of X by TSEP_1:2;
D is nowhere_dense by Th35;
then consider C, B being Subset of X such that
A2: ( C is closed & C is boundary ) and
A3: B is everywhere_dense and
A4: C /\ B = D and
A5: C \/ B = the carrier of X by TOPS_3:51;
B <> {} by A4;
then consider X1 being non empty strict everywhere_dense SubSpace of X such that
A6: B = the carrier of X1 by A3, Th17;
assume A7: ( not X0 is boundary or not X0 is closed ) ; ::_thesis: ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) )
now__::_thesis:_B_is_proper
assume not B is proper ; ::_thesis: contradiction
then B = the carrier of X by SUBSET_1:def_6;
then D = C by A4, XBOOLE_1:28;
hence contradiction by A7, A2, TSEP_1:11; ::_thesis: verum
end;
then reconsider X1 = X1 as non empty strict proper everywhere_dense SubSpace of X by A6, TEX_2:8;
C <> {} by A4;
then consider X2 being non empty strict closed boundary SubSpace of X such that
A8: C = the carrier of X2 by A2, Th67;
take X1 ; ::_thesis: ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) )
take X2 ; ::_thesis: ( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) )
C meets B by A4, XBOOLE_0:def_7;
then X1 meets X2 by A8, A6, TSEP_1:def_3;
then the carrier of (X1 meet X2) = D by A4, A8, A6, TSEP_1:def_4;
hence X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) by TSEP_1:5; ::_thesis: X1 union X2 = TopStruct(# the carrier of X, the topology of X #)
the carrier of (X1 union X2) = the carrier of X by A5, A8, A6, TSEP_1:def_2;
hence X1 union X2 = TopStruct(# the carrier of X, the topology of X #) by A1, TSEP_1:5; ::_thesis: verum
end;
theorem :: TEX_3:73
for X being non empty non almost_discrete TopSpace
for X0 being non empty everywhere_dense SubSpace of X holds
( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X0 being non empty everywhere_dense SubSpace of X holds
( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )
let X0 be non empty everywhere_dense SubSpace of X; ::_thesis: ( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
D is everywhere_dense by Th16;
then consider C, B being Subset of X such that
A1: ( C is open & C is dense ) and
A2: B is nowhere_dense and
A3: C \/ B = D and
A4: C misses B by TOPS_3:49;
C <> {} by A1, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A5: C = the carrier of X1 by A1, Th23;
assume A6: ( not X0 is dense or not X0 is open ) ; ::_thesis: ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) )
now__::_thesis:_C_is_proper
assume not C is proper ; ::_thesis: contradiction
then A7: C = the carrier of X by SUBSET_1:def_6;
C c= D by A3, XBOOLE_1:7;
then D = [#] X by A7, XBOOLE_0:def_10;
then ( D is dense & D is open ) ;
hence contradiction by A6, TSEP_1:16; ::_thesis: verum
end;
then reconsider X1 = X1 as non empty strict open proper dense SubSpace of X by A5, TEX_2:8;
now__::_thesis:_not_B_=_{}
percases ( not X0 is dense or not X0 is open ) by A6;
supposeA8: not X0 is dense ; ::_thesis: not B = {}
assume B = {} ; ::_thesis: contradiction
thus contradiction by A8; ::_thesis: verum
end;
supposeA9: not X0 is open ; ::_thesis: not B = {}
assume B = {} ; ::_thesis: contradiction
hence contradiction by A1, A3, A9, TSEP_1:16; ::_thesis: verum
end;
end;
end;
then consider X2 being non empty strict nowhere_dense SubSpace of X such that
A10: B = the carrier of X2 by A2, Th62;
take X1 ; ::_thesis: ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) )
take X2 ; ::_thesis: ( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) )
thus X1 misses X2 by A4, A5, A10, TSEP_1:def_3; ::_thesis: X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #)
the carrier of (X1 union X2) = the carrier of X0 by A3, A5, A10, TSEP_1:def_2;
hence X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) by TSEP_1:5; ::_thesis: verum
end;
theorem :: TEX_3:74
for X being non empty non almost_discrete TopSpace
for X0 being non empty nowhere_dense SubSpace of X ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X0 being non empty nowhere_dense SubSpace of X ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
let X0 be non empty nowhere_dense SubSpace of X; ::_thesis: ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
D is nowhere_dense by Th35;
then consider C, B being Subset of X such that
A1: ( C is closed & C is boundary ) and
A2: ( B is open & B is dense ) and
A3: C /\ (D \/ B) = D and
A4: C misses B and
A5: C \/ B = the carrier of X by TOPS_3:52;
B <> {} by A2, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A6: B = the carrier of X1 by A2, Th23;
A7: C <> {} by A3;
then consider X2 being non empty strict closed boundary SubSpace of X such that
A8: C = the carrier of X2 by A1, Th67;
A9: C /\ B = {} by A4, XBOOLE_0:def_7;
now__::_thesis:_B_is_proper
assume not B is proper ; ::_thesis: contradiction
then B = the carrier of X by SUBSET_1:def_6;
hence contradiction by A7, A9, XBOOLE_1:28; ::_thesis: verum
end;
then reconsider X1 = X1 as non empty strict open proper dense SubSpace of X by A6, TEX_2:8;
take X1 ; ::_thesis: ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
take X2 ; ::_thesis: ( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
for P, Q being Subset of X st P = the carrier of X1 & Q = the carrier of X2 holds
P,Q constitute_a_decomposition by A4, A5, A6, A8, TSEP_2:def_1;
hence X1,X2 constitute_a_decomposition by TSEP_2:def_2; ::_thesis: X0 is SubSpace of X2
D c= C by A3, XBOOLE_1:17;
hence X0 is SubSpace of X2 by A8, TSEP_1:4; ::_thesis: verum
end;
theorem :: TEX_3:75
for X being non empty non almost_discrete TopSpace
for X0 being proper everywhere_dense SubSpace of X ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X0 being proper everywhere_dense SubSpace of X ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
let X0 be proper everywhere_dense SubSpace of X; ::_thesis: ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
D is everywhere_dense by Th16;
then consider C, B being Subset of X such that
A1: ( C is open & C is dense ) and
A2: ( B is closed & B is boundary ) and
A3: C \/ (D /\ B) = D and
A4: C misses B and
A5: C \/ B = the carrier of X by TOPS_3:50;
C <> {} by A1, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A6: C = the carrier of X1 by A1, Th23;
A7: now__::_thesis:_C_is_proper
assume not C is proper ; ::_thesis: contradiction
then C = the carrier of X by SUBSET_1:def_6;
then the carrier of X c= D by A3, XBOOLE_1:7;
then D = the carrier of X by XBOOLE_0:def_10;
then not D is proper by SUBSET_1:def_6;
hence contradiction by TEX_2:8; ::_thesis: verum
end;
then not B is empty by A5, SUBSET_1:def_6;
then consider X2 being non empty strict closed boundary SubSpace of X such that
A8: B = the carrier of X2 by A2, Th67;
reconsider X1 = X1 as strict open proper dense SubSpace of X by A6, A7, TEX_2:8;
take X1 ; ::_thesis: ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
take X2 ; ::_thesis: ( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
for P, Q being Subset of X st P = the carrier of X1 & Q = the carrier of X2 holds
P,Q constitute_a_decomposition by A4, A5, A6, A8, TSEP_2:def_1;
hence X1,X2 constitute_a_decomposition by TSEP_2:def_2; ::_thesis: X1 is SubSpace of X0
C c= D by A3, XBOOLE_1:7;
hence X1 is SubSpace of X0 by A6, TSEP_1:4; ::_thesis: verum
end;