Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Representation Theorem for Boolean Algebras

by
Jaroslaw Stanislaw Walijewski

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;
```