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

theorem Th1: :: TDLAT_3:1

for X being TopSpace
for C being Subset of X holds Cl C = (Int (C `)) `

proof end;

theorem Th2: :: TDLAT_3:2

for X being TopSpace
for C being Subset of X holds Cl (C `) = (Int C) `

proof end;

theorem Th3: :: TDLAT_3:3

for X being TopSpace
for C being Subset of X holds Int (C `) = (Cl C) `

proof end;

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

proof end;

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 )

proof end;

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)

proof end;

::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 )

proof end;

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 )

proof end;

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) )

proof end;

:: 2. Discrete Topological Structures.

definition

let IT be TopStruct ;

attr IT is discrete means :Def1: :: TDLAT_3:def 1
the topology of IT = bool the carrier of IT;

attr IT 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} ;

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 )

proof end;

registration

cluster non empty strict discrete anti-discrete for TopStruct ;

existence
ex b₁ being TopStruct st
( b₁ is discrete & b₁ is anti-discrete & b₁ is strict & not b₁ is empty )

proof end;

end;

theorem :: 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

proof end;

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

proof end;

registration

cluster discrete -> TopSpace-like for TopStruct ;

coherence
for b₁ being TopStruct st b₁ is discrete holds
b₁ is TopSpace-like

proof end;

cluster anti-discrete -> TopSpace-like for TopStruct ;

coherence
for b₁ being TopStruct st b₁ is anti-discrete holds
b₁ is TopSpace-like

proof end;

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 )

proof end;

definition

let IT be TopStruct ;

attr IT is almost_discrete means :: 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 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 b₁ being TopStruct st b₁ is discrete holds
b₁ is almost_discrete ;

cluster anti-discrete -> almost_discrete for TopStruct ;

coherence
for b₁ being TopStruct st b₁ is anti-discrete holds
b₁ is almost_discrete by Th13;

end;

registration

cluster strict almost_discrete for TopStruct ;

existence
ex b₁ being TopStruct st
( b₁ is almost_discrete & b₁ is strict )

proof end;

end;

:: 3. Discrete Topological Spaces.

registration

cluster non empty strict TopSpace-like discrete anti-discrete for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is discrete & b₁ is anti-discrete & b₁ is strict & not b₁ is empty )

proof end;

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 )

proof end;

theorem Th16: :: TDLAT_3:16

for X being TopSpace holds
( X is discrete iff for A being Subset of X holds A is closed )

proof end;

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

proof end;

registration

let X be non empty discrete TopSpace;

cluster -> closed open discrete for SubSpace of X;

coherence
for b₁ being SubSpace of X holds
( b₁ is open & b₁ is closed & b₁ is discrete )

proof end;

end;

registration

let X be non empty discrete TopSpace;

cluster strict TopSpace-like closed open discrete almost_discrete for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is discrete & b₁ is strict )

proof end;

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 ) )

proof end;

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 ) )

proof end;

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

proof end;

registration

let X be non empty anti-discrete TopSpace;

cluster -> anti-discrete for SubSpace of X;

coherence
for b₁ being SubSpace of X holds b₁ is anti-discrete

proof end;

end;

registration

let X be non empty anti-discrete TopSpace;

cluster TopSpace-like anti-discrete almost_discrete for SubSpace of X;

existence
ex b₁ being SubSpace of X st b₁ is anti-discrete

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

registration

cluster strict TopSpace-like almost_discrete for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is almost_discrete & b₁ is strict )

proof end;

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

proof end;

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 ) ) )

proof end;

registration

cluster TopSpace-like discrete -> almost_discrete for TopStruct ;

coherence
for b₁ being TopSpace st b₁ is discrete holds
b₁ is almost_discrete ;

cluster TopSpace-like anti-discrete -> almost_discrete for TopStruct ;

coherence
for b₁ being TopSpace st b₁ is anti-discrete holds
b₁ 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 b₁ being non empty SubSpace of X holds b₁ is almost_discrete

proof end;

end;

registration

let X be non empty almost_discrete TopSpace;

cluster open -> closed for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is open holds
b₁ is closed by Th21;

cluster closed -> open for SubSpace of X;

coherence
for b₁ being SubSpace of X st b₁ is closed holds
b₁ is open by Th22;

end;

registration

let X be non empty almost_discrete TopSpace;

cluster non empty strict TopSpace-like almost_discrete for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is almost_discrete & b₁ is strict & not b₁ is empty )

proof end;

end;

:: 4. Extremally Disconnected Topological Spaces.

definition

let IT be non empty TopSpace;

attr IT 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 b₁ being non empty TopSpace st
( b₁ is extremally_disconnected & b₁ is strict )

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

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) )

proof end;

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) )

proof end;

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 ) )

proof end;

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 ) )

proof end;

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) )

proof end;

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 )

proof end;

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 ) ) )

proof end;

definition

let IT be non empty TopSpace;

attr IT 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 b₁ being non empty TopSpace st
( b₁ is hereditarily_extremally_disconnected & b₁ is strict )

proof end;

end;

registration

cluster non empty TopSpace-like hereditarily_extremally_disconnected -> non empty extremally_disconnected for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is hereditarily_extremally_disconnected holds
b₁ is extremally_disconnected

proof end;

cluster non empty TopSpace-like almost_discrete -> non empty hereditarily_extremally_disconnected for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is almost_discrete holds
b₁ is hereditarily_extremally_disconnected

proof end;

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

proof end;

registration

let X be non empty extremally_disconnected TopSpace;

cluster non empty open -> non empty extremally_disconnected for SubSpace of X;

coherence
for b₁ being non empty SubSpace of X st b₁ is open holds
b₁ is extremally_disconnected

proof end;

end;

registration

let X be non empty extremally_disconnected TopSpace;

cluster non empty strict TopSpace-like extremally_disconnected for SubSpace of X;

existence
ex b₁ being non empty SubSpace of X st
( b₁ is extremally_disconnected & b₁ is strict )

proof end;

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 b₁ being non empty SubSpace of X holds b₁ is hereditarily_extremally_disconnected

proof end;

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 b₁ being non empty SubSpace of X st
( b₁ is hereditarily_extremally_disconnected & b₁ is strict )

proof end;

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

proof end;

theorem Th39: :: TDLAT_3:39

for Y being non empty extremally_disconnected TopSpace holds Domains_of Y = Closed_Domains_of Y

proof end;

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 )

proof end;

theorem Th41: :: TDLAT_3:41

for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Closed_Domains_Lattice Y

proof end;

theorem Th42: :: TDLAT_3:42

for Y being non empty extremally_disconnected TopSpace holds Domains_of Y = Open_Domains_of Y

proof end;

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 )

proof end;

theorem Th44: :: TDLAT_3:44

for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Open_Domains_Lattice Y

proof end;

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 )

proof end;

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 )

proof end;

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)

proof end;

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) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) )

proof end;

theorem Th49: :: TDLAT_3:49

for X being non empty TopSpace holds
( X is extremally_disconnected iff Domains_Lattice X is M_Lattice )

proof end;

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 st Closed_Domains_Lattice X = Open_Domains_Lattice X holds
X is extremally_disconnected

proof end;

theorem :: TDLAT_3:53

for X being non empty TopSpace holds
( X is extremally_disconnected iff Domains_Lattice X is B_Lattice )

proof end;