The abstract of the Mizar article:

The Lattice of Domains of an Extremally Disconnected Space

by

Zbigniew Karno

Received August 27, 1992

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;