:: TEX_4 semantic presentation
begin
registration
let X be non empty TopSpace;
let A be non empty Subset of X;
cluster Cl A -> non empty ;
coherence
not Cl A is empty by PCOMPS_1:2;
end;
registration
let X be TopSpace;
let A be empty Subset of X;
cluster Cl A -> empty ;
coherence
Cl A is empty by PRE_TOPC:22;
end;
registration
let X be non empty TopSpace;
let A be non proper Subset of X;
cluster Cl A -> non proper ;
coherence
not Cl A is proper
proof
A = [#] X by SUBSET_1:def_6;
hence not Cl A is proper by TOPS_1:2; ::_thesis: verum
end;
end;
registration
let X be non trivial TopSpace;
let A be non trivial Subset of X;
cluster Cl A -> non trivial ;
coherence
not Cl A is trivial
proof
A c= Cl A by PRE_TOPC:18;
hence not Cl A is trivial ; ::_thesis: verum
end;
end;
theorem Th1: :: TEX_4:1
for X being non empty TopSpace
for A being Subset of X holds Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) }
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) }
let A be Subset of X; ::_thesis: Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) }
set G = { F where F is Subset of X : ( F is closed & A c= F ) } ;
A1: { F where F is Subset of X : ( F is closed & A c= F ) } c= bool the carrier of X
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { F where F is Subset of X : ( F is closed & A c= F ) } or C in bool the carrier of X )
assume C in { F where F is Subset of X : ( F is closed & A c= F ) } ; ::_thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is closed & A c= P ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
[#] X in { F where F is Subset of X : ( F is closed & A c= F ) } ;
then reconsider G = { F where F is Subset of X : ( F is closed & A c= F ) } as non empty Subset-Family of X by A1;
now__::_thesis:_for_P_being_set_st_P_in_G_holds_
A_c=_P
let P be set ; ::_thesis: ( P in G implies A c= P )
assume P in G ; ::_thesis: A c= P
then ex F being Subset of X st
( F = P & F is closed & A c= F ) ;
hence A c= P ; ::_thesis: verum
end;
then A2: A c= meet G by SETFAM_1:5;
A c= Cl A by PRE_TOPC:18;
then Cl A in G ;
then A3: meet G c= Cl A by SETFAM_1:3;
now__::_thesis:_for_S_being_Subset_of_X_st_S_in_G_holds_
S_is_closed
let S be Subset of X; ::_thesis: ( S in G implies S is closed )
assume S in G ; ::_thesis: S is closed
then ex F being Subset of X st
( F = S & F is closed & A c= F ) ;
hence S is closed ; ::_thesis: verum
end;
then G is closed by TOPS_2:def_2;
then Cl A c= meet G by A2, TOPS_1:5, TOPS_2:22;
hence Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) } by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th2: :: TEX_4:2
for X being non empty TopSpace
for x being Point of X holds Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) }
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X holds Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) }
let x be Point of X; ::_thesis: Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) }
set G = { F where F is Subset of X : ( F is closed & x in F ) } ;
set H = { F where F is Subset of X : ( F is closed & {x} c= F ) } ;
now__::_thesis:_for_P_being_set_st_P_in__{__F_where_F_is_Subset_of_X_:_(_F_is_closed_&_x_in_F_)__}__holds_
P_in__{__F_where_F_is_Subset_of_X_:_(_F_is_closed_&_{x}_c=_F_)__}_
let P be set ; ::_thesis: ( P in { F where F is Subset of X : ( F is closed & x in F ) } implies P in { F where F is Subset of X : ( F is closed & {x} c= F ) } )
assume P in { F where F is Subset of X : ( F is closed & x in F ) } ; ::_thesis: P in { F where F is Subset of X : ( F is closed & {x} c= F ) }
then consider F being Subset of X such that
A1: F = P and
A2: F is closed and
A3: x in F ;
{x} c= F by A3, ZFMISC_1:31;
hence P in { F where F is Subset of X : ( F is closed & {x} c= F ) } by A1, A2; ::_thesis: verum
end;
then A4: { F where F is Subset of X : ( F is closed & x in F ) } c= { F where F is Subset of X : ( F is closed & {x} c= F ) } by TARSKI:def_3;
now__::_thesis:_for_P_being_set_st_P_in__{__F_where_F_is_Subset_of_X_:_(_F_is_closed_&_{x}_c=_F_)__}__holds_
P_in__{__F_where_F_is_Subset_of_X_:_(_F_is_closed_&_x_in_F_)__}_
let P be set ; ::_thesis: ( P in { F where F is Subset of X : ( F is closed & {x} c= F ) } implies P in { F where F is Subset of X : ( F is closed & x in F ) } )
assume P in { F where F is Subset of X : ( F is closed & {x} c= F ) } ; ::_thesis: P in { F where F is Subset of X : ( F is closed & x in F ) }
then consider F being Subset of X such that
A5: F = P and
A6: F is closed and
A7: {x} c= F ;
x in F by A7, ZFMISC_1:31;
hence P in { F where F is Subset of X : ( F is closed & x in F ) } by A5, A6; ::_thesis: verum
end;
then A8: { F where F is Subset of X : ( F is closed & {x} c= F ) } c= { F where F is Subset of X : ( F is closed & x in F ) } by TARSKI:def_3;
Cl {x} = meet { F where F is Subset of X : ( F is closed & {x} c= F ) } by Th1;
hence Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) } by A4, A8, XBOOLE_0:def_10; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
let A be non proper Subset of X;
cluster Int A -> non proper ;
coherence
not Int A is proper
proof
A = [#] X by SUBSET_1:def_6;
hence not Int A is proper by TOPS_1:15; ::_thesis: verum
end;
end;
registration
let X be non empty TopSpace;
let A be proper Subset of X;
cluster Int A -> proper ;
coherence
Int A is proper
proof
now__::_thesis:_Int_A_is_proper
assume not Int A is proper ; ::_thesis: contradiction
then A1: Int A = [#] X by SUBSET_1:def_6;
Int A c= A by TOPS_1:16;
hence contradiction by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
hence Int A is proper ; ::_thesis: verum
end;
end;
registration
let X be non empty TopSpace;
let A be empty Subset of X;
cluster Int A -> empty ;
coherence
Int A is empty ;
end;
theorem :: TEX_4:3
for X being non empty TopSpace
for A being Subset of X holds Int A = union { G where G is Subset of X : ( G is open & G c= A ) }
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds Int A = union { G where G is Subset of X : ( G is open & G c= A ) }
let A be Subset of X; ::_thesis: Int A = union { G where G is Subset of X : ( G is open & G c= A ) }
set F = { G where G is Subset of X : ( G is open & G c= A ) } ;
A1: { G where G is Subset of X : ( G is open & G c= A ) } c= bool the carrier of X
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & G c= A ) } or C in bool the carrier of X )
assume C in { G where G is Subset of X : ( G is open & G c= A ) } ; ::_thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is open & P c= A ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
{} c= A by XBOOLE_1:2;
then {} X in { G where G is Subset of X : ( G is open & G c= A ) } ;
then reconsider F = { G where G is Subset of X : ( G is open & G c= A ) } as non empty Subset-Family of X by A1;
now__::_thesis:_for_P_being_set_st_P_in_F_holds_
P_c=_A
let P be set ; ::_thesis: ( P in F implies P c= A )
assume P in F ; ::_thesis: P c= A
then ex G being Subset of X st
( G = P & G is open & G c= A ) ;
hence P c= A ; ::_thesis: verum
end;
then A2: union F c= A by ZFMISC_1:76;
Int A c= A by TOPS_1:16;
then Int A in F ;
then A3: Int A c= union F by ZFMISC_1:74;
now__::_thesis:_for_S_being_Subset_of_X_st_S_in_F_holds_
S_is_open
let S be Subset of X; ::_thesis: ( S in F implies S is open )
assume S in F ; ::_thesis: S is open
then ex G being Subset of X st
( G = S & G is open & G c= A ) ;
hence S is open ; ::_thesis: verum
end;
then F is open by TOPS_2:def_1;
then union F c= Int A by A2, TOPS_1:24, TOPS_2:19;
hence Int A = union { G where G is Subset of X : ( G is open & G c= A ) } by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
definition
let Y be TopStruct ;
let IT be Subset of Y;
attrIT is anti-discrete means :Def1: :: TEX_4:def 1
for x being Point of Y
for G being Subset of Y st G is open & x in G & x in IT holds
IT c= G;
end;
:: deftheorem Def1 defines anti-discrete TEX_4:def_1_:_
for Y being TopStruct
for IT being Subset of Y holds
( IT is anti-discrete iff for x being Point of Y
for G being Subset of Y st G is open & x in G & x in IT holds
IT c= G );
definition
let Y be non empty TopStruct ;
let A be Subset of Y;
redefine attr A is anti-discrete means :Def2: :: TEX_4:def 2
for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F;
compatibility
( A is anti-discrete iff for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F )
proof
hereby ::_thesis: ( ( for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F ) implies A is anti-discrete )
assume A1: A is anti-discrete ; ::_thesis: for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F
let x be Point of Y; ::_thesis: for F being Subset of Y st F is closed & x in F & x in A holds
A c= F
let F be Subset of Y; ::_thesis: ( F is closed & x in F & x in A implies A c= F )
set G = ([#] Y) \ F;
A2: A \ F c= ([#] Y) \ F by XBOOLE_1:33;
assume F is closed ; ::_thesis: ( x in F & x in A implies A c= F )
then A3: ([#] Y) \ F is open by PRE_TOPC:def_3;
assume A4: x in F ; ::_thesis: ( x in A implies A c= F )
assume A5: x in A ; ::_thesis: A c= F
assume not A c= F ; ::_thesis: contradiction
then A \ F <> {} by XBOOLE_1:37;
then consider a being set such that
A6: a in A \ F by XBOOLE_0:def_1;
a in A by A6, XBOOLE_0:def_5;
then A c= ([#] Y) \ F by A1, A6, A2, A3, Def1;
then A7: A misses (([#] Y) \ F) ` by SUBSET_1:24;
A8: (([#] Y) \ F) ` = (F `) `
.= F ;
not A /\ F is empty by A4, A5, XBOOLE_0:def_4;
hence contradiction by A8, A7, XBOOLE_0:def_7; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A9: for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F ; ::_thesis: A is anti-discrete
now__::_thesis:_for_x_being_Point_of_Y
for_G_being_Subset_of_Y_st_G_is_open_&_x_in_G_&_x_in_A_holds_
A_c=_G
let x be Point of Y; ::_thesis: for G being Subset of Y st G is open & x in G & x in A holds
A c= G
let G be Subset of Y; ::_thesis: ( G is open & x in G & x in A implies A c= G )
set F = ([#] Y) \ G;
A10: A \ G c= ([#] Y) \ G by XBOOLE_1:33;
A11: G = ([#] Y) \ (([#] Y) \ G) by PRE_TOPC:3;
assume G is open ; ::_thesis: ( x in G & x in A implies A c= G )
then A12: ([#] Y) \ G is closed by A11, PRE_TOPC:def_3;
assume A13: x in G ; ::_thesis: ( x in A implies A c= G )
assume A14: x in A ; ::_thesis: A c= G
assume not A c= G ; ::_thesis: contradiction
then A \ G <> {} by XBOOLE_1:37;
then consider a being set such that
A15: a in A \ G by XBOOLE_0:def_1;
A16: ([#] Y) \ G = G ` ;
a in A by A15, XBOOLE_0:def_5;
then A c= ([#] Y) \ G by A9, A15, A10, A12;
then A misses (([#] Y) \ G) ` by SUBSET_1:24;
hence contradiction by A13, A14, A16, XBOOLE_0:3; ::_thesis: verum
end;
hence A is anti-discrete by Def1; ::_thesis: verum
end;
end;
end;
:: deftheorem Def2 defines anti-discrete TEX_4:def_2_:_
for Y being non empty TopStruct
for A being Subset of Y holds
( A is anti-discrete iff for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F );
definition
let Y be TopStruct ;
let A be Subset of Y;
redefine attr A is anti-discrete means :Def3: :: TEX_4:def 3
for G being Subset of Y holds
( not G is open or A misses G or A c= G );
compatibility
( A is anti-discrete iff for G being Subset of Y holds
( not G is open or A misses G or A c= G ) )
proof
hereby ::_thesis: ( ( for G being Subset of Y holds
( not G is open or A misses G or A c= G ) ) implies A is anti-discrete )
assume A1: A is anti-discrete ; ::_thesis: for G being Subset of Y st G is open & A meets G holds
A c= G
let G be Subset of Y; ::_thesis: ( G is open & A meets G implies A c= G )
assume A2: G is open ; ::_thesis: ( A meets G implies A c= G )
assume A meets G ; ::_thesis: A c= G
then consider a being set such that
A3: a in A /\ G by XBOOLE_0:4;
reconsider a = a as Point of Y by A3;
A4: a in G by A3, XBOOLE_0:def_4;
a in A by A3, XBOOLE_0:def_4;
hence A c= G by A1, A2, A4, Def1; ::_thesis: verum
end;
assume A5: for G being Subset of Y holds
( not G is open or A misses G or A c= G ) ; ::_thesis: A is anti-discrete
now__::_thesis:_for_x_being_Point_of_Y
for_G_being_Subset_of_Y_st_G_is_open_&_x_in_G_&_x_in_A_holds_
A_c=_G
let x be Point of Y; ::_thesis: for G being Subset of Y st G is open & x in G & x in A holds
A c= G
let G be Subset of Y; ::_thesis: ( G is open & x in G & x in A implies A c= G )
assume A6: G is open ; ::_thesis: ( x in G & x in A implies A c= G )
assume A7: x in G ; ::_thesis: ( x in A implies A c= G )
assume x in A ; ::_thesis: A c= G
then A meets G by A7, XBOOLE_0:3;
hence A c= G by A5, A6; ::_thesis: verum
end;
hence A is anti-discrete by Def1; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines anti-discrete TEX_4:def_3_:_
for Y being TopStruct
for A being Subset of Y holds
( A is anti-discrete iff for G being Subset of Y holds
( not G is open or A misses G or A c= G ) );
definition
let Y be TopStruct ;
let A be Subset of Y;
redefine attr A is anti-discrete means :Def4: :: TEX_4:def 4
for F being Subset of Y holds
( not F is closed or A misses F or A c= F );
compatibility
( A is anti-discrete iff for F being Subset of Y holds
( not F is closed or A misses F or A c= F ) )
proof
hereby ::_thesis: ( ( for F being Subset of Y holds
( not F is closed or A misses F or A c= F ) ) implies A is anti-discrete )
assume A1: A is anti-discrete ; ::_thesis: for G being Subset of Y st G is closed & A meets G holds
A c= G
let G be Subset of Y; ::_thesis: ( G is closed & A meets G implies A c= G )
assume G is closed ; ::_thesis: ( A meets G implies A c= G )
then ([#] Y) \ G is open by PRE_TOPC:def_3;
then A2: ( A misses G ` or A c= G ` ) by A1, Def3;
assume A meets G ; ::_thesis: A c= G
then A c= (G `) ` by A2, SUBSET_1:23;
hence A c= G ; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A3: for G being Subset of Y holds
( not G is closed or A misses G or A c= G ) ; ::_thesis: A is anti-discrete
now__::_thesis:_for_G_being_Subset_of_Y_st_G_is_open_&_A_meets_G_holds_
A_c=_G
let G be Subset of Y; ::_thesis: ( G is open & A meets G implies A c= G )
A4: G = ([#] Y) \ (([#] Y) \ G) by PRE_TOPC:3;
assume G is open ; ::_thesis: ( A meets G implies A c= G )
then ([#] Y) \ G is closed by A4, PRE_TOPC:def_3;
then A5: ( A misses G ` or A c= G ` ) by A3;
assume A meets G ; ::_thesis: A c= G
then A c= (G `) ` by A5, SUBSET_1:23;
hence A c= G ; ::_thesis: verum
end;
hence A is anti-discrete by Def3; ::_thesis: verum
end;
end;
end;
:: deftheorem Def4 defines anti-discrete TEX_4:def_4_:_
for Y being TopStruct
for A being Subset of Y holds
( A is anti-discrete iff for F being Subset of Y holds
( not F is closed or A misses F or A c= F ) );
theorem Th4: :: TEX_4:4
for Y0, Y1 being TopStruct
for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds
D1 is anti-discrete
proof
let Y0, Y1 be TopStruct ; ::_thesis: for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds
D1 is anti-discrete
let D0 be Subset of Y0; ::_thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds
D1 is anti-discrete
let D1 be Subset of Y1; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete implies D1 is anti-discrete )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not D0 = D1 or not D0 is anti-discrete or D1 is anti-discrete )
assume A2: D0 = D1 ; ::_thesis: ( not D0 is anti-discrete or D1 is anti-discrete )
assume A3: D0 is anti-discrete ; ::_thesis: D1 is anti-discrete
now__::_thesis:_for_D_being_Subset_of_Y1_holds_
(_not_D_is_open_or_D1_misses_D_or_D1_c=_D_)
let D be Subset of Y1; ::_thesis: ( not D is open or D1 misses D or D1 c= D )
reconsider E = D as Subset of Y0 by A1;
assume D is open ; ::_thesis: ( D1 misses D or D1 c= D )
then E in the topology of Y0 by A1, PRE_TOPC:def_2;
then E is open by PRE_TOPC:def_2;
hence ( D1 misses D or D1 c= D ) by A2, A3, Def3; ::_thesis: verum
end;
hence D1 is anti-discrete by Def3; ::_thesis: verum
end;
theorem Th5: :: TEX_4:5
for Y being non empty TopStruct
for A, B being Subset of Y st B c= A & A is anti-discrete holds
B is anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st B c= A & A is anti-discrete holds
B is anti-discrete
let A, B be Subset of Y; ::_thesis: ( B c= A & A is anti-discrete implies B is anti-discrete )
assume A1: B c= A ; ::_thesis: ( not A is anti-discrete or B is anti-discrete )
assume A2: A is anti-discrete ; ::_thesis: B is anti-discrete
now__::_thesis:_for_G_being_Subset_of_Y_st_G_is_open_&_B_meets_G_holds_
B_c=_G
let G be Subset of Y; ::_thesis: ( G is open & B meets G implies B c= G )
assume A3: G is open ; ::_thesis: ( B meets G implies B c= G )
assume B meets G ; ::_thesis: B c= G
then B /\ G <> {} by XBOOLE_0:def_7;
then A /\ G <> {} by A1, XBOOLE_1:3, XBOOLE_1:26;
then A meets G by XBOOLE_0:def_7;
then A c= G by A2, A3, Def3;
hence B c= G by A1, XBOOLE_1:1; ::_thesis: verum
end;
hence B is anti-discrete by Def3; ::_thesis: verum
end;
theorem Th6: :: TEX_4:6
for Y being non empty TopStruct
for x being Point of Y holds {x} is anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds {x} is anti-discrete
let x be Point of Y; ::_thesis: {x} is anti-discrete
now__::_thesis:_for_G_being_Subset_of_Y_st_G_is_open_&_{x}_meets_G_holds_
{x}_c=_G
let G be Subset of Y; ::_thesis: ( G is open & {x} meets G implies {x} c= G )
assume G is open ; ::_thesis: ( {x} meets G implies {x} c= G )
assume {x} meets G ; ::_thesis: {x} c= G
then consider a being set such that
A1: a in {x} /\ G by XBOOLE_0:4;
a in {x} by A1, XBOOLE_0:def_4;
then A2: a = x by TARSKI:def_1;
a in G by A1, XBOOLE_0:def_4;
hence {x} c= G by A2, ZFMISC_1:31; ::_thesis: verum
end;
hence {x} is anti-discrete by Def3; ::_thesis: verum
end;
theorem Th7: :: TEX_4:7
for Y being non empty TopStruct
for A being empty Subset of Y holds A is anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for A being empty Subset of Y holds A is anti-discrete
let A be empty Subset of Y; ::_thesis: A is anti-discrete
for G being Subset of Y holds
( not G is open or A misses G or A c= G ) by XBOOLE_1:65;
hence A is anti-discrete by Def3; ::_thesis: verum
end;
definition
let Y be TopStruct ;
let IT be Subset-Family of Y;
attrIT is anti-discrete-set-family means :Def5: :: TEX_4:def 5
for A being Subset of Y st A in IT holds
A is anti-discrete ;
end;
:: deftheorem Def5 defines anti-discrete-set-family TEX_4:def_5_:_
for Y being TopStruct
for IT being Subset-Family of Y holds
( IT is anti-discrete-set-family iff for A being Subset of Y st A in IT holds
A is anti-discrete );
theorem Th8: :: TEX_4:8
for Y being non empty TopStruct
for F being Subset-Family of Y st F is anti-discrete-set-family & meet F <> {} holds
union F is anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for F being Subset-Family of Y st F is anti-discrete-set-family & meet F <> {} holds
union F is anti-discrete
let F be Subset-Family of Y; ::_thesis: ( F is anti-discrete-set-family & meet F <> {} implies union F is anti-discrete )
assume A1: F is anti-discrete-set-family ; ::_thesis: ( not meet F <> {} or union F is anti-discrete )
assume A2: meet F <> {} ; ::_thesis: union F is anti-discrete
for G being Subset of Y holds
( not G is open or union F misses G or union F c= G )
proof
let G be Subset of Y; ::_thesis: ( not G is open or union F misses G or union F c= G )
assume A3: G is open ; ::_thesis: ( union F misses G or union F c= G )
assume union F meets G ; ::_thesis: union F c= G
then consider A0 being set such that
A4: A0 in F and
A5: A0 meets G by ZFMISC_1:80;
reconsider A0 = A0 as Subset of Y by A4;
A0 is anti-discrete by A1, A4, Def5;
then A6: A0 c= G by A3, A5, Def3;
meet F c= A0 by A4, SETFAM_1:3;
then A7: meet F c= G by A6, XBOOLE_1:1;
for B being set st B in F holds
B c= G
proof
let B be set ; ::_thesis: ( B in F implies B c= G )
assume A8: B in F ; ::_thesis: B c= G
then reconsider B0 = B as Subset of Y ;
meet F c= B0 by A8, SETFAM_1:3;
then B0 /\ G <> {} by A2, A7, XBOOLE_1:3, XBOOLE_1:19;
then A9: B0 meets G by XBOOLE_0:def_7;
B0 is anti-discrete by A1, A8, Def5;
hence B c= G by A3, A9, Def3; ::_thesis: verum
end;
hence union F c= G by ZFMISC_1:76; ::_thesis: verum
end;
hence union F is anti-discrete by Def3; ::_thesis: verum
end;
theorem :: TEX_4:9
for Y being non empty TopStruct
for F being Subset-Family of Y st F is anti-discrete-set-family holds
meet F is anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for F being Subset-Family of Y st F is anti-discrete-set-family holds
meet F is anti-discrete
let F be Subset-Family of Y; ::_thesis: ( F is anti-discrete-set-family implies meet F is anti-discrete )
assume A1: F is anti-discrete-set-family ; ::_thesis: meet F is anti-discrete
hereby ::_thesis: verum
percases ( meet F = {} or meet F <> {} ) ;
suppose meet F = {} ; ::_thesis: meet F is anti-discrete
hence meet F is anti-discrete by Th7; ::_thesis: verum
end;
supposeA2: meet F <> {} ; ::_thesis: meet F is anti-discrete
meet F c= union F by SETFAM_1:2;
hence meet F is anti-discrete by A1, A2, Th5, Th8; ::_thesis: verum
end;
end;
end;
end;
definition
let Y be TopStruct ;
let x be Point of Y;
func MaxADSF x -> Subset-Family of Y equals :: TEX_4:def 6
{ A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;
coherence
{ A where A is Subset of Y : ( A is anti-discrete & x in A ) } is Subset-Family of Y
proof
set F = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;
{ A where A is Subset of Y : ( A is anti-discrete & x in A ) } c= bool the carrier of Y
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } or C in bool the carrier of Y )
assume C in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ; ::_thesis: C in bool the carrier of Y
then ex A being Subset of Y st
( C = A & A is anti-discrete & x in A ) ;
hence C in bool the carrier of Y ; ::_thesis: verum
end;
hence { A where A is Subset of Y : ( A is anti-discrete & x in A ) } is Subset-Family of Y ; ::_thesis: verum
end;
end;
:: deftheorem defines MaxADSF TEX_4:def_6_:_
for Y being TopStruct
for x being Point of Y holds MaxADSF x = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;
registration
let Y be non empty TopStruct ;
let x be Point of Y;
cluster MaxADSF x -> non empty ;
coherence
not MaxADSF x is empty
proof
set F = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;
A1: x in {x} by TARSKI:def_1;
{x} is anti-discrete by Th6;
then {x} in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } by A1;
hence not MaxADSF x is empty ; ::_thesis: verum
end;
end;
theorem Th10: :: TEX_4:10
for Y being non empty TopStruct
for x being Point of Y holds MaxADSF x is anti-discrete-set-family
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds MaxADSF x is anti-discrete-set-family
let x be Point of Y; ::_thesis: MaxADSF x is anti-discrete-set-family
now__::_thesis:_for_A_being_Subset_of_Y_st_A_in_MaxADSF_x_holds_
A_is_anti-discrete
let A be Subset of Y; ::_thesis: ( A in MaxADSF x implies A is anti-discrete )
assume A in MaxADSF x ; ::_thesis: A is anti-discrete
then ex C being Subset of Y st
( C = A & C is anti-discrete & x in C ) ;
hence A is anti-discrete ; ::_thesis: verum
end;
hence MaxADSF x is anti-discrete-set-family by Def5; ::_thesis: verum
end;
theorem Th11: :: TEX_4:11
for Y being non empty TopStruct
for x being Point of Y holds {x} = meet (MaxADSF x)
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds {x} = meet (MaxADSF x)
let x be Point of Y; ::_thesis: {x} = meet (MaxADSF x)
A1: x in {x} by TARSKI:def_1;
now__::_thesis:_for_A_being_set_st_A_in_MaxADSF_x_holds_
{x}_c=_A
let A be set ; ::_thesis: ( A in MaxADSF x implies {x} c= A )
assume A in MaxADSF x ; ::_thesis: {x} c= A
then ex C being Subset of Y st
( C = A & C is anti-discrete & x in C ) ;
hence {x} c= A by ZFMISC_1:31; ::_thesis: verum
end;
then A2: {x} c= meet (MaxADSF x) by SETFAM_1:5;
{x} is anti-discrete by Th6;
then {x} in MaxADSF x by A1;
then meet (MaxADSF x) c= {x} by SETFAM_1:3;
hence {x} = meet (MaxADSF x) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th12: :: TEX_4:12
for Y being non empty TopStruct
for x being Point of Y holds {x} c= union (MaxADSF x)
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds {x} c= union (MaxADSF x)
let x be Point of Y; ::_thesis: {x} c= union (MaxADSF x)
{x} = meet (MaxADSF x) by Th11;
hence {x} c= union (MaxADSF x) by SETFAM_1:2; ::_thesis: verum
end;
theorem Th13: :: TEX_4:13
for Y being non empty TopStruct
for x being Point of Y holds union (MaxADSF x) is anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds union (MaxADSF x) is anti-discrete
let x be Point of Y; ::_thesis: union (MaxADSF x) is anti-discrete
{x} = meet (MaxADSF x) by Th11;
hence union (MaxADSF x) is anti-discrete by Th8, Th10; ::_thesis: verum
end;
begin
definition
let Y be TopStruct ;
let IT be Subset of Y;
attrIT is maximal_anti-discrete means :Def7: :: TEX_4:def 7
( IT is anti-discrete & ( for D being Subset of Y st D is anti-discrete & IT c= D holds
IT = D ) );
end;
:: deftheorem Def7 defines maximal_anti-discrete TEX_4:def_7_:_
for Y being TopStruct
for IT being Subset of Y holds
( IT is maximal_anti-discrete iff ( IT is anti-discrete & ( for D being Subset of Y st D is anti-discrete & IT c= D holds
IT = D ) ) );
theorem :: TEX_4:14
for Y0, Y1 being TopStruct
for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_anti-discrete holds
D1 is maximal_anti-discrete
proof
let Y0, Y1 be TopStruct ; ::_thesis: for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_anti-discrete holds
D1 is maximal_anti-discrete
let D0 be Subset of Y0; ::_thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_anti-discrete holds
D1 is maximal_anti-discrete
let D1 be Subset of Y1; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_anti-discrete implies D1 is maximal_anti-discrete )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not D0 = D1 or not D0 is maximal_anti-discrete or D1 is maximal_anti-discrete )
assume A2: D0 = D1 ; ::_thesis: ( not D0 is maximal_anti-discrete or D1 is maximal_anti-discrete )
assume A3: D0 is maximal_anti-discrete ; ::_thesis: D1 is maximal_anti-discrete
A4: now__::_thesis:_for_D_being_Subset_of_Y1_st_D_is_anti-discrete_&_D1_c=_D_holds_
D1_=_D
let D be Subset of Y1; ::_thesis: ( D is anti-discrete & D1 c= D implies D1 = D )
reconsider E = D as Subset of Y0 by A1;
assume D is anti-discrete ; ::_thesis: ( D1 c= D implies D1 = D )
then A5: E is anti-discrete by A1, Th4;
assume D1 c= D ; ::_thesis: D1 = D
hence D1 = D by A2, A3, A5, Def7; ::_thesis: verum
end;
D0 is anti-discrete by A3, Def7;
then D1 is anti-discrete by A1, A2, Th4;
hence D1 is maximal_anti-discrete by A4, Def7; ::_thesis: verum
end;
theorem Th15: :: TEX_4:15
for Y being non empty TopStruct
for A being empty Subset of Y holds not A is maximal_anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for A being empty Subset of Y holds not A is maximal_anti-discrete
consider a being set such that
A1: a in the carrier of Y by XBOOLE_0:def_1;
reconsider a = a as Point of Y by A1;
let A be empty Subset of Y; ::_thesis: not A is maximal_anti-discrete
now__::_thesis:_ex_C_being_Element_of_bool_the_carrier_of_Y_st_
(_C_is_anti-discrete_&_A_c=_C_&_A_<>_C_)
take C = {a}; ::_thesis: ( C is anti-discrete & A c= C & A <> C )
thus ( C is anti-discrete & A c= C & A <> C ) by Th6, XBOOLE_1:2; ::_thesis: verum
end;
hence not A is maximal_anti-discrete by Def7; ::_thesis: verum
end;
theorem Th16: :: TEX_4:16
for Y being non empty TopStruct
for A being non empty Subset of Y st A is anti-discrete & A is open holds
A is maximal_anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y st A is anti-discrete & A is open holds
A is maximal_anti-discrete
let A be non empty Subset of Y; ::_thesis: ( A is anti-discrete & A is open implies A is maximal_anti-discrete )
assume A1: A is anti-discrete ; ::_thesis: ( not A is open or A is maximal_anti-discrete )
assume A2: A is open ; ::_thesis: A is maximal_anti-discrete
for D being Subset of Y st D is anti-discrete & A c= D holds
A = D
proof
let D be Subset of Y; ::_thesis: ( D is anti-discrete & A c= D implies A = D )
assume D is anti-discrete ; ::_thesis: ( not A c= D or A = D )
then ( D misses A or D c= A ) by A2, Def3;
then A3: ( D /\ A = {} or D c= A ) by XBOOLE_0:def_7;
assume A c= D ; ::_thesis: A = D
hence A = D by A3, XBOOLE_0:def_10, XBOOLE_1:28; ::_thesis: verum
end;
hence A is maximal_anti-discrete by A1, Def7; ::_thesis: verum
end;
theorem Th17: :: TEX_4:17
for Y being non empty TopStruct
for A being non empty Subset of Y st A is anti-discrete & A is closed holds
A is maximal_anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y st A is anti-discrete & A is closed holds
A is maximal_anti-discrete
let A be non empty Subset of Y; ::_thesis: ( A is anti-discrete & A is closed implies A is maximal_anti-discrete )
assume A1: A is anti-discrete ; ::_thesis: ( not A is closed or A is maximal_anti-discrete )
assume A2: A is closed ; ::_thesis: A is maximal_anti-discrete
for D being Subset of Y st D is anti-discrete & A c= D holds
A = D
proof
let D be Subset of Y; ::_thesis: ( D is anti-discrete & A c= D implies A = D )
assume D is anti-discrete ; ::_thesis: ( not A c= D or A = D )
then ( D misses A or D c= A ) by A2, Def4;
then A3: ( D /\ A = {} or D c= A ) by XBOOLE_0:def_7;
assume A c= D ; ::_thesis: A = D
hence A = D by A3, XBOOLE_0:def_10, XBOOLE_1:28; ::_thesis: verum
end;
hence A is maximal_anti-discrete by A1, Def7; ::_thesis: verum
end;
definition
let Y be TopStruct ;
let x be Point of Y;
func MaxADSet x -> Subset of Y equals :: TEX_4:def 8
union (MaxADSF x);
coherence
union (MaxADSF x) is Subset of Y ;
end;
:: deftheorem defines MaxADSet TEX_4:def_8_:_
for Y being TopStruct
for x being Point of Y holds MaxADSet x = union (MaxADSF x);
registration
let Y be non empty TopStruct ;
let x be Point of Y;
cluster MaxADSet x -> non empty ;
coherence
not MaxADSet x is empty
proof
{x} c= union (MaxADSF x) by Th12;
hence not MaxADSet x is empty ; ::_thesis: verum
end;
end;
theorem :: TEX_4:18
for Y being non empty TopStruct
for x being Point of Y holds {x} c= MaxADSet x by Th12;
theorem Th19: :: TEX_4:19
for Y being non empty TopStruct
for D being Subset of Y
for x being Point of Y st D is anti-discrete & x in D holds
D c= MaxADSet x
proof
let Y be non empty TopStruct ; ::_thesis: for D being Subset of Y
for x being Point of Y st D is anti-discrete & x in D holds
D c= MaxADSet x
let D be Subset of Y; ::_thesis: for x being Point of Y st D is anti-discrete & x in D holds
D c= MaxADSet x
let x be Point of Y; ::_thesis: ( D is anti-discrete & x in D implies D c= MaxADSet x )
assume A1: D is anti-discrete ; ::_thesis: ( not x in D or D c= MaxADSet x )
assume x in D ; ::_thesis: D c= MaxADSet x
then D in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } by A1;
hence D c= MaxADSet x by ZFMISC_1:74; ::_thesis: verum
end;
theorem Th20: :: TEX_4:20
for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x is maximal_anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds MaxADSet x is maximal_anti-discrete
let x be Point of Y; ::_thesis: MaxADSet x is maximal_anti-discrete
A1: for D being Subset of Y st D is anti-discrete & MaxADSet x c= D holds
MaxADSet x = D
proof
let D be Subset of Y; ::_thesis: ( D is anti-discrete & MaxADSet x c= D implies MaxADSet x = D )
assume A2: D is anti-discrete ; ::_thesis: ( not MaxADSet x c= D or MaxADSet x = D )
assume A3: MaxADSet x c= D ; ::_thesis: MaxADSet x = D
{x} c= MaxADSet x by Th12;
then {x} c= D by A3, XBOOLE_1:1;
then x in D by ZFMISC_1:31;
then D c= MaxADSet x by A2, Th19;
hence MaxADSet x = D by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
MaxADSet x is anti-discrete by Th13;
hence MaxADSet x is maximal_anti-discrete by A1, Def7; ::_thesis: verum
end;
theorem Th21: :: TEX_4:21
for Y being non empty TopStruct
for x, y being Point of Y holds
( y in MaxADSet x iff MaxADSet y = MaxADSet x )
proof
let Y be non empty TopStruct ; ::_thesis: for x, y being Point of Y holds
( y in MaxADSet x iff MaxADSet y = MaxADSet x )
let x, y be Point of Y; ::_thesis: ( y in MaxADSet x iff MaxADSet y = MaxADSet x )
MaxADSet y is maximal_anti-discrete by Th20;
then A1: MaxADSet y is anti-discrete by Def7;
A2: MaxADSet x is maximal_anti-discrete by Th20;
then A3: MaxADSet x is anti-discrete by Def7;
thus ( y in MaxADSet x implies MaxADSet y = MaxADSet x ) ::_thesis: ( MaxADSet y = MaxADSet x implies y in MaxADSet x )
proof
assume y in MaxADSet x ; ::_thesis: MaxADSet y = MaxADSet x
then MaxADSet x in { A where A is Subset of Y : ( A is anti-discrete & y in A ) } by A3;
then MaxADSet x c= MaxADSet y by ZFMISC_1:74;
hence MaxADSet y = MaxADSet x by A2, A1, Def7; ::_thesis: verum
end;
assume A4: MaxADSet y = MaxADSet x ; ::_thesis: y in MaxADSet x
{y} c= MaxADSet y by Th12;
hence y in MaxADSet x by A4, ZFMISC_1:31; ::_thesis: verum
end;
theorem Th22: :: TEX_4:22
for Y being non empty TopStruct
for x, y being Point of Y holds
( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y )
proof
let Y be non empty TopStruct ; ::_thesis: for x, y being Point of Y holds
( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y )
let x, y be Point of Y; ::_thesis: ( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y )
assume (MaxADSet x) /\ (MaxADSet y) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: MaxADSet x = MaxADSet y
then consider a being set such that
A1: a in (MaxADSet x) /\ (MaxADSet y) by XBOOLE_0:def_1;
reconsider a = a as Point of Y by A1;
a in MaxADSet x by A1, XBOOLE_0:def_4;
then A2: MaxADSet a = MaxADSet x by Th21;
a in MaxADSet y by A1, XBOOLE_0:def_4;
hence MaxADSet x = MaxADSet y by A2, Th21; ::_thesis: verum
end;
theorem Th23: :: TEX_4:23
for Y being non empty TopStruct
for F being Subset of Y
for x being Point of Y st F is closed & x in F holds
MaxADSet x c= F
proof
let Y be non empty TopStruct ; ::_thesis: for F being Subset of Y
for x being Point of Y st F is closed & x in F holds
MaxADSet x c= F
let F be Subset of Y; ::_thesis: for x being Point of Y st F is closed & x in F holds
MaxADSet x c= F
let x be Point of Y; ::_thesis: ( F is closed & x in F implies MaxADSet x c= F )
assume that
A1: F is closed and
A2: x in F ; ::_thesis: MaxADSet x c= F
{x} c= MaxADSet x by Th12;
then A3: x in MaxADSet x by ZFMISC_1:31;
MaxADSet x is maximal_anti-discrete by Th20;
then MaxADSet x is anti-discrete by Def7;
hence MaxADSet x c= F by A1, A2, A3, Def2; ::_thesis: verum
end;
theorem Th24: :: TEX_4:24
for Y being non empty TopStruct
for G being Subset of Y
for x being Point of Y st G is open & x in G holds
MaxADSet x c= G
proof
let Y be non empty TopStruct ; ::_thesis: for G being Subset of Y
for x being Point of Y st G is open & x in G holds
MaxADSet x c= G
let G be Subset of Y; ::_thesis: for x being Point of Y st G is open & x in G holds
MaxADSet x c= G
let x be Point of Y; ::_thesis: ( G is open & x in G implies MaxADSet x c= G )
assume that
A1: G is open and
A2: x in G ; ::_thesis: MaxADSet x c= G
{x} c= MaxADSet x by Th12;
then A3: x in MaxADSet x by ZFMISC_1:31;
MaxADSet x is maximal_anti-discrete by Th20;
then MaxADSet x is anti-discrete by Def7;
hence MaxADSet x c= G by A1, A2, A3, Def1; ::_thesis: verum
end;
theorem :: TEX_4:25
for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) }
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) }
let x be Point of Y; ::_thesis: MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) }
set G = { F where F is Subset of Y : ( F is closed & x in F ) } ;
{ F where F is Subset of Y : ( F is closed & x in F ) } c= bool the carrier of Y
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { F where F is Subset of Y : ( F is closed & x in F ) } or C in bool the carrier of Y )
assume C in { F where F is Subset of Y : ( F is closed & x in F ) } ; ::_thesis: C in bool the carrier of Y
then ex P being Subset of Y st
( C = P & P is closed & x in P ) ;
hence C in bool the carrier of Y ; ::_thesis: verum
end;
then reconsider G = { F where F is Subset of Y : ( F is closed & x in F ) } as Subset-Family of Y ;
now__::_thesis:_for_C_being_set_st_C_in_G_holds_
MaxADSet_x_c=_C
let C be set ; ::_thesis: ( C in G implies MaxADSet x c= C )
assume C in G ; ::_thesis: MaxADSet x c= C
then ex F being Subset of Y st
( F = C & F is closed & x in F ) ;
hence MaxADSet x c= C by Th23; ::_thesis: verum
end;
hence MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) } by SETFAM_1:5; ::_thesis: verum
end;
theorem :: TEX_4:26
for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) }
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) }
let x be Point of Y; ::_thesis: MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) }
set F = { G where G is Subset of Y : ( G is open & x in G ) } ;
{ G where G is Subset of Y : ( G is open & x in G ) } c= bool the carrier of Y
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of Y : ( G is open & x in G ) } or C in bool the carrier of Y )
assume C in { G where G is Subset of Y : ( G is open & x in G ) } ; ::_thesis: C in bool the carrier of Y
then ex P being Subset of Y st
( C = P & P is open & x in P ) ;
hence C in bool the carrier of Y ; ::_thesis: verum
end;
then reconsider F = { G where G is Subset of Y : ( G is open & x in G ) } as Subset-Family of Y ;
now__::_thesis:_for_C_being_set_st_C_in_F_holds_
MaxADSet_x_c=_C
let C be set ; ::_thesis: ( C in F implies MaxADSet x c= C )
assume C in F ; ::_thesis: MaxADSet x c= C
then ex G being Subset of Y st
( G = C & G is open & x in G ) ;
hence MaxADSet x c= C by Th24; ::_thesis: verum
end;
hence MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) } by SETFAM_1:5; ::_thesis: verum
end;
definition
let Y be non empty TopStruct ;
let A be Subset of Y;
redefine attr A is maximal_anti-discrete means :Def9: :: TEX_4:def 9
ex x being Point of Y st
( x in A & A = MaxADSet x );
compatibility
( A is maximal_anti-discrete iff ex x being Point of Y st
( x in A & A = MaxADSet x ) )
proof
thus ( A is maximal_anti-discrete implies ex x being Point of Y st
( x in A & A = MaxADSet x ) ) ::_thesis: ( ex x being Point of Y st
( x in A & A = MaxADSet x ) implies A is maximal_anti-discrete )
proof
assume A1: A is maximal_anti-discrete ; ::_thesis: ex x being Point of Y st
( x in A & A = MaxADSet x )
then A <> {} by Th15;
then consider x being set such that
A2: x in A by XBOOLE_0:def_1;
reconsider x = x as Point of Y by A2;
take x ; ::_thesis: ( x in A & A = MaxADSet x )
thus x in A by A2; ::_thesis: A = MaxADSet x
MaxADSet x is maximal_anti-discrete by Th20;
then A3: MaxADSet x is anti-discrete by Def7;
A is anti-discrete by A1, Def7;
then A c= MaxADSet x by A2, Th19;
hence A = MaxADSet x by A1, A3, Def7; ::_thesis: verum
end;
assume ex x being Point of Y st
( x in A & A = MaxADSet x ) ; ::_thesis: A is maximal_anti-discrete
hence A is maximal_anti-discrete by Th20; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines maximal_anti-discrete TEX_4:def_9_:_
for Y being non empty TopStruct
for A being Subset of Y holds
( A is maximal_anti-discrete iff ex x being Point of Y st
( x in A & A = MaxADSet x ) );
theorem Th27: :: TEX_4:27
for Y being non empty TopStruct
for A being Subset of Y
for x being Point of Y st x in A & A is maximal_anti-discrete holds
A = MaxADSet x
proof
let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y
for x being Point of Y st x in A & A is maximal_anti-discrete holds
A = MaxADSet x
let A be Subset of Y; ::_thesis: for x being Point of Y st x in A & A is maximal_anti-discrete holds
A = MaxADSet x
let x be Point of Y; ::_thesis: ( x in A & A is maximal_anti-discrete implies A = MaxADSet x )
assume A1: x in A ; ::_thesis: ( not A is maximal_anti-discrete or A = MaxADSet x )
assume A is maximal_anti-discrete ; ::_thesis: A = MaxADSet x
then ex y being Point of Y st
( y in A & A = MaxADSet y ) by Def9;
hence A = MaxADSet x by A1, Th21; ::_thesis: verum
end;
definition
let Y be non empty TopStruct ;
let A be non empty Subset of Y;
redefine attr A is maximal_anti-discrete means :: TEX_4:def 10
for x being Point of Y st x in A holds
A = MaxADSet x;
compatibility
( A is maximal_anti-discrete iff for x being Point of Y st x in A holds
A = MaxADSet x )
proof
thus ( A is maximal_anti-discrete implies for x being Point of Y st x in A holds
A = MaxADSet x ) by Th27; ::_thesis: ( ( for x being Point of Y st x in A holds
A = MaxADSet x ) implies A is maximal_anti-discrete )
consider a being set such that
A1: a in A by XBOOLE_0:def_1;
reconsider a = a as Point of Y by A1;
assume A2: for x being Point of Y st x in A holds
A = MaxADSet x ; ::_thesis: A is maximal_anti-discrete
now__::_thesis:_ex_a_being_Point_of_Y_st_
(_a_in_A_&_A_=_MaxADSet_a_)
take a = a; ::_thesis: ( a in A & A = MaxADSet a )
thus a in A by A1; ::_thesis: A = MaxADSet a
thus A = MaxADSet a by A2, A1; ::_thesis: verum
end;
hence A is maximal_anti-discrete by Def9; ::_thesis: verum
end;
end;
:: deftheorem defines maximal_anti-discrete TEX_4:def_10_:_
for Y being non empty TopStruct
for A being non empty Subset of Y holds
( A is maximal_anti-discrete iff for x being Point of Y st x in A holds
A = MaxADSet x );
definition
let Y be non empty TopStruct ;
let A be Subset of Y;
func MaxADSet A -> Subset of Y equals :: TEX_4:def 11
union { (MaxADSet a) where a is Point of Y : a in A } ;
coherence
union { (MaxADSet a) where a is Point of Y : a in A } is Subset of Y
proof
set M = { (MaxADSet a) where a is Point of Y : a in A } ;
{ (MaxADSet a) where a is Point of Y : a in A } c= bool the carrier of Y
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { (MaxADSet a) where a is Point of Y : a in A } or C in bool the carrier of Y )
assume C in { (MaxADSet a) where a is Point of Y : a in A } ; ::_thesis: C in bool the carrier of Y
then ex a being Point of Y st
( C = MaxADSet a & a in A ) ;
hence C in bool the carrier of Y ; ::_thesis: verum
end;
then reconsider M = { (MaxADSet a) where a is Point of Y : a in A } as Subset-Family of Y ;
union M is Subset of Y ;
hence union { (MaxADSet a) where a is Point of Y : a in A } is Subset of Y ; ::_thesis: verum
end;
end;
:: deftheorem defines MaxADSet TEX_4:def_11_:_
for Y being non empty TopStruct
for A being Subset of Y holds MaxADSet A = union { (MaxADSet a) where a is Point of Y : a in A } ;
theorem Th28: :: TEX_4:28
for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x = MaxADSet {x}
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds MaxADSet x = MaxADSet {x}
let x be Point of Y; ::_thesis: MaxADSet x = MaxADSet {x}
set M = { (MaxADSet a) where a is Point of Y : a in {x} } ;
now__::_thesis:_for_P_being_set_st_P_in__{__(MaxADSet_a)_where_a_is_Point_of_Y_:_a_in_{x}__}__holds_
P_c=_MaxADSet_x
let P be set ; ::_thesis: ( P in { (MaxADSet a) where a is Point of Y : a in {x} } implies P c= MaxADSet x )
assume P in { (MaxADSet a) where a is Point of Y : a in {x} } ; ::_thesis: P c= MaxADSet x
then ex a being Point of Y st
( P = MaxADSet a & a in {x} ) ;
hence P c= MaxADSet x by TARSKI:def_1; ::_thesis: verum
end;
then A1: MaxADSet {x} c= MaxADSet x by ZFMISC_1:76;
x in {x} by TARSKI:def_1;
then MaxADSet x in { (MaxADSet a) where a is Point of Y : a in {x} } ;
then MaxADSet x c= MaxADSet {x} by ZFMISC_1:74;
hence MaxADSet x = MaxADSet {x} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th29: :: TEX_4:29
for Y being non empty TopStruct
for A being Subset of Y
for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x meets A
proof
let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y
for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x meets A
let A be Subset of Y; ::_thesis: for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x meets A
let x be Point of Y; ::_thesis: ( MaxADSet x meets MaxADSet A implies MaxADSet x meets A )
set E = { (MaxADSet a) where a is Point of Y : a in A } ;
assume (MaxADSet x) /\ (MaxADSet A) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: MaxADSet x meets A
then consider z being set such that
A1: z in (MaxADSet x) /\ (MaxADSet A) by XBOOLE_0:def_1;
reconsider z = z as Point of Y by A1;
z in MaxADSet A by A1, XBOOLE_0:def_4;
then consider C being set such that
A2: z in C and
A3: C in { (MaxADSet a) where a is Point of Y : a in A } by TARSKI:def_4;
z in MaxADSet x by A1, XBOOLE_0:def_4;
then A4: MaxADSet z = MaxADSet x by Th21;
consider b being Point of Y such that
A5: C = MaxADSet b and
A6: b in A by A3;
MaxADSet b = MaxADSet z by A2, A5, Th21;
then {b} c= MaxADSet x by A4, Th12;
then b in MaxADSet x by ZFMISC_1:31;
hence MaxADSet x meets A by A6, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th30: :: TEX_4:30
for Y being non empty TopStruct
for A being Subset of Y
for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x c= MaxADSet A
proof
let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y
for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x c= MaxADSet A
let A be Subset of Y; ::_thesis: for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x c= MaxADSet A
let x be Point of Y; ::_thesis: ( MaxADSet x meets MaxADSet A implies MaxADSet x c= MaxADSet A )
set F = { (MaxADSet b) where b is Point of Y : b in A } ;
assume MaxADSet x meets MaxADSet A ; ::_thesis: MaxADSet x c= MaxADSet A
then MaxADSet x meets A by Th29;
then consider z being set such that
A1: z in (MaxADSet x) /\ A by XBOOLE_0:4;
reconsider z = z as Point of Y by A1;
set E = { (MaxADSet a) where a is Point of Y : a in {z} } ;
z in A by A1, XBOOLE_0:def_4;
then A2: {z} c= A by ZFMISC_1:31;
{ (MaxADSet a) where a is Point of Y : a in {z} } c= { (MaxADSet b) where b is Point of Y : b in A }
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { (MaxADSet a) where a is Point of Y : a in {z} } or C in { (MaxADSet b) where b is Point of Y : b in A } )
assume C in { (MaxADSet a) where a is Point of Y : a in {z} } ; ::_thesis: C in { (MaxADSet b) where b is Point of Y : b in A }
then ex a being Point of Y st
( C = MaxADSet a & a in {z} ) ;
hence C in { (MaxADSet b) where b is Point of Y : b in A } by A2; ::_thesis: verum
end;
then MaxADSet {z} c= MaxADSet A by ZFMISC_1:77;
then A3: MaxADSet z c= MaxADSet A by Th28;
z in MaxADSet x by A1, XBOOLE_0:def_4;
hence MaxADSet x c= MaxADSet A by A3, Th21; ::_thesis: verum
end;
theorem Th31: :: TEX_4:31
for Y being non empty TopStruct
for A, B being Subset of Y st A c= B holds
MaxADSet A c= MaxADSet B
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st A c= B holds
MaxADSet A c= MaxADSet B
let A, B be Subset of Y; ::_thesis: ( A c= B implies MaxADSet A c= MaxADSet B )
set E = { (MaxADSet a) where a is Point of Y : a in A } ;
set F = { (MaxADSet b) where b is Point of Y : b in B } ;
assume A1: A c= B ; ::_thesis: MaxADSet A c= MaxADSet B
{ (MaxADSet a) where a is Point of Y : a in A } c= { (MaxADSet b) where b is Point of Y : b in B }
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { (MaxADSet a) where a is Point of Y : a in A } or C in { (MaxADSet b) where b is Point of Y : b in B } )
assume C in { (MaxADSet a) where a is Point of Y : a in A } ; ::_thesis: C in { (MaxADSet b) where b is Point of Y : b in B }
then ex a being Point of Y st
( C = MaxADSet a & a in A ) ;
hence C in { (MaxADSet b) where b is Point of Y : b in B } by A1; ::_thesis: verum
end;
hence MaxADSet A c= MaxADSet B by ZFMISC_1:77; ::_thesis: verum
end;
theorem Th32: :: TEX_4:32
for Y being non empty TopStruct
for A being Subset of Y holds A c= MaxADSet A
proof
let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y holds A c= MaxADSet A
let A be Subset of Y; ::_thesis: A c= MaxADSet A
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_in_MaxADSet_A
let x be set ; ::_thesis: ( x in A implies x in MaxADSet A )
assume A1: x in A ; ::_thesis: x in MaxADSet A
then reconsider a = x as Point of Y ;
{a} c= A by A1, ZFMISC_1:31;
then MaxADSet {a} c= MaxADSet A by Th31;
then A2: MaxADSet a c= MaxADSet A by Th28;
A3: a in {a} by TARSKI:def_1;
{a} c= MaxADSet a by Th12;
then {a} c= MaxADSet A by A2, XBOOLE_1:1;
hence x in MaxADSet A by A3; ::_thesis: verum
end;
hence A c= MaxADSet A by TARSKI:def_3; ::_thesis: verum
end;
theorem Th33: :: TEX_4:33
for Y being non empty TopStruct
for A being Subset of Y holds MaxADSet A = MaxADSet (MaxADSet A)
proof
let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y holds MaxADSet A = MaxADSet (MaxADSet A)
let A be Subset of Y; ::_thesis: MaxADSet A = MaxADSet (MaxADSet A)
A1: MaxADSet (MaxADSet A) c= MaxADSet A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MaxADSet (MaxADSet A) or x in MaxADSet A )
assume x in MaxADSet (MaxADSet A) ; ::_thesis: x in MaxADSet A
then consider C being set such that
A2: x in C and
A3: C in { (MaxADSet a) where a is Point of Y : a in MaxADSet A } by TARSKI:def_4;
consider a being Point of Y such that
A4: C = MaxADSet a and
A5: a in MaxADSet A by A3;
consider D being set such that
A6: a in D and
A7: D in { (MaxADSet b) where b is Point of Y : b in A } by A5, TARSKI:def_4;
consider b being Point of Y such that
A8: D = MaxADSet b and
b in A by A7;
MaxADSet a = MaxADSet b by A6, A8, Th21;
hence x in MaxADSet A by A2, A4, A7, A8, TARSKI:def_4; ::_thesis: verum
end;
MaxADSet A c= MaxADSet (MaxADSet A) by Th32;
hence MaxADSet A = MaxADSet (MaxADSet A) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th34: :: TEX_4:34
for Y being non empty TopStruct
for A, B being Subset of Y st A c= MaxADSet B holds
MaxADSet A c= MaxADSet B
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st A c= MaxADSet B holds
MaxADSet A c= MaxADSet B
let A, B be Subset of Y; ::_thesis: ( A c= MaxADSet B implies MaxADSet A c= MaxADSet B )
assume A c= MaxADSet B ; ::_thesis: MaxADSet A c= MaxADSet B
then MaxADSet A c= MaxADSet (MaxADSet B) by Th31;
hence MaxADSet A c= MaxADSet B by Th33; ::_thesis: verum
end;
theorem Th35: :: TEX_4:35
for Y being non empty TopStruct
for A, B being Subset of Y st B c= MaxADSet A & A c= MaxADSet B holds
MaxADSet A = MaxADSet B
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st B c= MaxADSet A & A c= MaxADSet B holds
MaxADSet A = MaxADSet B
let A, B be Subset of Y; ::_thesis: ( B c= MaxADSet A & A c= MaxADSet B implies MaxADSet A = MaxADSet B )
thus ( B c= MaxADSet A & A c= MaxADSet B implies MaxADSet A = MaxADSet B ) ::_thesis: verum
proof
assume that
A1: B c= MaxADSet A and
A2: A c= MaxADSet B ; ::_thesis: MaxADSet A = MaxADSet B
A3: MaxADSet A c= MaxADSet B by A2, Th34;
MaxADSet B c= MaxADSet A by A1, Th34;
hence MaxADSet A = MaxADSet B by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
theorem :: TEX_4:36
for Y being non empty TopStruct
for A, B being Subset of Y holds MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B)
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y holds MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B)
let A, B be Subset of Y; ::_thesis: MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B)
A1: MaxADSet (A \/ B) c= (MaxADSet A) \/ (MaxADSet B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MaxADSet (A \/ B) or x in (MaxADSet A) \/ (MaxADSet B) )
assume x in MaxADSet (A \/ B) ; ::_thesis: x in (MaxADSet A) \/ (MaxADSet B)
then consider C being set such that
A2: x in C and
A3: C in { (MaxADSet a) where a is Point of Y : a in A \/ B } by TARSKI:def_4;
consider a being Point of Y such that
A4: C = MaxADSet a and
A5: a in A \/ B by A3;
now__::_thesis:_x_in_(MaxADSet_A)_\/_(MaxADSet_B)
percases ( a in A or a in B ) by A5, XBOOLE_0:def_3;
supposeA6: a in A ; ::_thesis: x in (MaxADSet A) \/ (MaxADSet B)
now__::_thesis:_ex_C_being_set_st_
(_x_in_C_&_C_in__{__(MaxADSet_c)_where_c_is_Point_of_Y_:_c_in_A__}__)
take C = C; ::_thesis: ( x in C & C in { (MaxADSet c) where c is Point of Y : c in A } )
thus x in C by A2; ::_thesis: C in { (MaxADSet c) where c is Point of Y : c in A }
thus C in { (MaxADSet c) where c is Point of Y : c in A } by A4, A6; ::_thesis: verum
end;
then A7: x in MaxADSet A by TARSKI:def_4;
MaxADSet A c= (MaxADSet A) \/ (MaxADSet B) by XBOOLE_1:7;
hence x in (MaxADSet A) \/ (MaxADSet B) by A7; ::_thesis: verum
end;
supposeA8: a in B ; ::_thesis: x in (MaxADSet A) \/ (MaxADSet B)
now__::_thesis:_ex_C_being_set_st_
(_x_in_C_&_C_in__{__(MaxADSet_c)_where_c_is_Point_of_Y_:_c_in_B__}__)
take C = C; ::_thesis: ( x in C & C in { (MaxADSet c) where c is Point of Y : c in B } )
thus x in C by A2; ::_thesis: C in { (MaxADSet c) where c is Point of Y : c in B }
thus C in { (MaxADSet c) where c is Point of Y : c in B } by A4, A8; ::_thesis: verum
end;
then A9: x in MaxADSet B by TARSKI:def_4;
MaxADSet B c= (MaxADSet A) \/ (MaxADSet B) by XBOOLE_1:7;
hence x in (MaxADSet A) \/ (MaxADSet B) by A9; ::_thesis: verum
end;
end;
end;
hence x in (MaxADSet A) \/ (MaxADSet B) ; ::_thesis: verum
end;
A10: MaxADSet B c= MaxADSet (A \/ B) by Th31, XBOOLE_1:7;
MaxADSet A c= MaxADSet (A \/ B) by Th31, XBOOLE_1:7;
then (MaxADSet A) \/ (MaxADSet B) c= MaxADSet (A \/ B) by A10, XBOOLE_1:8;
hence MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th37: :: TEX_4:37
for Y being non empty TopStruct
for A, B being Subset of Y holds MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B)
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y holds MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B)
let A, B be Subset of Y; ::_thesis: MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B)
A1: MaxADSet (A /\ B) c= MaxADSet B by Th31, XBOOLE_1:17;
MaxADSet (A /\ B) c= MaxADSet A by Th31, XBOOLE_1:17;
hence MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B) by A1, XBOOLE_1:19; ::_thesis: verum
end;
registration
let Y be non empty TopStruct ;
let A be non empty Subset of Y;
cluster MaxADSet A -> non empty ;
coherence
not MaxADSet A is empty by Th32, XBOOLE_1:3;
end;
registration
let Y be non empty TopStruct ;
let A be empty Subset of Y;
cluster MaxADSet A -> empty ;
coherence
MaxADSet A is empty
proof
now__::_thesis:_MaxADSet_A_is_empty
assume not MaxADSet A is empty ; ::_thesis: contradiction
then consider x being set such that
A1: x in MaxADSet A by XBOOLE_0:def_1;
reconsider a = x as Point of Y by A1;
consider D being set such that
a in D and
A2: D in { (MaxADSet b) where b is Point of Y : b in A } by A1, TARSKI:def_4;
ex b being Point of Y st
( D = MaxADSet b & b in A ) by A2;
hence contradiction ; ::_thesis: verum
end;
hence MaxADSet A is empty ; ::_thesis: verum
end;
end;
registration
let Y be non empty TopStruct ;
let A be non proper Subset of Y;
cluster MaxADSet A -> non proper ;
coherence
not MaxADSet A is proper
proof
A = the carrier of Y by SUBSET_1:def_6;
then the carrier of Y c= MaxADSet A by Th32;
then MaxADSet A = the carrier of Y by XBOOLE_0:def_10;
hence not MaxADSet A is proper by SUBSET_1:def_6; ::_thesis: verum
end;
end;
registration
let Y be non trivial TopStruct ;
let A be non trivial Subset of Y;
cluster MaxADSet A -> non trivial ;
coherence
not MaxADSet A is trivial
proof
A c= MaxADSet A by Th32;
hence not MaxADSet A is trivial ; ::_thesis: verum
end;
end;
theorem Th38: :: TEX_4:38
for Y being non empty TopStruct
for G, A being Subset of Y st G is open & A c= G holds
MaxADSet A c= G
proof
let Y be non empty TopStruct ; ::_thesis: for G, A being Subset of Y st G is open & A c= G holds
MaxADSet A c= G
let G, A be Subset of Y; ::_thesis: ( G is open & A c= G implies MaxADSet A c= G )
assume A1: G is open ; ::_thesis: ( not A c= G or MaxADSet A c= G )
assume A2: A c= G ; ::_thesis: MaxADSet A c= G
MaxADSet A c= G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MaxADSet A or x in G )
assume A3: x in MaxADSet A ; ::_thesis: x in G
then reconsider a = x as Point of Y ;
consider D being set such that
A4: a in D and
A5: D in { (MaxADSet b) where b is Point of Y : b in A } by A3, TARSKI:def_4;
consider b being Point of Y such that
A6: D = MaxADSet b and
A7: b in A by A5;
A8: MaxADSet a = MaxADSet b by A4, A6, Th21;
A9: {a} c= MaxADSet a by Th12;
MaxADSet b c= G by A1, A2, A7, Th24;
then {a} c= G by A8, A9, XBOOLE_1:1;
hence x in G by ZFMISC_1:31; ::_thesis: verum
end;
hence MaxADSet A c= G ; ::_thesis: verum
end;
theorem Th39: :: TEX_4:39
for Y being non empty TopStruct
for A being Subset of Y st { G where G is Subset of Y : ( G is open & A c= G ) } <> {} holds
MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) }
proof
let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y st { G where G is Subset of Y : ( G is open & A c= G ) } <> {} holds
MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) }
let A be Subset of Y; ::_thesis: ( { G where G is Subset of Y : ( G is open & A c= G ) } <> {} implies MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) } )
set F = { G where G is Subset of Y : ( G is open & A c= G ) } ;
{ G where G is Subset of Y : ( G is open & A c= G ) } c= bool the carrier of Y
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of Y : ( G is open & A c= G ) } or C in bool the carrier of Y )
assume C in { G where G is Subset of Y : ( G is open & A c= G ) } ; ::_thesis: C in bool the carrier of Y
then ex P being Subset of Y st
( C = P & P is open & A c= P ) ;
hence C in bool the carrier of Y ; ::_thesis: verum
end;
then reconsider F = { G where G is Subset of Y : ( G is open & A c= G ) } as Subset-Family of Y ;
A1: now__::_thesis:_for_C_being_set_st_C_in_F_holds_
MaxADSet_A_c=_C
let C be set ; ::_thesis: ( C in F implies MaxADSet A c= C )
assume C in F ; ::_thesis: MaxADSet A c= C
then ex G being Subset of Y st
( G = C & G is open & A c= G ) ;
hence MaxADSet A c= C by Th38; ::_thesis: verum
end;
assume { G where G is Subset of Y : ( G is open & A c= G ) } <> {} ; ::_thesis: MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) }
hence MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) } by A1, SETFAM_1:5; ::_thesis: verum
end;
theorem Th40: :: TEX_4:40
for Y being non empty TopStruct
for F, A being Subset of Y st F is closed & A c= F holds
MaxADSet A c= F
proof
let Y be non empty TopStruct ; ::_thesis: for F, A being Subset of Y st F is closed & A c= F holds
MaxADSet A c= F
let F, A be Subset of Y; ::_thesis: ( F is closed & A c= F implies MaxADSet A c= F )
assume A1: F is closed ; ::_thesis: ( not A c= F or MaxADSet A c= F )
assume A2: A c= F ; ::_thesis: MaxADSet A c= F
MaxADSet A c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MaxADSet A or x in F )
assume A3: x in MaxADSet A ; ::_thesis: x in F
then reconsider a = x as Point of Y ;
consider D being set such that
A4: a in D and
A5: D in { (MaxADSet b) where b is Point of Y : b in A } by A3, TARSKI:def_4;
consider b being Point of Y such that
A6: D = MaxADSet b and
A7: b in A by A5;
A8: MaxADSet a = MaxADSet b by A4, A6, Th21;
A9: {a} c= MaxADSet a by Th12;
MaxADSet b c= F by A1, A2, A7, Th23;
then {a} c= F by A8, A9, XBOOLE_1:1;
hence x in F by ZFMISC_1:31; ::_thesis: verum
end;
hence MaxADSet A c= F ; ::_thesis: verum
end;
theorem Th41: :: TEX_4:41
for Y being non empty TopStruct
for A being Subset of Y st { F where F is Subset of Y : ( F is closed & A c= F ) } <> {} holds
MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) }
proof
let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y st { F where F is Subset of Y : ( F is closed & A c= F ) } <> {} holds
MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) }
let A be Subset of Y; ::_thesis: ( { F where F is Subset of Y : ( F is closed & A c= F ) } <> {} implies MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) } )
set G = { F where F is Subset of Y : ( F is closed & A c= F ) } ;
{ F where F is Subset of Y : ( F is closed & A c= F ) } c= bool the carrier of Y
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { F where F is Subset of Y : ( F is closed & A c= F ) } or C in bool the carrier of Y )
assume C in { F where F is Subset of Y : ( F is closed & A c= F ) } ; ::_thesis: C in bool the carrier of Y
then ex P being Subset of Y st
( C = P & P is closed & A c= P ) ;
hence C in bool the carrier of Y ; ::_thesis: verum
end;
then reconsider G = { F where F is Subset of Y : ( F is closed & A c= F ) } as Subset-Family of Y ;
A1: now__::_thesis:_for_C_being_set_st_C_in_G_holds_
MaxADSet_A_c=_C
let C be set ; ::_thesis: ( C in G implies MaxADSet A c= C )
assume C in G ; ::_thesis: MaxADSet A c= C
then ex F being Subset of Y st
( F = C & F is closed & A c= F ) ;
hence MaxADSet A c= C by Th40; ::_thesis: verum
end;
assume { F where F is Subset of Y : ( F is closed & A c= F ) } <> {} ; ::_thesis: MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) }
hence MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) } by A1, SETFAM_1:5; ::_thesis: verum
end;
begin
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete means :Def12: :: TEX_4:def 12
for x being Point of X st x in A holds
A c= Cl {x};
compatibility
( A is anti-discrete iff for x being Point of X st x in A holds
A c= Cl {x} )
proof
thus ( A is anti-discrete implies for x being Point of X st x in A holds
A c= Cl {x} ) ::_thesis: ( ( for x being Point of X st x in A holds
A c= Cl {x} ) implies A is anti-discrete )
proof
assume A1: A is anti-discrete ; ::_thesis: for x being Point of X st x in A holds
A c= Cl {x}
let x be Point of X; ::_thesis: ( x in A implies A c= Cl {x} )
assume A2: x in A ; ::_thesis: A c= Cl {x}
{x} c= Cl {x} by PRE_TOPC:18;
then A3: x in Cl {x} by ZFMISC_1:31;
( A misses Cl {x} or A c= Cl {x} ) by A1, Def4;
hence A c= Cl {x} by A2, A3, XBOOLE_0:3; ::_thesis: verum
end;
thus ( ( for x being Point of X st x in A holds
A c= Cl {x} ) implies A is anti-discrete ) ::_thesis: verum
proof
assume A4: for x being Point of X st x in A holds
A c= Cl {x} ; ::_thesis: A is anti-discrete
now__::_thesis:_for_F_being_Subset_of_X_st_F_is_closed_&_A_meets_F_holds_
A_c=_F
let F be Subset of X; ::_thesis: ( F is closed & A meets F implies A c= F )
assume A5: F is closed ; ::_thesis: ( A meets F implies A c= F )
assume A meets F ; ::_thesis: A c= F
then consider a being set such that
A6: a in A /\ F by XBOOLE_0:4;
reconsider a = a as Point of X by A6;
a in F by A6, XBOOLE_0:def_4;
then {a} c= F by ZFMISC_1:31;
then A7: Cl {a} c= F by A5, TOPS_1:5;
a in A by A6, XBOOLE_0:def_4;
then A c= Cl {a} by A4;
hence A c= F by A7, XBOOLE_1:1; ::_thesis: verum
end;
hence A is anti-discrete by Def4; ::_thesis: verum
end;
end;
end;
:: deftheorem Def12 defines anti-discrete TEX_4:def_12_:_
for X being non empty TopSpace
for A being Subset of X holds
( A is anti-discrete iff for x being Point of X st x in A holds
A c= Cl {x} );
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete means :: TEX_4:def 13
for x being Point of X st x in A holds
Cl A = Cl {x};
compatibility
( A is anti-discrete iff for x being Point of X st x in A holds
Cl A = Cl {x} )
proof
thus ( A is anti-discrete implies for x being Point of X st x in A holds
Cl A = Cl {x} ) ::_thesis: ( ( for x being Point of X st x in A holds
Cl A = Cl {x} ) implies A is anti-discrete )
proof
assume A1: A is anti-discrete ; ::_thesis: for x being Point of X st x in A holds
Cl A = Cl {x}
let x be Point of X; ::_thesis: ( x in A implies Cl A = Cl {x} )
assume A2: x in A ; ::_thesis: Cl A = Cl {x}
then {x} c= A by ZFMISC_1:31;
then A3: Cl {x} c= Cl A by PRE_TOPC:19;
A c= Cl {x} by A1, A2, Def12;
then Cl A c= Cl {x} by TOPS_1:5;
hence Cl A = Cl {x} by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
assume A4: for x being Point of X st x in A holds
Cl A = Cl {x} ; ::_thesis: A is anti-discrete
now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_holds_
A_c=_Cl_{x}
let x be Point of X; ::_thesis: ( x in A implies A c= Cl {x} )
assume x in A ; ::_thesis: A c= Cl {x}
then Cl A = Cl {x} by A4;
hence A c= Cl {x} by PRE_TOPC:18; ::_thesis: verum
end;
hence A is anti-discrete by Def12; ::_thesis: verum
end;
end;
:: deftheorem defines anti-discrete TEX_4:def_13_:_
for X being non empty TopSpace
for A being Subset of X holds
( A is anti-discrete iff for x being Point of X st x in A holds
Cl A = Cl {x} );
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete means :Def14: :: TEX_4:def 14
for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y};
compatibility
( A is anti-discrete iff for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y} )
proof
thus ( A is anti-discrete implies for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y} ) ::_thesis: ( ( for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y} ) implies A is anti-discrete )
proof
assume A1: A is anti-discrete ; ::_thesis: for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y}
let x, y be Point of X; ::_thesis: ( x in A & y in A implies Cl {x} = Cl {y} )
assume that
A2: x in A and
A3: y in A ; ::_thesis: Cl {x} = Cl {y}
A c= Cl {y} by A1, A3, Def12;
then {x} c= Cl {y} by A2, ZFMISC_1:31;
then A4: Cl {x} c= Cl {y} by TOPS_1:5;
A c= Cl {x} by A1, A2, Def12;
then {y} c= Cl {x} by A3, ZFMISC_1:31;
then Cl {y} c= Cl {x} by TOPS_1:5;
hence Cl {x} = Cl {y} by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
thus ( ( for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y} ) implies A is anti-discrete ) ::_thesis: verum
proof
assume A5: for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y} ; ::_thesis: A is anti-discrete
now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_holds_
A_c=_Cl_{x}
let x be Point of X; ::_thesis: ( x in A implies A c= Cl {x} )
assume A6: x in A ; ::_thesis: A c= Cl {x}
now__::_thesis:_for_a_being_set_st_a_in_A_holds_
a_in_Cl_{x}
let a be set ; ::_thesis: ( a in A implies a in Cl {x} )
assume A7: a in A ; ::_thesis: a in Cl {x}
then reconsider y = a as Point of X ;
{y} c= Cl {y} by PRE_TOPC:18;
then y in Cl {y} by ZFMISC_1:31;
hence a in Cl {x} by A5, A6, A7; ::_thesis: verum
end;
hence A c= Cl {x} by TARSKI:def_3; ::_thesis: verum
end;
hence A is anti-discrete by Def12; ::_thesis: verum
end;
end;
end;
:: deftheorem Def14 defines anti-discrete TEX_4:def_14_:_
for X being non empty TopSpace
for A being Subset of X holds
( A is anti-discrete iff for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y} );
theorem :: TEX_4:42
for X being non empty TopSpace
for x being Point of X
for D being Subset of X st D is anti-discrete & Cl {x} c= D holds
D = Cl {x}
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X
for D being Subset of X st D is anti-discrete & Cl {x} c= D holds
D = Cl {x}
let x be Point of X; ::_thesis: for D being Subset of X st D is anti-discrete & Cl {x} c= D holds
D = Cl {x}
let D be Subset of X; ::_thesis: ( D is anti-discrete & Cl {x} c= D implies D = Cl {x} )
assume D is anti-discrete ; ::_thesis: ( not Cl {x} c= D or D = Cl {x} )
then ( D misses Cl {x} or D c= Cl {x} ) by Def4;
then A1: ( D /\ (Cl {x}) = {} or D c= Cl {x} ) by XBOOLE_0:def_7;
assume Cl {x} c= D ; ::_thesis: D = Cl {x}
hence D = Cl {x} by A1, XBOOLE_0:def_10, XBOOLE_1:28; ::_thesis: verum
end;
theorem :: TEX_4:43
for X being non empty TopSpace
for A being Subset of X holds
( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds
A = Cl {x} )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds
A = Cl {x} )
let A be Subset of X; ::_thesis: ( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds
A = Cl {x} )
thus ( A is anti-discrete & A is closed implies for x being Point of X st x in A holds
A = Cl {x} ) ::_thesis: ( ( for x being Point of X st x in A holds
A = Cl {x} ) implies ( A is anti-discrete & A is closed ) )
proof
assume A1: A is anti-discrete ; ::_thesis: ( not A is closed or for x being Point of X st x in A holds
A = Cl {x} )
assume A2: A is closed ; ::_thesis: for x being Point of X st x in A holds
A = Cl {x}
let x be Point of X; ::_thesis: ( x in A implies A = Cl {x} )
assume A3: x in A ; ::_thesis: A = Cl {x}
then {x} c= A by ZFMISC_1:31;
then A4: Cl {x} c= A by A2, TOPS_1:5;
A c= Cl {x} by A1, A3, Def12;
hence A = Cl {x} by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
thus ( ( for x being Point of X st x in A holds
A = Cl {x} ) implies ( A is anti-discrete & A is closed ) ) ::_thesis: verum
proof
assume A5: for x being Point of X st x in A holds
A = Cl {x} ; ::_thesis: ( A is anti-discrete & A is closed )
then for x being Point of X st x in A holds
A c= Cl {x} ;
hence A is anti-discrete by Def12; ::_thesis: A is closed
hereby ::_thesis: verum
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: A is closed
hence A is closed ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: A is closed
then consider a being set such that
A6: a in A by XBOOLE_0:def_1;
reconsider a = a as Point of X by A6;
A = Cl {a} by A5, A6;
hence A is closed ; ::_thesis: verum
end;
end;
end;
end;
end;
theorem :: TEX_4:44
for X being non empty TopSpace
for A being Subset of X st A is anti-discrete & not A is open holds
A is boundary
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is anti-discrete & not A is open holds
A is boundary
let A be Subset of X; ::_thesis: ( A is anti-discrete & not A is open implies A is boundary )
A1: Int A c= A by TOPS_1:16;
assume A is anti-discrete ; ::_thesis: ( A is open or A is boundary )
then ( A misses Int A or A c= Int A ) by Def3;
then A2: ( A /\ (Int A) = {} or A c= Int A ) by XBOOLE_0:def_7;
assume A3: not A is open ; ::_thesis: A is boundary
assume not A is boundary ; ::_thesis: contradiction
then Int A <> {} by TOPS_1:48;
hence contradiction by A3, A2, A1, XBOOLE_0:def_10, XBOOLE_1:28; ::_thesis: verum
end;
theorem Th45: :: TEX_4:45
for X being non empty TopSpace
for x being Point of X st Cl {x} = {x} holds
{x} is maximal_anti-discrete
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X st Cl {x} = {x} holds
{x} is maximal_anti-discrete
let x be Point of X; ::_thesis: ( Cl {x} = {x} implies {x} is maximal_anti-discrete )
assume A1: Cl {x} = {x} ; ::_thesis: {x} is maximal_anti-discrete
{x} is anti-discrete by Th6;
hence {x} is maximal_anti-discrete by A1, Th17; ::_thesis: verum
end;
theorem Th46: :: TEX_4:46
for X being non empty TopSpace
for x being Point of X holds MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) }
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X holds MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) }
let x be Point of X; ::_thesis: MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) }
set F = { G where G is Subset of X : ( G is open & x in G ) } ;
{ G where G is Subset of X : ( G is open & x in G ) } c= bool the carrier of X
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & x in G ) } or C in bool the carrier of X )
assume C in { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is open & x in P ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
then reconsider F = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ;
now__::_thesis:_for_C_being_set_st_C_in_F_holds_
MaxADSet_x_c=_C
let C be set ; ::_thesis: ( C in F implies MaxADSet x c= C )
assume C in F ; ::_thesis: MaxADSet x c= C
then ex G being Subset of X st
( G = C & G is open & x in G ) ;
hence MaxADSet x c= C by Th24; ::_thesis: verum
end;
hence MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) } by SETFAM_1:5; ::_thesis: verum
end;
theorem Th47: :: TEX_4:47
for X being non empty TopSpace
for x being Point of X holds MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) }
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X holds MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) }
let x be Point of X; ::_thesis: MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) }
set G = { F where F is Subset of X : ( F is closed & x in F ) } ;
{ F where F is Subset of X : ( F is closed & x in F ) } c= bool the carrier of X
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { F where F is Subset of X : ( F is closed & x in F ) } or C in bool the carrier of X )
assume C in { F where F is Subset of X : ( F is closed & x in F ) } ; ::_thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is closed & x in P ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
then reconsider G = { F where F is Subset of X : ( F is closed & x in F ) } as Subset-Family of X ;
now__::_thesis:_for_C_being_set_st_C_in_G_holds_
MaxADSet_x_c=_C
let C be set ; ::_thesis: ( C in G implies MaxADSet x c= C )
assume C in G ; ::_thesis: MaxADSet x c= C
then ex F being Subset of X st
( F = C & F is closed & x in F ) ;
hence MaxADSet x c= C by Th23; ::_thesis: verum
end;
hence MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) } by SETFAM_1:5; ::_thesis: verum
end;
theorem Th48: :: TEX_4:48
for X being non empty TopSpace
for x being Point of X holds MaxADSet x c= Cl {x}
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X holds MaxADSet x c= Cl {x}
let x be Point of X; ::_thesis: MaxADSet x c= Cl {x}
Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) } by Th2;
hence MaxADSet x c= Cl {x} by Th47; ::_thesis: verum
end;
Lm1: for X being non empty TopSpace
for x, y being Point of X st MaxADSet x = MaxADSet y holds
Cl {x} = Cl {y}
proof
let X be non empty TopSpace; ::_thesis: for x, y being Point of X st MaxADSet x = MaxADSet y holds
Cl {x} = Cl {y}
let x, y be Point of X; ::_thesis: ( MaxADSet x = MaxADSet y implies Cl {x} = Cl {y} )
assume A1: MaxADSet x = MaxADSet y ; ::_thesis: Cl {x} = Cl {y}
then A2: y in MaxADSet x by Th21;
MaxADSet y is maximal_anti-discrete by Th20;
then A3: MaxADSet y is anti-discrete by Def7;
x in MaxADSet y by A1, Th21;
hence Cl {x} = Cl {y} by A1, A2, A3, Def14; ::_thesis: verum
end;
theorem Th49: :: TEX_4:49
for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )
proof
let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds
( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )
let x, y be Point of X; ::_thesis: ( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )
A1: MaxADSet x c= (MaxADSet x) \/ (MaxADSet y) by XBOOLE_1:7;
thus ( MaxADSet x = MaxADSet y implies Cl {x} = Cl {y} ) by Lm1; ::_thesis: ( Cl {x} = Cl {y} implies MaxADSet x = MaxADSet y )
A2: MaxADSet y c= (MaxADSet x) \/ (MaxADSet y) by XBOOLE_1:7;
assume A3: Cl {x} = Cl {y} ; ::_thesis: MaxADSet x = MaxADSet y
now__::_thesis:_for_a_being_Point_of_X_st_a_in_(MaxADSet_x)_\/_(MaxADSet_y)_holds_
(MaxADSet_x)_\/_(MaxADSet_y)_c=_Cl_{a}
let a be Point of X; ::_thesis: ( a in (MaxADSet x) \/ (MaxADSet y) implies (MaxADSet x) \/ (MaxADSet y) c= Cl {a} )
assume A4: a in (MaxADSet x) \/ (MaxADSet y) ; ::_thesis: (MaxADSet x) \/ (MaxADSet y) c= Cl {a}
now__::_thesis:_(MaxADSet_x)_\/_(MaxADSet_y)_c=_Cl_{a}
percases ( a in MaxADSet x or a in MaxADSet y ) by A4, XBOOLE_0:def_3;
suppose a in MaxADSet x ; ::_thesis: (MaxADSet x) \/ (MaxADSet y) c= Cl {a}
then A5: MaxADSet a = MaxADSet x by Th21;
then Cl {a} = Cl {x} by Lm1;
then A6: MaxADSet y c= Cl {a} by A3, Th48;
MaxADSet x c= Cl {a} by A5, Th48;
hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} by A6, XBOOLE_1:8; ::_thesis: verum
end;
suppose a in MaxADSet y ; ::_thesis: (MaxADSet x) \/ (MaxADSet y) c= Cl {a}
then A7: MaxADSet a = MaxADSet y by Th21;
then Cl {a} = Cl {y} by Lm1;
then A8: MaxADSet x c= Cl {a} by A3, Th48;
MaxADSet y c= Cl {a} by A7, Th48;
hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} by A8, XBOOLE_1:8; ::_thesis: verum
end;
end;
end;
hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} ; ::_thesis: verum
end;
then A9: (MaxADSet x) \/ (MaxADSet y) is anti-discrete by Def12;
A10: MaxADSet y is maximal_anti-discrete by Th20;
MaxADSet x is maximal_anti-discrete by Th20;
then MaxADSet x = (MaxADSet x) \/ (MaxADSet y) by A9, A1, Def7;
hence MaxADSet x = MaxADSet y by A9, A10, A2, Def7; ::_thesis: verum
end;
theorem :: TEX_4:50
for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff Cl {x} <> Cl {y} )
proof
let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff Cl {x} <> Cl {y} )
let x, y be Point of X; ::_thesis: ( MaxADSet x misses MaxADSet y iff Cl {x} <> Cl {y} )
thus ( MaxADSet x misses MaxADSet y implies Cl {x} <> Cl {y} ) by Th49; ::_thesis: ( Cl {x} <> Cl {y} implies MaxADSet x misses MaxADSet y )
assume A1: Cl {x} <> Cl {y} ; ::_thesis: MaxADSet x misses MaxADSet y
assume MaxADSet x meets MaxADSet y ; ::_thesis: contradiction
then MaxADSet x = MaxADSet y by Th22;
hence contradiction by A1, Th49; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
let x be Point of X;
:: original: MaxADSet
redefine func MaxADSet x -> non empty Subset of X equals :: TEX_4:def 15
(Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } );
compatibility
for b1 being non empty Subset of X holds
( b1 = MaxADSet x iff b1 = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } ) )
proof
set F = { G where G is Subset of X : ( G is open & x in G ) } ;
{ G where G is Subset of X : ( G is open & x in G ) } c= bool the carrier of X
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & x in G ) } or C in bool the carrier of X )
assume C in { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is open & x in P ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
then reconsider F = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ;
A1: MaxADSet x c= Cl {x} by Th48;
A2: (Cl {x}) /\ (meet F) c= MaxADSet x
proof
assume not (Cl {x}) /\ (meet F) c= MaxADSet x ; ::_thesis: contradiction
then ((Cl {x}) /\ (meet F)) \ (MaxADSet x) <> {} by XBOOLE_1:37;
then consider a being set such that
A3: a in ((Cl {x}) /\ (meet F)) \ (MaxADSet x) by XBOOLE_0:def_1;
A4: a in (Cl {x}) /\ (meet F) by A3, XBOOLE_0:def_5;
reconsider a = a as Point of X by A3;
not a in MaxADSet x by A3, XBOOLE_0:def_5;
then A5: MaxADSet a <> MaxADSet x by Th21;
now__::_thesis:_x_in_Cl_{a}
set G = (Cl {a}) ` ;
{a} c= Cl {a} by PRE_TOPC:18;
then A6: a in Cl {a} by ZFMISC_1:31;
assume not x in Cl {a} ; ::_thesis: contradiction
then x in (Cl {a}) ` by SUBSET_1:29;
then (Cl {a}) ` in F ;
then A7: meet F c= (Cl {a}) ` by SETFAM_1:3;
a in meet F by A4, XBOOLE_0:def_4;
hence contradiction by A7, A6, XBOOLE_0:def_5; ::_thesis: verum
end;
then {x} c= Cl {a} by ZFMISC_1:31;
then A8: Cl {x} c= Cl {a} by TOPS_1:5;
a in Cl {x} by A4, XBOOLE_0:def_4;
then {a} c= Cl {x} by ZFMISC_1:31;
then Cl {a} c= Cl {x} by TOPS_1:5;
then Cl {x} = Cl {a} by A8, XBOOLE_0:def_10;
hence contradiction by A5, Th49; ::_thesis: verum
end;
MaxADSet x c= meet F by Th46;
then MaxADSet x c= (Cl {x}) /\ (meet F) by A1, XBOOLE_1:19;
hence for b1 being non empty Subset of X holds
( b1 = MaxADSet x iff b1 = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } ) ) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
coherence
MaxADSet x is non empty Subset of X ;
end;
:: deftheorem defines MaxADSet TEX_4:def_15_:_
for X being non empty TopSpace
for x being Point of X holds MaxADSet x = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } );
theorem Th51: :: TEX_4:51
for X being non empty TopSpace
for x, y being Point of X holds
( Cl {x} c= Cl {y} iff meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } )
proof
let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds
( Cl {x} c= Cl {y} iff meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } )
let x, y be Point of X; ::_thesis: ( Cl {x} c= Cl {y} iff meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } )
set FX = { G where G is Subset of X : ( G is open & x in G ) } ;
set FY = { G where G is Subset of X : ( G is open & y in G ) } ;
A1: [#] X in { G where G is Subset of X : ( G is open & x in G ) } ;
thus ( Cl {x} c= Cl {y} implies meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } ) ::_thesis: ( meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } implies Cl {x} c= Cl {y} )
proof
assume A2: Cl {x} c= Cl {y} ; ::_thesis: meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) }
now__::_thesis:_for_P_being_set_st_P_in__{__G_where_G_is_Subset_of_X_:_(_G_is_open_&_x_in_G_)__}__holds_
P_in__{__G_where_G_is_Subset_of_X_:_(_G_is_open_&_y_in_G_)__}_
let P be set ; ::_thesis: ( P in { G where G is Subset of X : ( G is open & x in G ) } implies P in { G where G is Subset of X : ( G is open & y in G ) } )
assume P in { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: P in { G where G is Subset of X : ( G is open & y in G ) }
then consider G being Subset of X such that
A3: G = P and
A4: G is open and
A5: x in G ;
now__::_thesis:_y_in_G
assume not y in G ; ::_thesis: contradiction
then {y} misses G by ZFMISC_1:50;
then A6: Cl {y} misses G by A4, TSEP_1:36;
{x} c= Cl {x} by PRE_TOPC:18;
then x in Cl {x} by ZFMISC_1:31;
hence contradiction by A2, A5, A6, XBOOLE_0:3; ::_thesis: verum
end;
hence P in { G where G is Subset of X : ( G is open & y in G ) } by A3, A4; ::_thesis: verum
end;
then { G where G is Subset of X : ( G is open & x in G ) } c= { G where G is Subset of X : ( G is open & y in G ) } by TARSKI:def_3;
hence meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } by A1, SETFAM_1:6; ::_thesis: verum
end;
assume A7: meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: Cl {x} c= Cl {y}
set G = (Cl {y}) ` ;
assume A8: not Cl {x} c= Cl {y} ; ::_thesis: contradiction
now__::_thesis:_not_x_in_Cl_{y}
assume x in Cl {y} ; ::_thesis: contradiction
then {x} c= Cl {y} by ZFMISC_1:31;
hence contradiction by A8, TOPS_1:5; ::_thesis: verum
end;
then x in (Cl {y}) ` by SUBSET_1:29;
then (Cl {y}) ` in { G where G is Subset of X : ( G is open & x in G ) } ;
then meet { G where G is Subset of X : ( G is open & x in G ) } c= (Cl {y}) ` by SETFAM_1:3;
then A9: meet { G where G is Subset of X : ( G is open & y in G ) } c= (Cl {y}) ` by A7, XBOOLE_1:1;
{y} c= Cl {y} by PRE_TOPC:18;
then A10: y in Cl {y} by ZFMISC_1:31;
{y} c= MaxADSet y by Th12;
then A11: y in MaxADSet y by ZFMISC_1:31;
MaxADSet y c= meet { G where G is Subset of X : ( G is open & y in G ) } by Th46;
then y in meet { G where G is Subset of X : ( G is open & y in G ) } by A11;
hence contradiction by A9, A10, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: TEX_4:52
for X being non empty TopSpace
for x, y being Point of X holds
( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } )
proof
let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds
( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } )
let x, y be Point of X; ::_thesis: ( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } )
set FY = { G where G is Subset of X : ( G is open & y in G ) } ;
{ G where G is Subset of X : ( G is open & y in G ) } c= bool the carrier of X
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & y in G ) } or C in bool the carrier of X )
assume C in { G where G is Subset of X : ( G is open & y in G ) } ; ::_thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is open & y in P ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
then reconsider FY = { G where G is Subset of X : ( G is open & y in G ) } as Subset-Family of X ;
set FX = { G where G is Subset of X : ( G is open & x in G ) } ;
{ G where G is Subset of X : ( G is open & x in G ) } c= bool the carrier of X
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & x in G ) } or C in bool the carrier of X )
assume C in { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is open & x in P ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
then reconsider FX = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ;
thus ( Cl {x} c= Cl {y} implies MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } ) ::_thesis: ( MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } implies Cl {x} c= Cl {y} )
proof
assume Cl {x} c= Cl {y} ; ::_thesis: MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) }
then A1: meet FY c= meet FX by Th51;
(Cl {y}) /\ (meet FY) c= meet FY by XBOOLE_1:17;
hence MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } by A1, XBOOLE_1:1; ::_thesis: verum
end;
{y} c= MaxADSet y by Th12;
then A2: y in MaxADSet y by ZFMISC_1:31;
assume MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: Cl {x} c= Cl {y}
then A3: y in meet FX by A2;
set G = (Cl {y}) ` ;
assume A4: not Cl {x} c= Cl {y} ; ::_thesis: contradiction
now__::_thesis:_not_x_in_Cl_{y}
assume x in Cl {y} ; ::_thesis: contradiction
then {x} c= Cl {y} by ZFMISC_1:31;
hence contradiction by A4, TOPS_1:5; ::_thesis: verum
end;
then x in (Cl {y}) ` by SUBSET_1:29;
then (Cl {y}) ` in FX ;
then A5: meet FX c= (Cl {y}) ` by SETFAM_1:3;
{y} c= Cl {y} by PRE_TOPC:18;
then y in Cl {y} by ZFMISC_1:31;
hence contradiction by A5, A3, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th53: :: TEX_4:53
for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) )
proof
let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) )
let x, y be Point of X; ::_thesis: ( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) )
thus ( not MaxADSet x misses MaxADSet y or ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) ::_thesis: ( ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) implies MaxADSet x misses MaxADSet y )
proof
set V = (Cl {y}) ` ;
set W = (Cl {x}) ` ;
assume A1: (MaxADSet x) /\ (MaxADSet y) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) )
assume A2: for V being Subset of X st V is open & MaxADSet x c= V holds
V meets MaxADSet y ; ::_thesis: ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W )
now__::_thesis:_ex_W_being_Element_of_bool_the_carrier_of_X_st_
(_W_is_open_&_W_misses_MaxADSet_x_&_MaxADSet_y_c=_W_)
take W = (Cl {x}) ` ; ::_thesis: ( W is open & W misses MaxADSet x & MaxADSet y c= W )
thus W is open ; ::_thesis: ( W misses MaxADSet x & MaxADSet y c= W )
MaxADSet x c= Cl {x} by Th48;
hence W misses MaxADSet x by SUBSET_1:24; ::_thesis: MaxADSet y c= W
now__::_thesis:_MaxADSet_y_c=_W
MaxADSet y c= Cl {y} by Th48;
then (Cl {y}) ` misses MaxADSet y by SUBSET_1:24;
then not MaxADSet x c= (Cl {y}) ` by A2;
then (MaxADSet x) \ ((Cl {y}) `) <> {} by XBOOLE_1:37;
then consider b being set such that
A3: b in (MaxADSet x) \ ((Cl {y}) `) by XBOOLE_0:def_1;
A4: b in MaxADSet x by A3, XBOOLE_0:def_5;
reconsider b = b as Point of X by A3;
not b in (Cl {y}) ` by A3, XBOOLE_0:def_5;
then b in Cl {y} by SUBSET_1:29;
then A5: {b} c= Cl {y} by ZFMISC_1:31;
MaxADSet b = MaxADSet x by A4, Th21;
then Cl {b} = Cl {x} by Th49;
then A6: Cl {x} c= Cl {y} by A5, TOPS_1:5;
assume not MaxADSet y c= W ; ::_thesis: contradiction
then (MaxADSet y) \ W <> {} by XBOOLE_1:37;
then consider a being set such that
A7: a in (MaxADSet y) \ W by XBOOLE_0:def_1;
A8: a in MaxADSet y by A7, XBOOLE_0:def_5;
reconsider a = a as Point of X by A7;
not a in W by A7, XBOOLE_0:def_5;
then a in Cl {x} by SUBSET_1:29;
then A9: {a} c= Cl {x} by ZFMISC_1:31;
MaxADSet a = MaxADSet y by A8, Th21;
then Cl {a} = Cl {y} by Th49;
then Cl {y} c= Cl {x} by A9, TOPS_1:5;
then Cl {x} = Cl {y} by A6, XBOOLE_0:def_10;
then MaxADSet x = MaxADSet y by Th49;
hence contradiction by A1; ::_thesis: verum
end;
hence MaxADSet y c= W ; ::_thesis: verum
end;
hence ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; ::_thesis: verum
end;
assume A10: ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) ; ::_thesis: MaxADSet x misses MaxADSet y
assume MaxADSet x meets MaxADSet y ; ::_thesis: contradiction
then A11: MaxADSet x = MaxADSet y by Th22;
now__::_thesis:_contradiction
percases ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) by A10;
suppose ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) ; ::_thesis: contradiction
then consider V being Subset of X such that
V is open and
A12: MaxADSet x c= V and
A13: V misses MaxADSet y ;
V /\ (MaxADSet y) = {} by A13, XBOOLE_0:def_7;
hence contradiction by A11, A12, XBOOLE_1:28; ::_thesis: verum
end;
suppose ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; ::_thesis: contradiction
then consider W being Subset of X such that
W is open and
A14: W misses MaxADSet x and
A15: MaxADSet y c= W ;
W /\ (MaxADSet x) = {} by A14, XBOOLE_0:def_7;
hence contradiction by A11, A15, XBOOLE_1:28; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem :: TEX_4:54
for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) )
proof
let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) )
let x, y be Point of X; ::_thesis: ( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) )
thus ( not MaxADSet x misses MaxADSet y or ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ::_thesis: ( ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) implies MaxADSet x misses MaxADSet y )
proof
assume A1: MaxADSet x misses MaxADSet y ; ::_thesis: ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) )
hereby ::_thesis: verum
percases ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) by A1, Th53;
suppose ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) ; ::_thesis: ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) )
then consider V being Subset of X such that
A2: V is open and
A3: MaxADSet x c= V and
A4: V misses MaxADSet y ;
now__::_thesis:_ex_F_being_Element_of_bool_the_carrier_of_X_st_
(_F_is_closed_&_F_misses_MaxADSet_x_&_MaxADSet_y_c=_F_)
take F = V ` ; ::_thesis: ( F is closed & F misses MaxADSet x & MaxADSet y c= F )
thus F is closed by A2; ::_thesis: ( F misses MaxADSet x & MaxADSet y c= F )
thus F misses MaxADSet x by A3, SUBSET_1:24; ::_thesis: MaxADSet y c= F
thus MaxADSet y c= F by A4, SUBSET_1:23; ::_thesis: verum
end;
hence ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ; ::_thesis: verum
end;
suppose ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; ::_thesis: ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) )
then consider W being Subset of X such that
A5: W is open and
A6: W misses MaxADSet x and
A7: MaxADSet y c= W ;
now__::_thesis:_ex_E_being_Element_of_bool_the_carrier_of_X_st_
(_E_is_closed_&_MaxADSet_x_c=_E_&_E_misses_MaxADSet_y_)
take E = W ` ; ::_thesis: ( E is closed & MaxADSet x c= E & E misses MaxADSet y )
thus E is closed by A5; ::_thesis: ( MaxADSet x c= E & E misses MaxADSet y )
thus MaxADSet x c= E by A6, SUBSET_1:23; ::_thesis: E misses MaxADSet y
thus E misses MaxADSet y by A7, SUBSET_1:24; ::_thesis: verum
end;
hence ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ; ::_thesis: verum
end;
end;
end;
end;
assume A8: ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ; ::_thesis: MaxADSet x misses MaxADSet y
assume MaxADSet x meets MaxADSet y ; ::_thesis: contradiction
then A9: MaxADSet x = MaxADSet y by Th22;
now__::_thesis:_contradiction
percases ( ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) by A8;
suppose ex E being Subset of X st
( E is closed & MaxADSet x c= E & E misses MaxADSet y ) ; ::_thesis: contradiction
then consider E being Subset of X such that
E is closed and
A10: MaxADSet x c= E and
A11: E misses MaxADSet y ;
E /\ (MaxADSet y) = {} by A11, XBOOLE_0:def_7;
hence contradiction by A9, A10, XBOOLE_1:28; ::_thesis: verum
end;
suppose ex F being Subset of X st
( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ; ::_thesis: contradiction
then consider F being Subset of X such that
F is closed and
A12: F misses MaxADSet x and
A13: MaxADSet y c= F ;
F /\ (MaxADSet x) = {} by A12, XBOOLE_0:def_7;
hence contradiction by A9, A13, XBOOLE_1:28; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem Th55: :: TEX_4:55
for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) }
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) }
let A be Subset of X; ::_thesis: MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) }
set F = { G where G is Subset of X : ( G is open & A c= G ) } ;
{ G where G is Subset of X : ( G is open & A c= G ) } c= bool the carrier of X
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & A c= G ) } or C in bool the carrier of X )
assume C in { G where G is Subset of X : ( G is open & A c= G ) } ; ::_thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is open & A c= P ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
then reconsider F = { G where G is Subset of X : ( G is open & A c= G ) } as Subset-Family of X ;
[#] X in F ;
hence MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) } by Th39; ::_thesis: verum
end;
theorem Th56: :: TEX_4:56
for X being non empty TopSpace
for P being Subset of X st P is open holds
MaxADSet P = P
proof
let X be non empty TopSpace; ::_thesis: for P being Subset of X st P is open holds
MaxADSet P = P
let P be Subset of X; ::_thesis: ( P is open implies MaxADSet P = P )
set F = { G where G is Subset of X : ( G is open & P c= G ) } ;
A1: P c= MaxADSet P by Th32;
assume P is open ; ::_thesis: MaxADSet P = P
then P in { G where G is Subset of X : ( G is open & P c= G ) } ;
then A2: meet { G where G is Subset of X : ( G is open & P c= G ) } c= P by SETFAM_1:3;
MaxADSet P c= meet { G where G is Subset of X : ( G is open & P c= G ) } by Th55;
then MaxADSet P c= P by A2, XBOOLE_1:1;
hence MaxADSet P = P by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TEX_4:57
for X being non empty TopSpace
for A being Subset of X holds MaxADSet (Int A) = Int A by Th56;
theorem Th58: :: TEX_4:58
for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) }
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) }
let A be Subset of X; ::_thesis: MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) }
set G = { F where F is Subset of X : ( F is closed & A c= F ) } ;
{ F where F is Subset of X : ( F is closed & A c= F ) } c= bool the carrier of X
proof
let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { F where F is Subset of X : ( F is closed & A c= F ) } or C in bool the carrier of X )
assume C in { F where F is Subset of X : ( F is closed & A c= F ) } ; ::_thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is closed & A c= P ) ;
hence C in bool the carrier of X ; ::_thesis: verum
end;
then reconsider G = { F where F is Subset of X : ( F is closed & A c= F ) } as Subset-Family of X ;
[#] X in G ;
hence MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) } by Th41; ::_thesis: verum
end;
theorem Th59: :: TEX_4:59
for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= Cl A
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds MaxADSet A c= Cl A
let A be Subset of X; ::_thesis: MaxADSet A c= Cl A
Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) } by Th1;
hence MaxADSet A c= Cl A by Th58; ::_thesis: verum
end;
theorem Th60: :: TEX_4:60
for X being non empty TopSpace
for P being Subset of X st P is closed holds
MaxADSet P = P
proof
let X be non empty TopSpace; ::_thesis: for P being Subset of X st P is closed holds
MaxADSet P = P
let P be Subset of X; ::_thesis: ( P is closed implies MaxADSet P = P )
assume P is closed ; ::_thesis: MaxADSet P = P
then A1: Cl P = P by PRE_TOPC:22;
A2: P c= MaxADSet P by Th32;
MaxADSet P c= Cl P by Th59;
hence MaxADSet P = P by A1, A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TEX_4:61
for X being non empty TopSpace
for A being Subset of X holds MaxADSet (Cl A) = Cl A by Th60;
theorem :: TEX_4:62
for X being non empty TopSpace
for A being Subset of X holds Cl (MaxADSet A) = Cl A
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds Cl (MaxADSet A) = Cl A
let A be Subset of X; ::_thesis: Cl (MaxADSet A) = Cl A
A1: Cl (MaxADSet A) c= Cl A by Th59, TOPS_1:5;
Cl A c= Cl (MaxADSet A) by Th32, PRE_TOPC:19;
hence Cl (MaxADSet A) = Cl A by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TEX_4:63
for X being non empty TopSpace
for A, B being Subset of X st MaxADSet A = MaxADSet B holds
Cl A = Cl B
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st MaxADSet A = MaxADSet B holds
Cl A = Cl B
let A, B be Subset of X; ::_thesis: ( MaxADSet A = MaxADSet B implies Cl A = Cl B )
A1: MaxADSet A c= Cl A by Th59;
A2: MaxADSet B c= Cl B by Th59;
assume A3: MaxADSet A = MaxADSet B ; ::_thesis: Cl A = Cl B
then A c= MaxADSet B by Th32;
then A c= Cl B by A2, XBOOLE_1:1;
then A4: Cl A c= Cl B by TOPS_1:5;
B c= MaxADSet A by A3, Th32;
then B c= Cl A by A1, XBOOLE_1:1;
then Cl B c= Cl A by TOPS_1:5;
hence Cl A = Cl B by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TEX_4:64
for X being non empty TopSpace
for P, Q being Subset of X st ( P is closed or Q is closed ) holds
MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
proof
let X be non empty TopSpace; ::_thesis: for P, Q being Subset of X st ( P is closed or Q is closed ) holds
MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
let P, Q be Subset of X; ::_thesis: ( ( P is closed or Q is closed ) implies MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) )
assume A1: ( P is closed or Q is closed ) ; ::_thesis: MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
A2: (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q)
proof
assume not (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q) ; ::_thesis: contradiction
then consider x being set such that
A3: x in (MaxADSet P) /\ (MaxADSet Q) and
A4: not x in MaxADSet (P /\ Q) by TARSKI:def_3;
reconsider x = x as Point of X by A3;
now__::_thesis:_contradiction
percases ( P is closed or Q is closed ) by A1;
supposeA5: P is closed ; ::_thesis: contradiction
then P = MaxADSet P by Th60;
then x in P by A3, XBOOLE_0:def_4;
then A6: MaxADSet x c= P by A5, Th23;
A7: P /\ Q c= MaxADSet (P /\ Q) by Th32;
x in MaxADSet Q by A3, XBOOLE_0:def_4;
then consider D being set such that
A8: x in D and
A9: D in { (MaxADSet b) where b is Point of X : b in Q } by TARSKI:def_4;
consider b being Point of X such that
A10: D = MaxADSet b and
A11: b in Q by A9;
{b} c= MaxADSet b by Th12;
then A12: b in MaxADSet b by ZFMISC_1:31;
MaxADSet x = MaxADSet b by A8, A10, Th21;
then b in P /\ Q by A6, A11, A12, XBOOLE_0:def_4;
then MaxADSet b meets MaxADSet (P /\ Q) by A12, A7, XBOOLE_0:3;
then MaxADSet b c= MaxADSet (P /\ Q) by Th30;
hence contradiction by A4, A8, A10; ::_thesis: verum
end;
supposeA13: Q is closed ; ::_thesis: contradiction
then Q = MaxADSet Q by Th60;
then x in Q by A3, XBOOLE_0:def_4;
then A14: MaxADSet x c= Q by A13, Th23;
A15: P /\ Q c= MaxADSet (P /\ Q) by Th32;
x in MaxADSet P by A3, XBOOLE_0:def_4;
then consider D being set such that
A16: x in D and
A17: D in { (MaxADSet b) where b is Point of X : b in P } by TARSKI:def_4;
consider b being Point of X such that
A18: D = MaxADSet b and
A19: b in P by A17;
{b} c= MaxADSet b by Th12;
then A20: b in MaxADSet b by ZFMISC_1:31;
MaxADSet x = MaxADSet b by A16, A18, Th21;
then b in P /\ Q by A14, A19, A20, XBOOLE_0:def_4;
then MaxADSet b meets MaxADSet (P /\ Q) by A20, A15, XBOOLE_0:3;
then MaxADSet b c= MaxADSet (P /\ Q) by Th30;
hence contradiction by A4, A16, A18; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
MaxADSet (P /\ Q) c= (MaxADSet P) /\ (MaxADSet Q) by Th37;
hence MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TEX_4:65
for X being non empty TopSpace
for P, Q being Subset of X st ( P is open or Q is open ) holds
MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
proof
let X be non empty TopSpace; ::_thesis: for P, Q being Subset of X st ( P is open or Q is open ) holds
MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
let P, Q be Subset of X; ::_thesis: ( ( P is open or Q is open ) implies MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) )
assume A1: ( P is open or Q is open ) ; ::_thesis: MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
A2: (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q)
proof
assume not (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q) ; ::_thesis: contradiction
then consider x being set such that
A3: x in (MaxADSet P) /\ (MaxADSet Q) and
A4: not x in MaxADSet (P /\ Q) by TARSKI:def_3;
reconsider x = x as Point of X by A3;
now__::_thesis:_contradiction
percases ( P is open or Q is open ) by A1;
supposeA5: P is open ; ::_thesis: contradiction
then P = MaxADSet P by Th56;
then x in P by A3, XBOOLE_0:def_4;
then A6: MaxADSet x c= P by A5, Th24;
A7: P /\ Q c= MaxADSet (P /\ Q) by Th32;
x in MaxADSet Q by A3, XBOOLE_0:def_4;
then consider D being set such that
A8: x in D and
A9: D in { (MaxADSet b) where b is Point of X : b in Q } by TARSKI:def_4;
consider b being Point of X such that
A10: D = MaxADSet b and
A11: b in Q by A9;
{b} c= MaxADSet b by Th12;
then A12: b in MaxADSet b by ZFMISC_1:31;
MaxADSet x = MaxADSet b by A8, A10, Th21;
then b in P /\ Q by A6, A11, A12, XBOOLE_0:def_4;
then MaxADSet b meets MaxADSet (P /\ Q) by A12, A7, XBOOLE_0:3;
then MaxADSet b c= MaxADSet (P /\ Q) by Th30;
hence contradiction by A4, A8, A10; ::_thesis: verum
end;
supposeA13: Q is open ; ::_thesis: contradiction
then Q = MaxADSet Q by Th56;
then x in Q by A3, XBOOLE_0:def_4;
then A14: MaxADSet x c= Q by A13, Th24;
A15: P /\ Q c= MaxADSet (P /\ Q) by Th32;
x in MaxADSet P by A3, XBOOLE_0:def_4;
then consider D being set such that
A16: x in D and
A17: D in { (MaxADSet b) where b is Point of X : b in P } by TARSKI:def_4;
consider b being Point of X such that
A18: D = MaxADSet b and
A19: b in P by A17;
{b} c= MaxADSet b by Th12;
then A20: b in MaxADSet b by ZFMISC_1:31;
MaxADSet x = MaxADSet b by A16, A18, Th21;
then b in P /\ Q by A14, A19, A20, XBOOLE_0:def_4;
then MaxADSet b meets MaxADSet (P /\ Q) by A20, A15, XBOOLE_0:3;
then MaxADSet b c= MaxADSet (P /\ Q) by Th30;
hence contradiction by A4, A16, A18; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
MaxADSet (P /\ Q) c= (MaxADSet P) /\ (MaxADSet Q) by Th37;
hence MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
theorem Th66: :: TEX_4:66
for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds
A is anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds
A is anti-discrete
let Y0 be SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds
A is anti-discrete
let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 & Y0 is anti-discrete implies A is anti-discrete )
assume A1: A = the carrier of Y0 ; ::_thesis: ( not Y0 is anti-discrete or A is anti-discrete )
assume Y0 is anti-discrete ; ::_thesis: A is anti-discrete
then A2: the topology of Y0 = {{}, the carrier of Y0} by TDLAT_3:def_2;
now__::_thesis:_for_G_being_Subset_of_Y_holds_
(_not_G_is_open_or_A_misses_G_or_A_c=_G_)
let G be Subset of Y; ::_thesis: ( not G is open or A misses G or A c= G )
reconsider H = A /\ G as Subset of Y0 by A1, XBOOLE_1:17;
assume A3: G is open ; ::_thesis: ( A misses G or A c= G )
now__::_thesis:_ex_G_being_Subset_of_Y_st_
(_G_in_the_topology_of_Y_&_H_=_G_/\_([#]_Y0)_)
take G = G; ::_thesis: ( G in the topology of Y & H = G /\ ([#] Y0) )
thus G in the topology of Y by A3, PRE_TOPC:def_2; ::_thesis: H = G /\ ([#] Y0)
thus H = G /\ ([#] Y0) by A1; ::_thesis: verum
end;
then H in the topology of Y0 by PRE_TOPC:def_4;
then ( A /\ G = {} or A /\ G = the carrier of Y0 ) by A2, TARSKI:def_2;
hence ( A misses G or A c= G ) by A1, XBOOLE_0:def_7, XBOOLE_1:17; ::_thesis: verum
end;
hence A is anti-discrete by Def3; ::_thesis: verum
end;
theorem Th67: :: TEX_4:67
for Y being non empty TopStruct
for Y0 being SubSpace of Y st Y0 is TopSpace-like holds
for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds
Y0 is anti-discrete
proof
let Y be non empty TopStruct ; ::_thesis: for Y0 being SubSpace of Y st Y0 is TopSpace-like holds
for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds
Y0 is anti-discrete
let Y0 be SubSpace of Y; ::_thesis: ( Y0 is TopSpace-like implies for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds
Y0 is anti-discrete )
assume A1: Y0 is TopSpace-like ; ::_thesis: for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds
Y0 is anti-discrete
then A2: the carrier of Y0 in the topology of Y0 by PRE_TOPC:def_1;
let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 & A is anti-discrete implies Y0 is anti-discrete )
assume A3: A = the carrier of Y0 ; ::_thesis: ( not A is anti-discrete or Y0 is anti-discrete )
assume A4: A is anti-discrete ; ::_thesis: Y0 is anti-discrete
now__::_thesis:_for_D_being_set_st_D_in_the_topology_of_Y0_holds_
D_in_{{},_the_carrier_of_Y0}
let D be set ; ::_thesis: ( D in the topology of Y0 implies D in {{}, the carrier of Y0} )
assume A5: D in the topology of Y0 ; ::_thesis: D in {{}, the carrier of Y0}
then reconsider C = D as Subset of Y0 ;
consider E being Subset of Y such that
A6: E in the topology of Y and
A7: C = E /\ ([#] Y0) by A5, PRE_TOPC:def_4;
reconsider E = E as Subset of Y ;
A8: E is open by A6, PRE_TOPC:def_2;
now__::_thesis:_(_C_=_{}_or_C_=_A_)
percases ( A misses E or A c= E ) by A4, A8, Def3;
suppose A misses E ; ::_thesis: ( C = {} or C = A )
hence ( C = {} or C = A ) by A3, A7, XBOOLE_0:def_7; ::_thesis: verum
end;
suppose A c= E ; ::_thesis: ( C = {} or C = A )
hence ( C = {} or C = A ) by A3, A7, XBOOLE_1:28; ::_thesis: verum
end;
end;
end;
hence D in {{}, the carrier of Y0} by A3, TARSKI:def_2; ::_thesis: verum
end;
then A9: the topology of Y0 c= {{}, the carrier of Y0} by TARSKI:def_3;
{} in the topology of Y0 by A1, PRE_TOPC:1;
then {{}, the carrier of Y0} c= the topology of Y0 by A2, ZFMISC_1:32;
then the topology of Y0 = {{}, the carrier of Y0} by A9, XBOOLE_0:def_10;
hence Y0 is anti-discrete by TDLAT_3:def_2; ::_thesis: verum
end;
theorem :: TEX_4:68
for X being non empty TopSpace
for Y0 being non empty SubSpace of X st ( for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds
Y0 is anti-discrete
proof
let X be non empty TopSpace; ::_thesis: for Y0 being non empty SubSpace of X st ( for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds
Y0 is anti-discrete
let Y0 be non empty SubSpace of X; ::_thesis: ( ( for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) implies Y0 is anti-discrete )
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
assume A1: for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ; ::_thesis: Y0 is anti-discrete
now__::_thesis:_for_G_being_Subset_of_X_holds_
(_not_G_is_open_or_A_misses_G_or_A_c=_G_)
let G be Subset of X; ::_thesis: ( not G is open or A misses G or A c= G )
assume A2: G is open ; ::_thesis: ( A misses G or A c= G )
now__::_thesis:_(_A_misses_G_or_A_c=_G_)
percases ( G is empty or not G is empty ) ;
suppose G is empty ; ::_thesis: ( A misses G or A c= G )
hence ( A misses G or A c= G ) by XBOOLE_1:65; ::_thesis: verum
end;
suppose not G is empty ; ::_thesis: ( A misses G or A c= G )
then consider X0 being non empty strict open SubSpace of X such that
A3: G = the carrier of X0 by A2, TSEP_1:20;
( Y0 misses X0 or Y0 is SubSpace of X0 ) by A1;
hence ( A misses G or A c= G ) by A3, TSEP_1:4, TSEP_1:def_3; ::_thesis: verum
end;
end;
end;
hence ( A misses G or A c= G ) ; ::_thesis: verum
end;
then A is anti-discrete by Def3;
hence Y0 is anti-discrete by Th67; ::_thesis: verum
end;
theorem :: TEX_4:69
for X being non empty TopSpace
for Y0 being non empty SubSpace of X st ( for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds
Y0 is anti-discrete
proof
let X be non empty TopSpace; ::_thesis: for Y0 being non empty SubSpace of X st ( for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds
Y0 is anti-discrete
let Y0 be non empty SubSpace of X; ::_thesis: ( ( for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) implies Y0 is anti-discrete )
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
assume A1: for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ; ::_thesis: Y0 is anti-discrete
now__::_thesis:_for_G_being_Subset_of_X_holds_
(_not_G_is_closed_or_A_misses_G_or_A_c=_G_)
let G be Subset of X; ::_thesis: ( not G is closed or A misses G or A c= G )
assume A2: G is closed ; ::_thesis: ( A misses G or A c= G )
now__::_thesis:_(_A_misses_G_or_A_c=_G_)
percases ( G is empty or not G is empty ) ;
suppose G is empty ; ::_thesis: ( A misses G or A c= G )
hence ( A misses G or A c= G ) by XBOOLE_1:65; ::_thesis: verum
end;
suppose not G is empty ; ::_thesis: ( A misses G or A c= G )
then consider X0 being non empty strict closed SubSpace of X such that
A3: G = the carrier of X0 by A2, TSEP_1:15;
( Y0 misses X0 or Y0 is SubSpace of X0 ) by A1;
hence ( A misses G or A c= G ) by A3, TSEP_1:4, TSEP_1:def_3; ::_thesis: verum
end;
end;
end;
hence ( A misses G or A c= G ) ; ::_thesis: verum
end;
then A is anti-discrete by Def4;
hence Y0 is anti-discrete by Th67; ::_thesis: verum
end;
theorem :: TEX_4:70
for X being non empty TopSpace
for Y0 being anti-discrete SubSpace of X
for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 )
proof
let X be non empty TopSpace; ::_thesis: for Y0 being anti-discrete SubSpace of X
for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 )
let Y0 be anti-discrete SubSpace of X; ::_thesis: for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 )
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
let X0 be open SubSpace of X; ::_thesis: ( Y0 misses X0 or Y0 is SubSpace of X0 )
reconsider G = the carrier of X0 as Subset of X by TSEP_1:1;
A1: G is open by TSEP_1:16;
A is anti-discrete by Th66;
then ( A misses G or A c= G ) by A1, Def3;
hence ( Y0 misses X0 or Y0 is SubSpace of X0 ) by TSEP_1:4, TSEP_1:def_3; ::_thesis: verum
end;
theorem :: TEX_4:71
for X being non empty TopSpace
for Y0 being anti-discrete SubSpace of X
for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 )
proof
let X be non empty TopSpace; ::_thesis: for Y0 being anti-discrete SubSpace of X
for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 )
let Y0 be anti-discrete SubSpace of X; ::_thesis: for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 )
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
let X0 be closed SubSpace of X; ::_thesis: ( Y0 misses X0 or Y0 is SubSpace of X0 )
reconsider G = the carrier of X0 as Subset of X by TSEP_1:1;
A1: G is closed by TSEP_1:11;
A is anti-discrete by Th66;
then ( A misses G or A c= G ) by A1, Def4;
hence ( Y0 misses X0 or Y0 is SubSpace of X0 ) by TSEP_1:4, TSEP_1:def_3; ::_thesis: verum
end;
definition
let Y be non empty TopStruct ;
let IT be SubSpace of Y;
attrIT is maximal_anti-discrete means :Def16: :: TEX_4:def 16
( IT is anti-discrete & ( for Y0 being SubSpace of Y st Y0 is anti-discrete & the carrier of IT c= the carrier of Y0 holds
the carrier of IT = the carrier of Y0 ) );
end;
:: deftheorem Def16 defines maximal_anti-discrete TEX_4:def_16_:_
for Y being non empty TopStruct
for IT being SubSpace of Y holds
( IT is maximal_anti-discrete iff ( IT is anti-discrete & ( for Y0 being SubSpace of Y st Y0 is anti-discrete & the carrier of IT c= the carrier of Y0 holds
the carrier of IT = the carrier of Y0 ) ) );
registration
let Y be non empty TopStruct ;
cluster maximal_anti-discrete -> anti-discrete for SubSpace of Y;
coherence
for b1 being SubSpace of Y st b1 is maximal_anti-discrete holds
b1 is anti-discrete by Def16;
cluster non anti-discrete -> non maximal_anti-discrete for SubSpace of Y;
coherence
for b1 being SubSpace of Y st not b1 is anti-discrete holds
not b1 is maximal_anti-discrete ;
end;
theorem Th72: :: TEX_4:72
for X being non empty TopSpace
for Y0 being non empty SubSpace of X
for A being Subset of X st A = the carrier of Y0 holds
( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )
proof
let X be non empty TopSpace; ::_thesis: for Y0 being non empty SubSpace of X
for A being Subset of X st A = the carrier of Y0 holds
( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )
let Y0 be non empty SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of Y0 holds
( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )
let A be Subset of X; ::_thesis: ( A = the carrier of Y0 implies ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete ) )
assume A1: A = the carrier of Y0 ; ::_thesis: ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )
thus ( Y0 is maximal_anti-discrete implies A is maximal_anti-discrete ) ::_thesis: ( A is maximal_anti-discrete implies Y0 is maximal_anti-discrete )
proof
assume A2: Y0 is maximal_anti-discrete ; ::_thesis: A is maximal_anti-discrete
A3: now__::_thesis:_for_D_being_Subset_of_X_st_D_is_anti-discrete_&_A_c=_D_holds_
A_=_D
let D be Subset of X; ::_thesis: ( D is anti-discrete & A c= D implies A = D )
assume A4: D is anti-discrete ; ::_thesis: ( A c= D implies A = D )
assume A5: A c= D ; ::_thesis: A = D
then D <> {} by A1;
then consider X0 being non empty strict SubSpace of X such that
A6: D = the carrier of X0 by TSEP_1:10;
X0 is anti-discrete by A4, A6, Th67;
hence A = D by A1, A2, A5, A6, Def16; ::_thesis: verum
end;
A is anti-discrete by A1, A2, Th66;
hence A is maximal_anti-discrete by A3, Def7; ::_thesis: verum
end;
assume A7: A is maximal_anti-discrete ; ::_thesis: Y0 is maximal_anti-discrete
A8: now__::_thesis:_for_X0_being_SubSpace_of_X_st_X0_is_anti-discrete_&_the_carrier_of_Y0_c=_the_carrier_of_X0_holds_
the_carrier_of_Y0_=_the_carrier_of_X0
let X0 be SubSpace of X; ::_thesis: ( X0 is anti-discrete & the carrier of Y0 c= the carrier of X0 implies the carrier of Y0 = the carrier of X0 )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is anti-discrete ; ::_thesis: ( the carrier of Y0 c= the carrier of X0 implies the carrier of Y0 = the carrier of X0 )
then A9: D is anti-discrete by Th66;
assume the carrier of Y0 c= the carrier of X0 ; ::_thesis: the carrier of Y0 = the carrier of X0
hence the carrier of Y0 = the carrier of X0 by A1, A7, A9, Def7; ::_thesis: verum
end;
A is anti-discrete by A7, Def7;
then Y0 is anti-discrete by A1, Th67;
hence Y0 is maximal_anti-discrete by A8, Def16; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster non empty open anti-discrete -> non empty maximal_anti-discrete for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is open & b1 is anti-discrete holds
b1 is maximal_anti-discrete
proof
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is open & X0 is anti-discrete implies X0 is maximal_anti-discrete )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is open ; ::_thesis: ( not X0 is anti-discrete or X0 is maximal_anti-discrete )
then A1: A is open by TSEP_1:16;
assume X0 is anti-discrete ; ::_thesis: X0 is maximal_anti-discrete
then A is anti-discrete by Th66;
then A is maximal_anti-discrete by A1, Th16;
hence X0 is maximal_anti-discrete by Th72; ::_thesis: verum
end;
cluster non empty open non maximal_anti-discrete -> non empty non anti-discrete for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is open & not b1 is maximal_anti-discrete holds
not b1 is anti-discrete ;
cluster non empty anti-discrete non maximal_anti-discrete -> non empty non open for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is anti-discrete & not b1 is maximal_anti-discrete holds
not b1 is open ;
cluster non empty closed anti-discrete -> non empty maximal_anti-discrete for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is closed & b1 is anti-discrete holds
b1 is maximal_anti-discrete
proof
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is closed & X0 is anti-discrete implies X0 is maximal_anti-discrete )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is closed ; ::_thesis: ( not X0 is anti-discrete or X0 is maximal_anti-discrete )
then A2: A is closed by TSEP_1:11;
assume X0 is anti-discrete ; ::_thesis: X0 is maximal_anti-discrete
then A is anti-discrete by Th66;
then A is maximal_anti-discrete by A2, Th17;
hence X0 is maximal_anti-discrete by Th72; ::_thesis: verum
end;
cluster non empty closed non maximal_anti-discrete -> non empty non anti-discrete for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is closed & not b1 is maximal_anti-discrete holds
not b1 is anti-discrete ;
cluster non empty anti-discrete non maximal_anti-discrete -> non empty non closed for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is anti-discrete & not b1 is maximal_anti-discrete holds
not b1 is closed ;
end;
definition
let Y be TopStruct ;
let x be Point of Y;
func MaxADSspace x -> strict SubSpace of Y means :Def17: :: TEX_4:def 17
the carrier of it = MaxADSet x;
existence
ex b1 being strict SubSpace of Y st the carrier of b1 = MaxADSet x
proof
set D = MaxADSet x;
set Y0 = Y | (MaxADSet x);
take Y | (MaxADSet x) ; ::_thesis: the carrier of (Y | (MaxADSet x)) = MaxADSet x
MaxADSet x = [#] (Y | (MaxADSet x)) by PRE_TOPC:def_5;
hence the carrier of (Y | (MaxADSet x)) = MaxADSet x ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict SubSpace of Y st the carrier of b1 = MaxADSet x & the carrier of b2 = MaxADSet x holds
b1 = b2
proof
let Y1, Y2 be strict SubSpace of Y; ::_thesis: ( the carrier of Y1 = MaxADSet x & the carrier of Y2 = MaxADSet x implies Y1 = Y2 )
assume that
A1: the carrier of Y1 = MaxADSet x and
A2: the carrier of Y2 = MaxADSet x ; ::_thesis: Y1 = Y2
set A1 = the carrier of Y1;
set A2 = the carrier of Y2;
A3: the carrier of Y2 = [#] Y2 ;
A4: the carrier of Y1 = [#] Y1 ;
then the carrier of Y1 c= [#] Y by PRE_TOPC:def_4;
then reconsider A1 = the carrier of Y1 as Subset of Y ;
Y1 = Y | A1 by A4, PRE_TOPC:def_5;
hence Y1 = Y2 by A1, A2, A3, PRE_TOPC:def_5; ::_thesis: verum
end;
end;
:: deftheorem Def17 defines MaxADSspace TEX_4:def_17_:_
for Y being TopStruct
for x being Point of Y
for b3 being strict SubSpace of Y holds
( b3 = MaxADSspace x iff the carrier of b3 = MaxADSet x );
registration
let Y be non empty TopStruct ;
let x be Point of Y;
cluster MaxADSspace x -> non empty strict ;
coherence
not MaxADSspace x is empty
proof
the carrier of (MaxADSspace x) = MaxADSet x by Def17;
hence not the carrier of (MaxADSspace x) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
Lm2: for Y being non empty TopStruct
for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds
X1 is SubSpace of X2
proof
let Y be non empty TopStruct ; ::_thesis: for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds
X1 is SubSpace of X2
let X1, X2 be SubSpace of Y; ::_thesis: ( the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2 )
set A1 = the carrier of X1;
set A2 = the carrier of X2;
A1: the carrier of X1 = [#] X1 ;
assume A2: the carrier of X1 c= the carrier of X2 ; ::_thesis: X1 is SubSpace of X2
A3: the carrier of X2 = [#] X2 ;
for P being Subset of X1 holds
( P in the topology of X1 iff ex Q being Subset of X2 st
( Q in the topology of X2 & P = Q /\ the carrier of X1 ) )
proof
let P be Subset of X1; ::_thesis: ( P in the topology of X1 iff ex Q being Subset of X2 st
( Q in the topology of X2 & P = Q /\ the carrier of X1 ) )
thus ( P in the topology of X1 implies ex Q being Subset of X2 st
( Q in the topology of X2 & P = Q /\ the carrier of X1 ) ) ::_thesis: ( ex Q being Subset of X2 st
( Q in the topology of X2 & P = Q /\ the carrier of X1 ) implies P in the topology of X1 )
proof
assume P in the topology of X1 ; ::_thesis: ex Q being Subset of X2 st
( Q in the topology of X2 & P = Q /\ the carrier of X1 )
then consider R being Subset of Y such that
A4: R in the topology of Y and
A5: P = R /\ the carrier of X1 by A1, PRE_TOPC:def_4;
reconsider Q = R /\ the carrier of X2 as Subset of X2 by XBOOLE_1:17;
take Q ; ::_thesis: ( Q in the topology of X2 & P = Q /\ the carrier of X1 )
thus Q in the topology of X2 by A3, A4, PRE_TOPC:def_4; ::_thesis: P = Q /\ the carrier of X1
Q /\ the carrier of X1 = R /\ ( the carrier of X2 /\ the carrier of X1) by XBOOLE_1:16
.= R /\ the carrier of X1 by A2, XBOOLE_1:28 ;
hence P = Q /\ the carrier of X1 by A5; ::_thesis: verum
end;
given Q being Subset of X2 such that A6: Q in the topology of X2 and
A7: P = Q /\ the carrier of X1 ; ::_thesis: P in the topology of X1
consider R being Subset of Y such that
A8: R in the topology of Y and
A9: Q = R /\ ([#] X2) by A6, PRE_TOPC:def_4;
P = R /\ ( the carrier of X2 /\ the carrier of X1) by A7, A9, XBOOLE_1:16
.= R /\ the carrier of X1 by A2, XBOOLE_1:28 ;
hence P in the topology of X1 by A1, A8, PRE_TOPC:def_4; ::_thesis: verum
end;
hence X1 is SubSpace of X2 by A1, A3, A2, PRE_TOPC:def_4; ::_thesis: verum
end;
theorem :: TEX_4:73
for Y being non empty TopStruct
for x being Point of Y holds Sspace x is SubSpace of MaxADSspace x
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds Sspace x is SubSpace of MaxADSspace x
let x be Point of Y; ::_thesis: Sspace x is SubSpace of MaxADSspace x
A1: the carrier of (Sspace x) = {x} by TEX_2:def_2;
the carrier of (MaxADSspace x) = MaxADSet x by Def17;
hence Sspace x is SubSpace of MaxADSspace x by A1, Lm2, Th12; ::_thesis: verum
end;
theorem :: TEX_4:74
for Y being non empty TopStruct
for x, y being Point of Y holds
( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) )
proof
let Y be non empty TopStruct ; ::_thesis: for x, y being Point of Y holds
( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) )
let x, y be Point of Y; ::_thesis: ( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) )
A1: the carrier of (MaxADSspace x) = MaxADSet x by Def17;
thus ( y is Point of (MaxADSspace x) implies TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) ) ::_thesis: ( TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) implies y is Point of (MaxADSspace x) )
proof
assume y is Point of (MaxADSspace x) ; ::_thesis: TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #)
then MaxADSet y = MaxADSet x by A1, Th21;
hence TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) by A1, Def17; ::_thesis: verum
end;
assume A2: TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) ; ::_thesis: y is Point of (MaxADSspace x)
the carrier of (MaxADSspace y) = MaxADSet y by Def17;
hence y is Point of (MaxADSspace x) by A2, Th21; ::_thesis: verum
end;
theorem :: TEX_4:75
for Y being non empty TopStruct
for x, y being Point of Y holds
( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) )
proof
let Y be non empty TopStruct ; ::_thesis: for x, y being Point of Y holds
( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) )
let x, y be Point of Y; ::_thesis: ( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) )
assume A1: the carrier of (MaxADSspace x) meets the carrier of (MaxADSspace y) ; ::_thesis: TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #)
A2: the carrier of (MaxADSspace y) = MaxADSet y by Def17;
the carrier of (MaxADSspace x) = MaxADSet x by Def17;
hence TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) by A2, A1, Th22, TSEP_1:5; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster strict TopSpace-like maximal_anti-discrete for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is maximal_anti-discrete & b1 is strict )
proof
consider a being set such that
A1: a in the carrier of X by XBOOLE_0:def_1;
reconsider a = a as Point of X by A1;
consider X0 being non empty strict SubSpace of X such that
A2: MaxADSet a = the carrier of X0 by TSEP_1:10;
take X0 ; ::_thesis: ( X0 is maximal_anti-discrete & X0 is strict )
MaxADSet a is maximal_anti-discrete by Th20;
hence ( X0 is maximal_anti-discrete & X0 is strict ) by A2, Th72; ::_thesis: verum
end;
end;
registration
let X be non empty TopSpace;
let x be Point of X;
cluster MaxADSspace x -> strict maximal_anti-discrete ;
coherence
MaxADSspace x is maximal_anti-discrete
proof
A1: MaxADSet x is maximal_anti-discrete by Th20;
MaxADSet x = the carrier of (MaxADSspace x) by Def17;
hence MaxADSspace x is maximal_anti-discrete by A1, Th72; ::_thesis: verum
end;
end;
theorem :: TEX_4:76
for X being non empty TopSpace
for X0 being non empty closed SubSpace of X
for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty closed SubSpace of X
for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0
let X0 be non empty closed SubSpace of X; ::_thesis: for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0
let x be Point of X; ::_thesis: ( x is Point of X0 implies MaxADSspace x is SubSpace of X0 )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: A is closed by TSEP_1:11;
assume x is Point of X0 ; ::_thesis: MaxADSspace x is SubSpace of X0
then MaxADSet x c= A by A1, Th23;
then the carrier of (MaxADSspace x) c= the carrier of X0 by Def17;
hence MaxADSspace x is SubSpace of X0 by Lm2; ::_thesis: verum
end;
theorem :: TEX_4:77
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty open SubSpace of X
for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0
let X0 be non empty open SubSpace of X; ::_thesis: for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0
let x be Point of X; ::_thesis: ( x is Point of X0 implies MaxADSspace x is SubSpace of X0 )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: A is open by TSEP_1:16;
assume x is Point of X0 ; ::_thesis: MaxADSspace x is SubSpace of X0
then MaxADSet x c= A by A1, Th24;
then the carrier of (MaxADSspace x) c= the carrier of X0 by Def17;
hence MaxADSspace x is SubSpace of X0 by Lm2; ::_thesis: verum
end;
theorem :: TEX_4:78
for X being non empty TopSpace
for x being Point of X st Cl {x} = {x} holds
Sspace x is maximal_anti-discrete
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X st Cl {x} = {x} holds
Sspace x is maximal_anti-discrete
let x be Point of X; ::_thesis: ( Cl {x} = {x} implies Sspace x is maximal_anti-discrete )
assume Cl {x} = {x} ; ::_thesis: Sspace x is maximal_anti-discrete
then A1: {x} is maximal_anti-discrete by Th45;
the carrier of (Sspace x) = {x} by TEX_2:def_2;
hence Sspace x is maximal_anti-discrete by A1, Th72; ::_thesis: verum
end;
notation
let Y be TopStruct ;
let A be Subset of Y;
synonym Sspace A for Y | A;
end;
Lm3: for Y being TopStruct
for A being Subset of Y holds the carrier of (Y | A) = A
proof
let Y be TopStruct ; ::_thesis: for A being Subset of Y holds the carrier of (Y | A) = A
let A be Subset of Y; ::_thesis: the carrier of (Y | A) = A
[#] (Y | A) = A by PRE_TOPC:def_5;
hence the carrier of (Y | A) = A ; ::_thesis: verum
end;
theorem :: TEX_4:79
for Y being non empty TopStruct
for A being non empty Subset of Y holds A is Subset of (Sspace A)
proof
let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y holds A is Subset of (Sspace A)
let A be non empty Subset of Y; ::_thesis: A is Subset of (Sspace A)
the carrier of (Sspace A) c= the carrier of (Sspace A) ;
hence A is Subset of (Sspace A) by Lm3; ::_thesis: verum
end;
theorem :: TEX_4:80
for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being non empty Subset of Y st A is Subset of Y0 holds
Sspace A is SubSpace of Y0
proof
let Y be non empty TopStruct ; ::_thesis: for Y0 being SubSpace of Y
for A being non empty Subset of Y st A is Subset of Y0 holds
Sspace A is SubSpace of Y0
let Y0 be SubSpace of Y; ::_thesis: for A being non empty Subset of Y st A is Subset of Y0 holds
Sspace A is SubSpace of Y0
let A be non empty Subset of Y; ::_thesis: ( A is Subset of Y0 implies Sspace A is SubSpace of Y0 )
assume A is Subset of Y0 ; ::_thesis: Sspace A is SubSpace of Y0
then A c= the carrier of Y0 ;
then the carrier of (Sspace A) c= the carrier of Y0 by Lm3;
hence Sspace A is SubSpace of Y0 by Lm2; ::_thesis: verum
end;
registration
let Y be non trivial TopStruct ;
cluster strict non proper for SubSpace of Y;
existence
ex b1 being SubSpace of Y st
( not b1 is proper & b1 is strict )
proof
[#] Y = the carrier of Y ;
then reconsider A0 = the carrier of Y as non empty Subset of Y ;
set Y0 = Y | A0;
take Y | A0 ; ::_thesis: ( not Y | A0 is proper & Y | A0 is strict )
A0 = [#] (Y | A0) by PRE_TOPC:def_5;
hence ( not Y | A0 is proper & Y | A0 is strict ) by TEX_2:10; ::_thesis: verum
end;
end;
registration
let Y be non trivial TopStruct ;
let A be non trivial Subset of Y;
cluster Sspace A -> non trivial ;
coherence
not Sspace A is trivial by Lm3;
end;
registration
let Y be non empty TopStruct ;
let A be non proper Subset of Y;
cluster Sspace A -> non proper ;
coherence
not Sspace A is proper
proof
now__::_thesis:_not_Sspace_A_is_proper
assume A1: Sspace A is proper ; ::_thesis: contradiction
the carrier of (Sspace A) = A by Lm3;
hence contradiction by A1, TEX_2:8; ::_thesis: verum
end;
hence not Sspace A is proper ; ::_thesis: verum
end;
end;
definition
let Y be non empty TopStruct ;
let A be Subset of Y;
func MaxADSspace A -> strict SubSpace of Y means :Def18: :: TEX_4:def 18
the carrier of it = MaxADSet A;
existence
ex b1 being strict SubSpace of Y st the carrier of b1 = MaxADSet A
proof
set D = MaxADSet A;
set Y0 = Y | (MaxADSet A);
take Y | (MaxADSet A) ; ::_thesis: the carrier of (Y | (MaxADSet A)) = MaxADSet A
MaxADSet A = [#] (Y | (MaxADSet A)) by PRE_TOPC:def_5;
hence the carrier of (Y | (MaxADSet A)) = MaxADSet A ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict SubSpace of Y st the carrier of b1 = MaxADSet A & the carrier of b2 = MaxADSet A holds
b1 = b2
proof
let Y1, Y2 be strict SubSpace of Y; ::_thesis: ( the carrier of Y1 = MaxADSet A & the carrier of Y2 = MaxADSet A implies Y1 = Y2 )
assume that
A1: the carrier of Y1 = MaxADSet A and
A2: the carrier of Y2 = MaxADSet A ; ::_thesis: Y1 = Y2
set A1 = the carrier of Y1;
set A2 = the carrier of Y2;
A3: the carrier of Y2 = [#] Y2 ;
A4: the carrier of Y1 = [#] Y1 ;
then the carrier of Y1 c= [#] Y by PRE_TOPC:def_4;
then reconsider A1 = the carrier of Y1 as Subset of Y ;
Y1 = Y | A1 by A4, PRE_TOPC:def_5;
hence Y1 = Y2 by A1, A2, A3, PRE_TOPC:def_5; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines MaxADSspace TEX_4:def_18_:_
for Y being non empty TopStruct
for A being Subset of Y
for b3 being strict SubSpace of Y holds
( b3 = MaxADSspace A iff the carrier of b3 = MaxADSet A );
registration
let Y be non empty TopStruct ;
let A be non empty Subset of Y;
cluster MaxADSspace A -> non empty strict ;
coherence
not MaxADSspace A is empty
proof
the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence not the carrier of (MaxADSspace A) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
theorem :: TEX_4:81
for Y being non empty TopStruct
for A being non empty Subset of Y holds A is Subset of (MaxADSspace A)
proof
let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y holds A is Subset of (MaxADSspace A)
let A be non empty Subset of Y; ::_thesis: A is Subset of (MaxADSspace A)
the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence A is Subset of (MaxADSspace A) by Th32; ::_thesis: verum
end;
theorem :: TEX_4:82
for Y being non empty TopStruct
for A being non empty Subset of Y holds Sspace A is SubSpace of MaxADSspace A
proof
let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y holds Sspace A is SubSpace of MaxADSspace A
let A be non empty Subset of Y; ::_thesis: Sspace A is SubSpace of MaxADSspace A
A1: the carrier of (Sspace A) = A by Lm3;
the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence Sspace A is SubSpace of MaxADSspace A by A1, Lm2, Th32; ::_thesis: verum
end;
theorem :: TEX_4:83
for Y being non empty TopStruct
for x being Point of Y holds TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #)
proof
let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #)
let x be Point of Y; ::_thesis: TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #)
A1: the carrier of (MaxADSspace {x}) = MaxADSet {x} by Def18;
the carrier of (MaxADSspace x) = MaxADSet x by Def17;
hence TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #) by A1, Th28, TSEP_1:5; ::_thesis: verum
end;
theorem :: TEX_4:84
for Y being non empty TopStruct
for A, B being non empty Subset of Y st A c= B holds
MaxADSspace A is SubSpace of MaxADSspace B
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being non empty Subset of Y st A c= B holds
MaxADSspace A is SubSpace of MaxADSspace B
let A, B be non empty Subset of Y; ::_thesis: ( A c= B implies MaxADSspace A is SubSpace of MaxADSspace B )
assume A1: A c= B ; ::_thesis: MaxADSspace A is SubSpace of MaxADSspace B
A2: the carrier of (MaxADSspace B) = MaxADSet B by Def18;
the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence MaxADSspace A is SubSpace of MaxADSspace B by A2, A1, Lm2, Th31; ::_thesis: verum
end;
theorem :: TEX_4:85
for Y being non empty TopStruct
for A being non empty Subset of Y holds TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #)
proof
let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y holds TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #)
let A be non empty Subset of Y; ::_thesis: TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #)
A1: the carrier of (MaxADSspace (MaxADSet A)) = MaxADSet (MaxADSet A) by Def18;
the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #) by A1, Th33, TSEP_1:5; ::_thesis: verum
end;
theorem :: TEX_4:86
for Y being non empty TopStruct
for A, B being non empty Subset of Y st A is Subset of (MaxADSspace B) holds
MaxADSspace A is SubSpace of MaxADSspace B
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being non empty Subset of Y st A is Subset of (MaxADSspace B) holds
MaxADSspace A is SubSpace of MaxADSspace B
let A, B be non empty Subset of Y; ::_thesis: ( A is Subset of (MaxADSspace B) implies MaxADSspace A is SubSpace of MaxADSspace B )
assume A1: A is Subset of (MaxADSspace B) ; ::_thesis: MaxADSspace A is SubSpace of MaxADSspace B
A2: the carrier of (MaxADSspace B) = MaxADSet B by Def18;
the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence MaxADSspace A is SubSpace of MaxADSspace B by A2, A1, Lm2, Th34; ::_thesis: verum
end;
theorem :: TEX_4:87
for Y being non empty TopStruct
for A, B being non empty Subset of Y holds
( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) )
proof
let Y be non empty TopStruct ; ::_thesis: for A, B being non empty Subset of Y holds
( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) )
let A, B be non empty Subset of Y; ::_thesis: ( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) )
A1: the carrier of (MaxADSspace B) = MaxADSet B by Def18;
A2: the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) implies TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) ) by A1, Th35, TSEP_1:5; ::_thesis: ( TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) implies ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) )
assume TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) ; ::_thesis: ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) )
hence ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) by A2, A1, Th32; ::_thesis: verum
end;
registration
let Y be non trivial TopStruct ;
let A be non trivial Subset of Y;
cluster MaxADSspace A -> non trivial strict ;
coherence
not MaxADSspace A is trivial
proof
not MaxADSet A is trivial ;
hence not MaxADSspace A is trivial by Def18; ::_thesis: verum
end;
end;
registration
let Y be non empty TopStruct ;
let A be non proper Subset of Y;
cluster MaxADSspace A -> strict non proper ;
coherence
not MaxADSspace A is proper
proof
now__::_thesis:_not_MaxADSspace_A_is_proper
assume A1: MaxADSspace A is proper ; ::_thesis: contradiction
the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence contradiction by A1, TEX_2:8; ::_thesis: verum
end;
hence not MaxADSspace A is proper ; ::_thesis: verum
end;
end;
theorem :: TEX_4:88
for X being non empty TopSpace
for X0 being open SubSpace of X
for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0
proof
let X be non empty TopSpace; ::_thesis: for X0 being open SubSpace of X
for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0
let X0 be open SubSpace of X; ::_thesis: for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0
let A be non empty Subset of X; ::_thesis: ( A is Subset of X0 implies MaxADSspace A is SubSpace of X0 )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
A1: D is open by TSEP_1:16;
assume A is Subset of X0 ; ::_thesis: MaxADSspace A is SubSpace of X0
then MaxADSet A c= D by A1, Th38;
then the carrier of (MaxADSspace A) c= the carrier of X0 by Def18;
hence MaxADSspace A is SubSpace of X0 by Lm2; ::_thesis: verum
end;
theorem :: TEX_4:89
for X being non empty TopSpace
for X0 being closed SubSpace of X
for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0
proof
let X be non empty TopSpace; ::_thesis: for X0 being closed SubSpace of X
for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0
let X0 be closed SubSpace of X; ::_thesis: for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0
let A be non empty Subset of X; ::_thesis: ( A is Subset of X0 implies MaxADSspace A is SubSpace of X0 )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
A1: D is closed by TSEP_1:11;
assume A is Subset of X0 ; ::_thesis: MaxADSspace A is SubSpace of X0
then MaxADSet A c= D by A1, Th40;
then the carrier of (MaxADSspace A) c= the carrier of X0 by Def18;
hence MaxADSspace A is SubSpace of X0 by Lm2; ::_thesis: verum
end;