Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### The Lattice of Domains of an Extremally Disconnected Space

by
Zbigniew Karno

MML identifier: TDLAT_3
[ Mizar article, MML identifier index ]

```environ

vocabulary PRE_TOPC, TOPS_1, BOOLE, SUBSET_1, NATTRA_1, SETFAM_1, TARSKI,
TDLAT_1, RELAT_1, LATTICES, FUNCT_1, TDLAT_2, TDLAT_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, RELAT_1,
PRE_TOPC, TOPS_1, TOPS_2, PCOMPS_1, BORSUK_1, TSEP_1, BINOP_1, LATTICES,
LATTICE3, TDLAT_1, TDLAT_2;
constructors TOPS_1, TOPS_2, BORSUK_1, TSEP_1, LATTICE3, TDLAT_1, TDLAT_2,
PARTFUN1, MEMBERED;
clusters PRE_TOPC, BORSUK_1, TSEP_1, LATTICES, STRUCT_0, COMPLSP1, RELSET_1,
SUBSET_1, MEMBERED, ZFMISC_1;
requirements BOOLE, SUBSET;

begin
:: 1. Selected Properties of Subsets of a Topological Space.
reserve X for TopSpace;

::Properties of the Closure and the Interior Operators.
reserve C for Subset of X;

canceled;

theorem :: TDLAT_3:2
Cl C = (Int C`)`;

theorem :: TDLAT_3:3
Cl C` = (Int C)`;

theorem :: TDLAT_3:4
Int C` =  (Cl C)`;

reserve A, B for Subset of X;

canceled;

theorem :: TDLAT_3:6
A \/ B = the carrier of X implies
(A is closed implies A \/ Int B = the carrier of X) &
(B is closed implies Int A \/ B = the carrier of X);

theorem :: TDLAT_3:7
A is open & A is closed iff Cl A = Int A;

theorem :: TDLAT_3:8
A is open & A is closed implies Int Cl A = Cl Int A;

::Properties of Domains.
theorem :: TDLAT_3:9
A is condensed & Cl Int A c= Int Cl A implies
A is open_condensed & A is closed_condensed;

theorem :: TDLAT_3:10
A is condensed & Cl Int A c= Int Cl A implies A is open & A is closed;

theorem :: TDLAT_3:11
A is condensed implies Int Cl A = Int A & Cl A = Cl Int A;

begin
:: 2. Discrete Topological Structures.

definition let IT be TopStruct;
attr IT is discrete means
:: TDLAT_3:def 1
the topology of IT = bool the carrier of IT;
attr IT is anti-discrete means
:: TDLAT_3:def 2
the topology of IT = {{}, the carrier of IT};
end;

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

theorem :: TDLAT_3:13
for Y being TopStruct st
{} in the topology of Y & the carrier of Y in the topology of Y holds
bool the carrier of Y = {{}, the carrier of Y} implies
Y is discrete & Y is anti-discrete;

definition
cluster discrete anti-discrete strict non empty TopStruct;
end;

theorem :: TDLAT_3:14
for Y being discrete TopStruct, A being Subset of Y holds
(the carrier of Y) \ A in the topology of Y;

theorem :: TDLAT_3:15
for Y being anti-discrete TopStruct, A being Subset of Y st
A in the topology of Y holds (the carrier of Y) \ A in the topology of Y;

definition
cluster discrete -> TopSpace-like TopStruct;
cluster anti-discrete -> TopSpace-like TopStruct;
end;

theorem :: TDLAT_3:16
for Y being TopSpace-like TopStruct holds
bool the carrier of Y = {{}, the carrier of Y} implies
Y is discrete & Y is anti-discrete;

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;

definition
cluster discrete -> almost_discrete TopStruct;
cluster anti-discrete -> almost_discrete TopStruct;
end;

definition
cluster almost_discrete strict TopStruct;
end;

begin
:: 3. Discrete Topological Spaces.

definition
cluster discrete anti-discrete strict non empty TopSpace;
end;

theorem :: TDLAT_3:17
X is discrete iff
for A being Subset of X holds A is open;

theorem :: TDLAT_3:18
X is discrete iff
for A being Subset of X holds A is closed;

theorem :: TDLAT_3:19
(for A being Subset of X, x being Point of X st A = {x} holds
A is open) implies X is discrete;

definition let X be discrete non empty TopSpace;
cluster -> open closed discrete SubSpace of X;
end;

definition let X be discrete non empty TopSpace;
cluster discrete strict SubSpace of X;
end;

theorem :: TDLAT_3:20
X is anti-discrete iff
for A being Subset of X st A is open
holds A = {} or A = the carrier of X;

theorem :: TDLAT_3:21
X is anti-discrete iff
for A being Subset of X st A is closed
holds A = {} or A = the carrier of X;

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

definition let X be anti-discrete non empty TopSpace;
cluster -> anti-discrete SubSpace of X;
end;

definition let X be anti-discrete non empty TopSpace;
cluster anti-discrete SubSpace of X;
end;

theorem :: TDLAT_3:23
X is almost_discrete iff
for A being Subset of X st A is open holds A is closed;

theorem :: TDLAT_3:24
X is almost_discrete iff
for A being Subset of X st A is closed holds A is open;

theorem :: TDLAT_3:25
X is almost_discrete iff
for A being Subset of X st A is open holds Cl A = A;

theorem :: TDLAT_3:26
X is almost_discrete iff
for A being Subset of X st A is closed holds Int A = A;

definition
cluster almost_discrete strict TopSpace;
end;

theorem :: TDLAT_3:27
(for A being Subset of X, x being Point of X st A = {x}
holds Cl A is open)
implies X is almost_discrete;

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

definition
cluster discrete -> almost_discrete TopSpace;
cluster anti-discrete -> almost_discrete TopSpace;
end;

definition let X be almost_discrete non empty TopSpace;
cluster -> almost_discrete (non empty SubSpace of X);
end;

definition let X be almost_discrete non empty TopSpace;
cluster open -> closed SubSpace of X;
cluster closed -> open SubSpace of X;
end;

definition let X be almost_discrete non empty TopSpace;
cluster almost_discrete strict non empty SubSpace of X;
end;

begin
:: 4. Extremally Disconnected Topological Spaces.

definition let IT be non empty TopSpace;
attr IT is extremally_disconnected means
:: TDLAT_3:def 4
for A being Subset of IT st A is open holds Cl A is open;
end;

definition
cluster extremally_disconnected strict (non empty TopSpace);
end;

reserve X for non empty TopSpace;

theorem :: TDLAT_3:29
X is extremally_disconnected iff
for A being Subset of X st A is closed holds Int A is closed;

theorem :: TDLAT_3:30
X is extremally_disconnected iff
for A, B being Subset of X st A is open & B is open holds
A misses B implies Cl A misses Cl B;

theorem :: TDLAT_3:31
X is extremally_disconnected iff
for A, B being Subset of X st A is closed & B is closed holds
A \/ B = the carrier of X implies (Int A) \/ (Int B) = the carrier of X;

theorem :: TDLAT_3:32
X is extremally_disconnected iff
for A being Subset of X st A is open holds Cl A = Int Cl A;

theorem :: TDLAT_3:33
X is extremally_disconnected iff
for A being Subset of X st A is closed holds Int A = Cl Int A;

theorem :: TDLAT_3:34
X is extremally_disconnected iff
for A being Subset of X st A is condensed
holds A is closed & A is open;

theorem :: TDLAT_3:35
X is extremally_disconnected iff
for A being Subset of X st A is condensed holds
A is closed_condensed & A is open_condensed;

theorem :: TDLAT_3:36
X is extremally_disconnected iff
for A being Subset of X st A is condensed
holds Int Cl A = Cl Int A;

theorem :: TDLAT_3:37
X is extremally_disconnected iff
for A being Subset of X st A is condensed holds Int A = Cl A;

theorem :: TDLAT_3:38
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);

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

definition
cluster hereditarily_extremally_disconnected strict (non empty TopSpace);
end;

definition
cluster
hereditarily_extremally_disconnected -> extremally_disconnected
(non empty TopSpace);
cluster
almost_discrete -> hereditarily_extremally_disconnected (non empty TopSpace);
end;

theorem :: TDLAT_3:39
for X being extremally_disconnected (non empty TopSpace),
X0 being non empty SubSpace of X,
A being Subset of X st A = the carrier of X0 & A is dense
holds X0 is extremally_disconnected;

definition let X be extremally_disconnected (non empty TopSpace);
cluster open -> extremally_disconnected (non empty SubSpace of X);
end;

definition let X be extremally_disconnected (non empty TopSpace);
cluster extremally_disconnected strict (non empty SubSpace of X);
end;

definition let X be hereditarily_extremally_disconnected (non empty TopSpace);
cluster -> hereditarily_extremally_disconnected (non empty SubSpace of X);
end;

definition let X be hereditarily_extremally_disconnected (non empty TopSpace);
cluster hereditarily_extremally_disconnected strict (non empty SubSpace of X);
end;

theorem :: TDLAT_3:40
(for X0 being closed non empty SubSpace of X
holds X0 is extremally_disconnected)
implies X is hereditarily_extremally_disconnected;

begin
:: 5. The Lattice of Domains of Extremally Disconnected Spaces.

::Properties of the Lattice of Domains of an Extremally Disconnected Space.
reserve Y for extremally_disconnected (non empty TopSpace);

theorem :: TDLAT_3:41
Domains_of Y = Closed_Domains_of Y;

theorem :: TDLAT_3:42
D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y;

theorem :: TDLAT_3:43
Domains_Lattice Y = Closed_Domains_Lattice Y;

theorem :: TDLAT_3:44
Domains_of Y = Open_Domains_of Y;

theorem :: TDLAT_3:45
D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y;

theorem :: TDLAT_3:46
Domains_Lattice Y = Open_Domains_Lattice Y;

theorem :: TDLAT_3:47
for A, B being Element of Domains_of Y holds
(D-Union Y).(A,B) = A \/ B & (D-Meet Y).(A,B) = A /\ B;

theorem :: TDLAT_3:48
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;

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

theorem :: TDLAT_3:50
for F being Subset-Family of Y st F is domains-family
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);

::Lattice-theoretic Characterizations of Extremally Disconnected Spaces.
reserve X for non empty TopSpace;

theorem :: TDLAT_3:51
X is extremally_disconnected iff Domains_Lattice X is M_Lattice;

theorem :: TDLAT_3:52
Domains_Lattice X = Closed_Domains_Lattice X implies
X is extremally_disconnected;

theorem :: TDLAT_3:53
Domains_Lattice X = Open_Domains_Lattice X implies
X is extremally_disconnected;

theorem :: TDLAT_3:54
Closed_Domains_Lattice X = Open_Domains_Lattice X implies
X is extremally_disconnected;

theorem :: TDLAT_3:55
X is extremally_disconnected iff Domains_Lattice X is B_Lattice;
```