:: The Lattice of Domains of an Extremally Disconnected Space
::  by Zbigniew Karno
::
:: Received August 27, 1992
:: Copyright (c) 1992-2021 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;