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;