The abstract of the Mizar article:

Representation Theorem for Boolean Algebras

by

Jaroslaw Stanislaw Walijewski

Received July 14, 1993

MML identifier: LOPCLSET

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, SETFAM_1, BOOLE, BINOP_1, FUNCT_1, LATTICES, SUBSET_1,
      REALSET1, FILTER_0, RELAT_1, TARSKI, FINSUB_1, LATTICE2, SETWISEO,
      FINSET_1, RFINSEQ, CARD_1, GROUP_6, MOD_4, WELLORD1, LOPCLSET;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      PARTFUN1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, PRE_TOPC, LATTICES,
      LATTICE2, FILTER_0, REALSET1, FINSET_1, SETWISEO, LATTICE4, RFINSEQ,
      CARD_1, GRCAT_1;
 constructors BINOP_1, LATTICE2, REALSET1, SETWISEO, LATTICE4, RFINSEQ,
      FILTER_1, GRCAT_1, MEMBERED, PRE_TOPC;
 clusters FINSET_1, FINSUB_1, LATTICES, PRE_TOPC, RLSUB_2, STRUCT_0, RELSET_1,
      SUBSET_1, SETFAM_1, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1;
 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;

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

canceled;

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

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

theorem :: LOPCLSET:4
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:5
for x,y be Element of
    LattStr(#OpenClosedSet(T),T_join T,T_meet T#),
       x',y' be Element of OpenClosedSet(T)
       st x=x' & y=y' holds x"\/"y = x' \/ y';

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

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

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

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

theorem :: LOPCLSET:10
  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:11
 for T being non empty TopSpace, x,y being Element of
    OpenClosedSetLatt(T) holds x"\/"y = x \/ y;

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

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

theorem :: LOPCLSET:14
   OpenClosedSetLatt(T) is Boolean;

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

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

reserve x,y,X,Y for set;

definition
 cluster non trivial 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 of bool the carrier of BL equals
:: LOPCLSET:def 5
 {F : F is_ultrafilter};
end;

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

canceled;

theorem :: LOPCLSET:18
  x in ultraset BL iff (ex UF st UF = x & UF is_ultrafilter);

theorem :: LOPCLSET:19
for a holds { F :F is_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_ultrafilter & a in UF };
end;

theorem :: LOPCLSET:20
  x in UFilter BL.a iff (ex F st F=x & F is_ultrafilter & a in F);

theorem :: LOPCLSET:21
   F in UFilter BL.a iff F is_ultrafilter & a in F;

 theorem :: LOPCLSET:22
 for F st F is_ultrafilter holds a "\/" b in F iff a in F or b in F;

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

theorem :: LOPCLSET:24
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;

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

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

theorem :: LOPCLSET:26
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;

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

theorem :: LOPCLSET:27
  (F is_ultrafilter & not F in UFilter BL.a) implies not a in F;

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

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

theorem :: LOPCLSET:29
UFilter BL is one-to-one;

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

theorem :: LOPCLSET:31
 for A,B,X being set holds (X c= union (A \/ B) &
    for Y being set st Y in B holds Y misses X )
        implies X c= union A;

theorem :: LOPCLSET:32
  for X being non empty set ex Y being Finite_Subset of X st Y is non empty;

definition let D be non empty set;
 cluster non empty Finite_Subset of D;
end;

canceled;

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

theorem :: LOPCLSET:35
 for L being 0_Lattice holds
  not ex F being Filter of L st F is_ultrafilter & Bottom L in F;

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

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

theorem :: LOPCLSET:38
   ultraset BL = union X & X is Subset of StoneR BL implies
  ex Y being Finite_Subset of X st ultraset BL = union Y;

canceled;

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

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

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

theorem :: LOPCLSET:42
UFilter BL is isomorphism;

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

theorem :: LOPCLSET:44
  for BL being non trivial B_Lattice ex T being non empty TopSpace st
  BL, OpenClosedSetLatt(T) are_isomorphic;