:: Representation Theorem for Boolean Algebras
::  by Jaros{\l}aw Stanis{\l}aw Walijewski
::
:: Received July 14, 1993
:: Copyright (c) 1993-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 XBOOLE_0, PRE_TOPC, SUBSET_1, SETFAM_1, RCOMP_1, TARSKI,
      ZFMISC_1, STRUCT_0, BINOP_1, FUNCT_1, LATTICES, EQREL_1, XXREAL_2,
      CARD_FIL, RELAT_1, INT_2, FINSUB_1, SETWISEO, FILTER_0, LATTICE2, PBOOLE,
      FINSET_1, CLASSES1, CARD_1, GROUP_6, FUNCT_2, WELLORD1, LOPCLSET,
      LATTICE4;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, PRE_TOPC, LATTICES,
      LATTICE2, FILTER_0, FINSET_1, SETWISEO, LATTICE4, CLASSES1, CARD_1;
 constructors BINOP_1, SETWISEO, PRE_TOPC, LATTICE2, FILTER_1, CLASSES1,
      LATTICE4, RELSET_1, FILTER_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
      FINSUB_1, STRUCT_0, LATTICES, PRE_TOPC, CARD_1, RELSET_1, TOPS_1,
      LATTICE2;
 requirements BOOLE, SUBSET;


begin

reserve T for non empty TopSpace,
  X,Z for Subset of T;

definition
  let T be non empty TopStruct;
  func OpenClosedSet(T) -> Subset-Family of T equals
:: LOPCLSET:def 1
  {x where x is Subset of T: x is open closed};
end;

registration
  let T be non empty TopSpace;
  cluster OpenClosedSet(T) -> non empty;
end;

theorem :: LOPCLSET:1
  X in OpenClosedSet(T) implies X is open;

theorem :: LOPCLSET:2
  X in OpenClosedSet(T) implies X is closed;

theorem :: LOPCLSET:3
  X is open closed implies X in OpenClosedSet(T);

reserve x,y for Element of OpenClosedSet(T);

definition
  let T;
  let C,D be Element of OpenClosedSet(T);
  redefine func C \/ D -> Element of OpenClosedSet(T);
  redefine func C /\ D -> Element of OpenClosedSet(T);
end;

definition
  let T;
  func T_join T -> BinOp of OpenClosedSet(T) means
:: LOPCLSET:def 2

  for A,B being Element of OpenClosedSet(T) holds it.(A,B) = A \/ B;
  func T_meet T -> BinOp of OpenClosedSet(T) means
:: LOPCLSET:def 3

  for A,B being Element of OpenClosedSet(T) holds it.(A,B) = A /\ B;
end;

theorem :: LOPCLSET:4
  for x,y be Element of LattStr(#OpenClosedSet(T),T_join T,T_meet T#),
  x9,y9 be Element of OpenClosedSet(T)
  st x=x9 & y=y9 holds x"\/"y = x9 \/ y9;

theorem :: LOPCLSET:5
  for x,y be Element of LattStr(#OpenClosedSet(T),T_join T,T_meet T#),
  x9,y9 be Element of OpenClosedSet(T)
  st x=x9 & y=y9 holds x"/\"y = x9 /\ y9;

theorem :: LOPCLSET:6
  {} T is Element of OpenClosedSet(T);

theorem :: LOPCLSET:7
  [#] T is Element of OpenClosedSet(T);

theorem :: LOPCLSET:8
  x` is Element of OpenClosedSet(T);

theorem :: LOPCLSET:9
  LattStr(#OpenClosedSet(T),T_join T,T_meet T#) is Lattice;

definition
  let T be non empty TopSpace;
  func OpenClosedSetLatt(T) -> Lattice equals
:: LOPCLSET:def 4
  LattStr(#OpenClosedSet(T),T_join T,T_meet T#);
end;

theorem :: LOPCLSET:10
  for T being non empty TopSpace, x,y being Element of
  OpenClosedSetLatt(T) holds x"\/"y = x \/ y;

theorem :: LOPCLSET:11
  for T being non empty TopSpace , x,y being Element of
  OpenClosedSetLatt(T) holds x"/\"y = x /\ y;

theorem :: LOPCLSET:12
  the carrier of OpenClosedSetLatt(T) = OpenClosedSet(T);

registration
  let T;
  cluster OpenClosedSetLatt(T) -> Boolean;
end;

theorem :: LOPCLSET:13
  [#] T is Element of OpenClosedSetLatt(T);

theorem :: LOPCLSET:14
  {} T is Element of OpenClosedSetLatt(T);

reserve x,y,X for set;

registration
  cluster non trivial for B_Lattice;
end;

reserve BL for non trivial B_Lattice,
  a,b,c,p,q for Element of BL,
  UF,F,F0,F1,F2 for Filter of BL;

definition
  let BL;
  func ultraset BL -> Subset-Family of BL equals
:: LOPCLSET:def 5
  {F : F is being_ultrafilter};
end;

registration
  let BL;
  cluster ultraset BL -> non empty;
end;

theorem :: LOPCLSET:15
  x in ultraset BL iff ex UF st UF = x & UF is being_ultrafilter;

theorem :: LOPCLSET:16
  for a holds { F :F is being_ultrafilter & a in F} c= ultraset BL;

definition
  let BL;
  func UFilter BL -> Function means
:: LOPCLSET:def 6

  dom it = the carrier of BL & for a being Element of BL
  holds it.a = {UF:  UF is being_ultrafilter & a in UF };
end;

theorem :: LOPCLSET:17
  x in UFilter BL.a iff ex F st F=x & F is being_ultrafilter & a in F;

theorem :: LOPCLSET:18
  F in UFilter BL.a iff F is being_ultrafilter & a in F;

theorem :: LOPCLSET:19
  for F st F is being_ultrafilter holds a "\/" b in F iff a in F or b in F;

theorem :: LOPCLSET:20
  UFilter BL.(a "/\" b) = UFilter BL.a /\ UFilter BL.b;

theorem :: LOPCLSET:21
  UFilter BL.(a "\/" b) = UFilter BL.a \/ UFilter BL.b;

definition
  let BL;
  redefine func UFilter BL -> Function of the carrier of BL, bool ultraset BL;
end;

definition
  let BL;
  func StoneR BL -> set equals
:: LOPCLSET:def 7
  rng UFilter BL;
end;

registration
  let BL;
  cluster StoneR BL -> non empty;
end;

theorem :: LOPCLSET:22
  StoneR BL c= bool ultraset BL;

theorem :: LOPCLSET:23
  x in StoneR BL iff ex a st (UFilter BL).a =x;

definition
  let BL;
  func StoneSpace BL -> strict TopSpace means
:: LOPCLSET:def 8

  the carrier of it =ultraset BL & the topology of it =
  {union A where A is Subset-Family of ultraset BL : A c= StoneR BL };
end;

registration
  let BL;
  cluster StoneSpace BL -> non empty;
end;

theorem :: LOPCLSET:24
  F is being_ultrafilter & not F in UFilter BL.a implies not a in F;

theorem :: LOPCLSET:25
  ultraset BL \ UFilter BL.a = UFilter BL.a`;

definition
  let BL;
  func StoneBLattice BL -> Lattice equals
:: LOPCLSET:def 9
  OpenClosedSetLatt(StoneSpace BL );
end;

registration
  let BL;
  cluster UFilter BL -> one-to-one;
end;

theorem :: LOPCLSET:26
  union StoneR BL = ultraset BL;

theorem :: LOPCLSET:27
  for X being non empty set ex Y being Element of Fin X st Y is non empty;

registration
  let D be non empty set;
  cluster non empty for Element of Fin D;
end;

theorem :: LOPCLSET:28
  for L being non trivial B_Lattice, D being non empty Subset of L
  st Bottom L in <.D.) ex B being non empty Element of Fin the carrier of L
  st B c= D & FinMeet(B) = Bottom L;

theorem :: LOPCLSET:29
  for L being 0_Lattice holds
  not ex F being Filter of L st F is being_ultrafilter & Bottom L in F;

theorem :: LOPCLSET:30
  UFilter BL.Bottom BL = {};

theorem :: LOPCLSET:31
  UFilter BL.Top BL = ultraset BL;

theorem :: LOPCLSET:32
  ultraset BL = union X & X is Subset of StoneR BL implies
  ex Y being Element of Fin X st ultraset BL = union Y;

theorem :: LOPCLSET:33
  StoneR BL = OpenClosedSet(StoneSpace BL);

definition
  let BL;
  redefine func UFilter BL -> Homomorphism of BL,StoneBLattice BL;
end;

theorem :: LOPCLSET:34
  rng UFilter BL = the carrier of StoneBLattice BL;

registration
  let BL;
  cluster UFilter BL -> bijective for Function of BL,StoneBLattice BL;
end;

theorem :: LOPCLSET:35
  BL,StoneBLattice BL are_isomorphic;

::$N Stone Representation Theorem for Boolean Algebras
theorem :: LOPCLSET:36
  for BL being non trivial B_Lattice ex T being non empty TopSpace st
  BL, OpenClosedSetLatt(T) are_isomorphic;