:: The Lattice of Domains of an Extremally Disconnected Space
:: by Zbigniew Karno
::
:: Received August 27, 1992
:: Copyright (c) 1992-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PRE_TOPC, SUBSET_1, TOPS_1, XBOOLE_0, STRUCT_0, RCOMP_1, TARSKI,
NATTRA_1, ZFMISC_1, SETFAM_1, TDLAT_1, REALSET1, LATTICES, FUNCT_1,
EQREL_1, TDLAT_2, PBOOLE, TDLAT_3;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, STRUCT_0, REALSET1, PRE_TOPC,
TOPS_1, TOPS_2, BORSUK_1, TSEP_1, BINOP_1, LATTICES, LATTICE3, TDLAT_1,
TDLAT_2;
constructors SETFAM_1, REALSET1, TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_1,
TDLAT_2, TSEP_1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, PRE_TOPC,
TOPS_1, BORSUK_1, TSEP_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;
theorem :: TDLAT_3:1
Cl C = (Int C`)`;
theorem :: TDLAT_3:2
Cl C` = (Int C)`;
theorem :: TDLAT_3:3
Int C` = (Cl C)`;
reserve A, B for Subset of X;
theorem :: TDLAT_3:4
A \/ B = the carrier of X implies (A is closed implies A \/ Int B =
the carrier of X);
theorem :: TDLAT_3:5
A is open closed iff Cl A = Int A;
theorem :: TDLAT_3:6
A is open & A is closed implies Int Cl A = Cl Int A;
::Properties of Domains.
theorem :: TDLAT_3:7
A is condensed & Cl Int A c= Int Cl A implies A is open_condensed
& A is closed_condensed;
theorem :: TDLAT_3:8
A is condensed & Cl Int A c= Int Cl A implies A is open & A is closed;
theorem :: TDLAT_3:9
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:10
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:11
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;
registration
cluster discrete anti-discrete strict non empty for TopStruct;
end;
theorem :: TDLAT_3:12
for Y being discrete TopStruct, A being Subset of Y holds (the
carrier of Y) \ A in the topology of Y;
theorem :: TDLAT_3:13
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;
registration
cluster discrete -> TopSpace-like for TopStruct;
cluster anti-discrete -> TopSpace-like for TopStruct;
end;
theorem :: TDLAT_3:14
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;
registration
cluster discrete -> almost_discrete for TopStruct;
cluster anti-discrete -> almost_discrete for TopStruct;
end;
registration
cluster almost_discrete strict for TopStruct;
end;
begin
:: 3. Discrete Topological Spaces.
registration
cluster discrete anti-discrete strict non empty for TopSpace;
end;
theorem :: TDLAT_3:15
X is discrete iff for A being Subset of X holds A is open;
theorem :: TDLAT_3:16
X is discrete iff for A being Subset of X holds A is closed;
theorem :: TDLAT_3:17
(for A being Subset of X, x being Point of X st A = {x} holds A
is open) implies X is discrete;
registration
let X be discrete non empty TopSpace;
cluster -> open closed discrete for SubSpace of X;
end;
registration
let X be discrete non empty TopSpace;
cluster discrete strict for SubSpace of X;
end;
theorem :: TDLAT_3:18
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:19
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:20
(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;
registration
let X be anti-discrete non empty TopSpace;
cluster -> anti-discrete for SubSpace of X;
end;
registration
let X be anti-discrete non empty TopSpace;
cluster anti-discrete for SubSpace of X;
end;
theorem :: TDLAT_3:21
X is almost_discrete iff for A being Subset of X st A is open
holds A is closed;
theorem :: TDLAT_3:22
X is almost_discrete iff for A being Subset of X st A is closed
holds A is open;
theorem :: TDLAT_3:23
X is almost_discrete iff for A being Subset of X st A is open holds Cl A = A;
theorem :: TDLAT_3:24
X is almost_discrete iff for A being Subset of X st A is closed holds
Int A = A;
registration
cluster almost_discrete strict for TopSpace;
end;
theorem :: TDLAT_3:25
(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:26
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;
registration
cluster discrete -> almost_discrete for TopSpace;
cluster anti-discrete -> almost_discrete for TopSpace;
end;
registration
let X be almost_discrete non empty TopSpace;
cluster -> almost_discrete for non empty SubSpace of X;
end;
registration
let X be almost_discrete non empty TopSpace;
cluster open -> closed for SubSpace of X;
cluster closed -> open for SubSpace of X;
end;
registration
let X be almost_discrete non empty TopSpace;
cluster almost_discrete strict non empty for 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;
registration
cluster extremally_disconnected strict for non empty TopSpace;
end;
reserve X for non empty TopSpace;
theorem :: TDLAT_3:27
X is extremally_disconnected iff for A being Subset of X st A is
closed holds Int A is closed;
theorem :: TDLAT_3:28
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:29
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:30
X is extremally_disconnected iff for A being Subset of X st A is
open holds Cl A = Int Cl A;
theorem :: TDLAT_3:31
X is extremally_disconnected iff for A being Subset of X st A is
closed holds Int A = Cl Int A;
theorem :: TDLAT_3:32
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:33
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:34
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:35
X is extremally_disconnected iff for A being Subset of X st A is
condensed holds Int A = Cl A;
theorem :: TDLAT_3:36
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;
registration
cluster hereditarily_extremally_disconnected strict for non empty TopSpace;
end;
registration
cluster hereditarily_extremally_disconnected -> extremally_disconnected for
non
empty TopSpace;
cluster almost_discrete -> hereditarily_extremally_disconnected for
non empty
TopSpace;
end;
theorem :: TDLAT_3:37
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;
registration
let X be extremally_disconnected non empty TopSpace;
cluster open -> extremally_disconnected for non empty SubSpace of X;
end;
registration
let X be extremally_disconnected non empty TopSpace;
cluster extremally_disconnected strict for non empty SubSpace of X;
end;
registration
let X be hereditarily_extremally_disconnected non empty TopSpace;
cluster -> hereditarily_extremally_disconnected for
non empty SubSpace of X;
end;
registration
let X be hereditarily_extremally_disconnected non empty TopSpace;
cluster hereditarily_extremally_disconnected strict for
non empty SubSpace of X;
end;
theorem :: TDLAT_3:38
(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:39
Domains_of Y = Closed_Domains_of Y;
theorem :: TDLAT_3:40
D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y;
theorem :: TDLAT_3:41
Domains_Lattice Y = Closed_Domains_Lattice Y;
theorem :: TDLAT_3:42
Domains_of Y = Open_Domains_of Y;
theorem :: TDLAT_3:43
D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y;
theorem :: TDLAT_3:44
Domains_Lattice Y = Open_Domains_Lattice Y;
theorem :: TDLAT_3:45
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:46
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:47
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:48
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:49
X is extremally_disconnected iff Domains_Lattice X is M_Lattice;
theorem :: TDLAT_3:50
Domains_Lattice X = Closed_Domains_Lattice X implies
X is extremally_disconnected;
theorem :: TDLAT_3:51
Domains_Lattice X = Open_Domains_Lattice X implies
X is extremally_disconnected;
theorem :: TDLAT_3:52
Closed_Domains_Lattice X = Open_Domains_Lattice X implies
X is extremally_disconnected;
theorem :: TDLAT_3:53
X is extremally_disconnected iff Domains_Lattice X is B_Lattice;