:: The Lattice of Domains of an Extremally Disconnected Space
:: by Zbigniew Karno
::
:: Received August 27, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

theorem Th1: :: TDLAT_3:1
for X being TopSpace
for C being Subset of X holds Cl C = (Int (C `)) `
proofend;

theorem Th2: :: TDLAT_3:2
for X being TopSpace
for C being Subset of X holds Cl (C `) = (Int C) `
proofend;

theorem Th3: :: TDLAT_3:3
for X being TopSpace
for C being Subset of X holds Int (C `) = (Cl C) `
proofend;

theorem :: TDLAT_3:4
for X being TopSpace
for A, B being Subset of X st A \/ B = the carrier of X & A is closed holds
A \/ (Int B) = the carrier of X
proofend;

theorem Th5: :: TDLAT_3:5
for X being TopSpace
for A being Subset of X holds
( ( A is open & A is closed ) iff Cl A = Int A )
proofend;

theorem :: TDLAT_3:6
for X being TopSpace
for A being Subset of X st A is open & A is closed holds
Int (Cl A) = Cl (Int A)
proofend;

::Properties of Domains.
theorem Th7: :: TDLAT_3:7
for X being TopSpace
for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds
( A is open_condensed & A is closed_condensed )
proofend;

theorem Th8: :: TDLAT_3:8
for X being TopSpace
for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds
( A is open & A is closed )
proofend;

theorem Th9: :: TDLAT_3:9
for X being TopSpace
for A being Subset of X st A is condensed holds
( Int (Cl A) = Int A & Cl A = Cl (Int A) )
proofend;

begin

:: 2. Discrete Topological Structures.
definition
let IT be TopStruct ;
attrIT is discrete  means :Def1: :: TDLAT_3:def 1
 the topology of IT = bool the carrier of IT;
attrIT is anti-discrete  means :Def2: :: TDLAT_3:def 2
 the topology of IT = {{}, the carrier of IT};
end;

:: deftheorem Def1 defines discrete TDLAT_3:def_1_:_
 for IT being TopStruct holds
( IT is discrete iff the topology of IT = bool the carrier of IT );

:: deftheorem Def2 defines anti-discrete TDLAT_3:def_2_:_
 for IT being TopStruct holds
( IT is anti-discrete iff the topology of IT = {{}, the carrier of IT} );

theorem :: TDLAT_3:10
for Y being TopStruct st Y is discrete & Y is anti-discrete holds
bool the carrier of Y = {{}, the carrier of Y}
proofend;

theorem Th11: :: TDLAT_3:11
for Y being TopStruct st {} in the topology of Y & the carrier of Y in the topology of Y & bool the carrier of Y = {{}, the carrier of Y} holds
( Y is discrete & Y is anti-discrete )
proofend;

registration
cluster non empty strict discrete anti-discrete for TopStruct ;
existence
 ex b1 being TopStruct st
( b1 is discrete & b1 is anti-discrete & b1 is strict & not b1 is empty )
proofend;
end;

theorem Th12: :: TDLAT_3:12
for Y being discrete TopStruct
for A being Subset of Y holds the carrier of Y \ A in the topology of Y
proofend;

theorem Th13: :: TDLAT_3:13
for Y being anti-discrete TopStruct
for A being Subset of Y st A in the topology of Y holds
the carrier of Y \ A in the topology of Y
proofend;

registration
cluster discrete  ->  TopSpace-like for TopStruct ;
coherence
 for b1 being TopStruct st b1 is discrete holds
b1 is TopSpace-like
proofend;
cluster anti-discrete  ->  TopSpace-like for TopStruct ;
coherence
 for b1 being TopStruct st b1 is anti-discrete holds
b1 is TopSpace-like
proofend;
end;

theorem :: TDLAT_3:14
for Y being TopSpace-like TopStruct st bool the carrier of Y = {{}, the carrier of Y} holds
( Y is discrete & Y is anti-discrete )
proofend;

definition
let IT be TopStruct ;
attrIT is almost_discrete  means :Def3: :: TDLAT_3:def 3
 for A being Subset of IT st A in the topology of IT holds
the carrier of IT \ A in the topology of IT;
end;

:: deftheorem Def3 defines almost_discrete TDLAT_3:def_3_:_
 for IT being TopStruct holds
( IT is almost_discrete iff for A being Subset of IT st A in the topology of IT holds
the carrier of IT \ A in the topology of IT );

registration
cluster discrete  ->  almost_discrete for TopStruct ;
coherence
 for b1 being TopStruct st b1 is discrete holds
b1 is almost_discrete
proofend;
cluster anti-discrete  ->  almost_discrete for TopStruct ;
coherence
 for b1 being TopStruct st b1 is anti-discrete holds
b1 is almost_discrete
proofend;
end;

registration
cluster strict almost_discrete for TopStruct ;
existence
 ex b1 being TopStruct st
( b1 is almost_discrete & b1 is strict )
proofend;
end;

begin

:: 3. Discrete Topological Spaces.
registration
cluster non empty strict TopSpace-like discrete anti-discrete for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is discrete & b1 is anti-discrete & b1 is strict & not b1 is empty )
proofend;
end;

theorem Th15: :: TDLAT_3:15
for X being TopSpace holds
( X is discrete iff for A being Subset of X holds A is open )
proofend;

theorem Th16: :: TDLAT_3:16
for X being TopSpace holds
( X is discrete iff for A being Subset of X holds A is closed )
proofend;

theorem Th17: :: TDLAT_3:17
for X being TopSpace st ( for A being Subset of X
for x being Point of X st A = {x} holds
A is open ) holds
X is discrete
proofend;

registration
let X be non empty discrete TopSpace;
cluster  ->  closed open discrete for SubSpace of X;
coherence
 for b1 being SubSpace of X holds
( b1 is open & b1 is closed & b1 is discrete )
proofend;
end;

registration
let X be non empty discrete TopSpace;
cluster strict TopSpace-like closed open discrete almost_discrete for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is discrete & b1 is strict )
proofend;
end;

theorem Th18: :: TDLAT_3:18
for X being TopSpace holds
( X is anti-discrete iff for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) )
proofend;

theorem Th19: :: TDLAT_3:19
for X being TopSpace holds
( X is anti-discrete iff for A being Subset of X holds
( not A is closed or A = {} or A = the carrier of X ) )
proofend;

theorem :: TDLAT_3:20
for X being TopSpace st ( for A being Subset of X
for x being Point of X st A = {x} holds
Cl A = the carrier of X ) holds
X is anti-discrete
proofend;

registration
let X be non empty anti-discrete TopSpace;
cluster  ->  anti-discrete for SubSpace of X;
coherence
 for b1 being SubSpace of X holds b1 is anti-discrete
proofend;
end;

registration
let X be non empty anti-discrete TopSpace;
cluster TopSpace-like anti-discrete almost_discrete for SubSpace of X;
existence
 ex b1 being SubSpace of X st b1 is anti-discrete
proofend;
end;

theorem Th21: :: TDLAT_3:21
for X being TopSpace holds
( X is almost_discrete iff for A being Subset of X st A is open holds
A is closed )
proofend;

theorem Th22: :: TDLAT_3:22
for X being TopSpace holds
( X is almost_discrete iff for A being Subset of X st A is closed holds
A is open )
proofend;

theorem :: TDLAT_3:23
for X being TopSpace holds
( X is almost_discrete iff for A being Subset of X st A is open holds
Cl A = A )
proofend;

theorem :: TDLAT_3:24
for X being TopSpace holds
( X is almost_discrete iff for A being Subset of X st A is closed holds
Int A = A )
proofend;

registration
cluster strict TopSpace-like almost_discrete for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is almost_discrete & b1 is strict )
proofend;
end;

theorem :: TDLAT_3:25
for X being TopSpace st ( for A being Subset of X
for x being Point of X st A = {x} holds
Cl A is open ) holds
X is almost_discrete
proofend;

theorem :: TDLAT_3:26
for X being TopSpace holds
( X is discrete iff ( X is almost_discrete & ( for A being Subset of X
for x being Point of X st A = {x} holds
A is closed ) ) )
proofend;

registration
cluster TopSpace-like discrete  ->  almost_discrete for TopStruct ;
coherence
 for b1 being TopSpace st b1 is discrete holds
b1 is almost_discrete ;
cluster TopSpace-like anti-discrete  ->  almost_discrete for TopStruct ;
coherence
 for b1 being TopSpace st b1 is anti-discrete holds
b1 is almost_discrete ;
end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty  ->  non empty almost_discrete for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X holds b1 is almost_discrete
proofend;
end;

registration
let X be non empty almost_discrete TopSpace;
cluster open  ->  closed for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is open holds
b1 is closed
proofend;
cluster closed  ->  open for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is closed holds
b1 is open
proofend;
end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty strict TopSpace-like almost_discrete for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is almost_discrete & b1 is strict & not b1 is empty )
proofend;
end;

begin

:: 4. Extremally Disconnected Topological Spaces.
definition
let IT be non empty TopSpace;
attrIT is extremally_disconnected  means :Def4: :: TDLAT_3:def 4
 for A being Subset of IT st A is open holds
Cl A is open ;
end;

:: deftheorem Def4 defines extremally_disconnected TDLAT_3:def_4_:_
 for IT being non empty TopSpace holds
( IT is extremally_disconnected iff for A being Subset of IT st A is open holds
Cl A is open );

registration
cluster non empty strict TopSpace-like extremally_disconnected for TopStruct ;
existence
 ex b1 being non empty TopSpace st
( b1 is extremally_disconnected & b1 is strict )
proofend;
end;

theorem Th27: :: TDLAT_3:27
for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is closed holds
Int A is closed )
proofend;

theorem Th28: :: TDLAT_3:28
for X being non empty TopSpace holds
( X is extremally_disconnected iff for A, B being Subset of X st A is open & B is open & A misses B holds
Cl A misses Cl B )
proofend;

theorem :: TDLAT_3:29
for X being non empty TopSpace holds
( X is extremally_disconnected iff for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds
(Int A) \/ (Int B) = the carrier of X )
proofend;

theorem Th30: :: TDLAT_3:30
for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is open holds
Cl A = Int (Cl A) )
proofend;

theorem :: TDLAT_3:31
for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is closed holds
Int A = Cl (Int A) )
proofend;

theorem Th32: :: TDLAT_3:32
for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
( A is closed & A is open ) )
proofend;

theorem Th33: :: TDLAT_3:33
for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
( A is closed_condensed & A is open_condensed ) )
proofend;

theorem Th34: :: TDLAT_3:34
for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
Int (Cl A) = Cl (Int A) )
proofend;

theorem :: TDLAT_3:35
for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
Int A = Cl A )
proofend;

theorem Th36: :: TDLAT_3:36
for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X holds
( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) )
proofend;

definition
let IT be non empty TopSpace;
attrIT is hereditarily_extremally_disconnected  means :Def5: :: TDLAT_3:def 5
 for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected ;
end;

:: deftheorem Def5 defines hereditarily_extremally_disconnected TDLAT_3:def_5_:_
 for IT being non empty TopSpace holds
( IT is hereditarily_extremally_disconnected iff for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected );

registration
cluster non empty strict TopSpace-like hereditarily_extremally_disconnected for TopStruct ;
existence
 ex b1 being non empty TopSpace st
( b1 is hereditarily_extremally_disconnected & b1 is strict )
proofend;
end;

registration
cluster non empty TopSpace-like hereditarily_extremally_disconnected  ->  non empty extremally_disconnected for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is hereditarily_extremally_disconnected holds
b1 is extremally_disconnected
proofend;
cluster non empty TopSpace-like almost_discrete  ->  non empty hereditarily_extremally_disconnected for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is almost_discrete holds
b1 is hereditarily_extremally_disconnected
proofend;
end;

theorem Th37: :: TDLAT_3:37
for X being non empty extremally_disconnected TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X st A = the carrier of X0 & A is dense holds
X0 is extremally_disconnected
proofend;

registration
let X be non empty extremally_disconnected TopSpace;
cluster non empty open  ->  non empty extremally_disconnected for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is open holds
b1 is extremally_disconnected
proofend;
end;

registration
let X be non empty extremally_disconnected TopSpace;
cluster non empty strict TopSpace-like extremally_disconnected for SubSpace of X;
existence
 ex b1 being non empty SubSpace of X st
( b1 is extremally_disconnected & b1 is strict )
proofend;
end;

registration
let X be non empty hereditarily_extremally_disconnected TopSpace;
cluster non empty  ->  non empty hereditarily_extremally_disconnected for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X holds b1 is hereditarily_extremally_disconnected
proofend;
end;

registration
let X be non empty hereditarily_extremally_disconnected TopSpace;
cluster non empty strict TopSpace-like extremally_disconnected hereditarily_extremally_disconnected for SubSpace of X;
existence
 ex b1 being non empty SubSpace of X st
( b1 is hereditarily_extremally_disconnected & b1 is strict )
proofend;
end;

theorem :: TDLAT_3:38
for X being non empty TopSpace st ( for X0 being non empty closed SubSpace of X holds X0 is extremally_disconnected ) holds
X is hereditarily_extremally_disconnected
proofend;

begin

theorem Th39: :: TDLAT_3:39
for Y being non empty extremally_disconnected TopSpace holds Domains_of Y = Closed_Domains_of Y
proofend;

theorem Th40: :: TDLAT_3:40
for Y being non empty extremally_disconnected TopSpace holds
( D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y )
proofend;

theorem Th41: :: TDLAT_3:41
for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Closed_Domains_Lattice Y
proofend;

theorem Th42: :: TDLAT_3:42
for Y being non empty extremally_disconnected TopSpace holds Domains_of Y = Open_Domains_of Y
proofend;

theorem Th43: :: TDLAT_3:43
for Y being non empty extremally_disconnected TopSpace holds
( D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y )
proofend;

theorem Th44: :: TDLAT_3:44
for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Open_Domains_Lattice Y
proofend;

theorem Th45: :: TDLAT_3:45
for Y being non empty extremally_disconnected TopSpace
for A, B being Element of Domains_of Y holds
( (D-Union Y) . (A,B) = A \/ B & (D-Meet Y) . (A,B) = A /\ B )
proofend;

theorem :: TDLAT_3:46
for Y being non empty extremally_disconnected TopSpace
for a, b being Element of (Domains_Lattice Y)
for A, B being Element of Domains_of Y st a = A & b = B holds
( a "\/" b = A \/ B & a "/\" b = A /\ B )
proofend;

theorem :: TDLAT_3:47
for Y being non empty extremally_disconnected TopSpace
for F being Subset-Family of Y st F is domains-family holds
for S being Subset of (Domains_Lattice Y) st S = F holds
"\/" (S,(Domains_Lattice Y)) = Cl (union F)
proofend;

theorem :: TDLAT_3:48
for Y being non empty extremally_disconnected TopSpace
for F being Subset-Family of Y st F is domains-family holds
for S being Subset of (Domains_Lattice Y) st S = F holds
( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) &amp; ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) )
proofend;

theorem Th49: :: TDLAT_3:49
for X being non empty TopSpace holds
( X is extremally_disconnected iff Domains_Lattice X is M_Lattice )
proofend;

theorem :: TDLAT_3:50
for X being non empty TopSpace st Domains_Lattice X = Closed_Domains_Lattice X holds
X is extremally_disconnected by Th49;

theorem :: TDLAT_3:51
for X being non empty TopSpace st Domains_Lattice X = Open_Domains_Lattice X holds
X is extremally_disconnected by Th49;

theorem :: TDLAT_3:52
for X being non empty TopSpace holds X is extremally_disconnected
proofend;

theorem :: TDLAT_3:53
for X being non empty TopSpace holds
( X is extremally_disconnected iff Domains_Lattice X is B_Lattice )
proofend;