:: Representation Theorem for Boolean Algebras
:: by Jaros{\l}aw Stanis{\l}aw Walijewski
::
:: Received July 14, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

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 & x is closed )  }  ;
coherence
  {  x where x is Subset of T : ( x is open & x is closed )  }  is Subset-Family of T
proofend;
end;

:: deftheorem  defines OpenClosedSet LOPCLSET:def_1_:_
 for T being non empty TopStruct holds OpenClosedSet T =  {  x where x is Subset of T : ( x is open & x is closed )  }  ;

registration
let T be non empty TopSpace;
cluster OpenClosedSet T ->  non empty ;
coherence
 not OpenClosedSet T is empty
proofend;
end;

theorem Th1: :: LOPCLSET:1
for T being non empty TopSpace
for X being Subset of T st X in OpenClosedSet T holds
X is open
proofend;

theorem Th2: :: LOPCLSET:2
for T being non empty TopSpace
for X being Subset of T st X in OpenClosedSet T holds
X is closed
proofend;

theorem Th3: :: LOPCLSET:3
for T being non empty TopSpace
for X being Subset of T st X is open & X is closed holds
X in OpenClosedSet T ;

definition
let T be non empty TopSpace;
let C, D be Element of OpenClosedSet T;
:: original:\/
redefine funcC \/ D ->  Element of OpenClosedSet T;
coherence
 C \/ D is Element of OpenClosedSet T
proofend;
:: original:/\
redefine funcC /\ D ->  Element of OpenClosedSet T;
coherence
 C /\ D is Element of OpenClosedSet T
proofend;
end;

definition
let T be non empty TopSpace;
deffunc H1( Element of OpenClosedSet T, Element of OpenClosedSet T) ->  Element of OpenClosedSet T = $1 \/ $2;
func T_join T ->  BinOp of (OpenClosedSet T) means :Def2: :: LOPCLSET:def 2
 for A, B being Element of OpenClosedSet T holds it . (A,B) = A \/ B;
existence
 ex b1 being BinOp of (OpenClosedSet T) st
for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A \/ B
proofend;
uniqueness
 for b1, b2 being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A \/ B ) & ( for A, B being Element of OpenClosedSet T holds b2 . (A,B) = A \/ B ) holds
b1 = b2
proofend;
deffunc H2( Element of OpenClosedSet T, Element of OpenClosedSet T) ->  Element of OpenClosedSet T = $1 /\ $2;
func T_meet T ->  BinOp of (OpenClosedSet T) means :Def3: :: LOPCLSET:def 3
 for A, B being Element of OpenClosedSet T holds it . (A,B) = A /\ B;
existence
 ex b1 being BinOp of (OpenClosedSet T) st
for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A /\ B
proofend;
uniqueness
 for b1, b2 being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A /\ B ) & ( for A, B being Element of OpenClosedSet T holds b2 . (A,B) = A /\ B ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines T_join LOPCLSET:def_2_:_
 for T being non empty TopSpace
for b2 being BinOp of (OpenClosedSet T) holds
( b2 = T_join T iff for A, B being Element of OpenClosedSet T holds b2 . (A,B) = A \/ B );

:: deftheorem Def3 defines T_meet LOPCLSET:def_3_:_
 for T being non empty TopSpace
for b2 being BinOp of (OpenClosedSet T) holds
( b2 = T_meet T iff for A, B being Element of OpenClosedSet T holds b2 . (A,B) = A /\ B );

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

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

theorem :: LOPCLSET:6
for T being non empty TopSpace holds {} T is Element of OpenClosedSet T by Th3;

theorem :: LOPCLSET:7
for T being non empty TopSpace holds [#] T is Element of OpenClosedSet T by Th3;

theorem Th8: :: LOPCLSET:8
for T being non empty TopSpace
for x being Element of OpenClosedSet T holds x ` is Element of OpenClosedSet T
proofend;

theorem Th9: :: LOPCLSET:9
for T being non empty TopSpace holds LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice
proofend;

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

:: deftheorem  defines OpenClosedSetLatt LOPCLSET:def_4_:_
 for T being non empty TopSpace holds OpenClosedSetLatt T = LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #);

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

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

theorem :: LOPCLSET:12
for T being non empty TopSpace holds the carrier of (OpenClosedSetLatt T) = OpenClosedSet T ;

registration
let T be non empty TopSpace;
cluster OpenClosedSetLatt T ->  Boolean ;
coherence
 OpenClosedSetLatt T is Boolean
proofend;
end;

theorem :: LOPCLSET:13
for T being non empty TopSpace holds [#] T is Element of (OpenClosedSetLatt T) by Th3;

theorem :: LOPCLSET:14
for T being non empty TopSpace holds {} T is Element of (OpenClosedSetLatt T) by Th3;

registration
cluster non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean for LattStr ;
existence
 not for b1 being B_Lattice holds b1 is trivial
proofend;
end;

definition
let BL be non trivial B_Lattice;
func ultraset BL ->  Subset-Family of BL equals :: LOPCLSET:def 5
 {  F where F is Filter of BL : F is being_ultrafilter  }  ;
coherence
  {  F where F is Filter of BL : F is being_ultrafilter  }  is Subset-Family of BL
proofend;
end;

:: deftheorem  defines ultraset LOPCLSET:def_5_:_
 for BL being non trivial B_Lattice holds ultraset BL =  {  F where F is Filter of BL : F is being_ultrafilter  }  ;

registration
let BL be non trivial B_Lattice;
cluster ultraset BL ->  non empty ;
coherence
 not ultraset BL is empty
proofend;
end;

theorem :: LOPCLSET:15
for x being set
for BL being non trivial B_Lattice holds
( x in ultraset BL iff ex UF being Filter of BL st
( UF = x & UF is being_ultrafilter ) ) ;

theorem Th16: :: LOPCLSET:16
for BL being non trivial B_Lattice
for a being Element of BL holds  {  F where F is Filter of BL : ( F is being_ultrafilter & a in F )  }  c= ultraset BL
proofend;

definition
let BL be non trivial B_Lattice;
func UFilter BL ->  Function means :Def6: :: LOPCLSET:def 6
( dom it = the carrier of BL & ( for a being Element of BL holds it . a =  {  UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF )  }  ) );
existence
 ex b1 being Function st
( dom b1 = the carrier of BL & ( for a being Element of BL holds b1 . a =  {  UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF )  }  ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = the carrier of BL & ( for a being Element of BL holds b1 . a =  {  UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF )  }  ) & dom b2 = the carrier of BL & ( for a being Element of BL holds b2 . a =  {  UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF )  }  ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines UFilter LOPCLSET:def_6_:_
 for BL being non trivial B_Lattice
for b2 being Function holds
( b2 = UFilter BL iff ( dom b2 = the carrier of BL & ( for a being Element of BL holds b2 . a =  {  UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF )  }  ) ) );

theorem Th17: :: LOPCLSET:17
for x being set
for BL being non trivial B_Lattice
for a being Element of BL holds
( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) )
proofend;

theorem Th18: :: LOPCLSET:18
for BL being non trivial B_Lattice
for a being Element of BL
for F being Filter of BL holds
( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )
proofend;

theorem Th19: :: LOPCLSET:19
for BL being non trivial B_Lattice
for a, b being Element of BL
for F being Filter of BL st F is being_ultrafilter holds
( a "\/" b in F iff ( a in F or b in F ) )
proofend;

theorem Th20: :: LOPCLSET:20
for BL being non trivial B_Lattice
for a, b being Element of BL holds (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b)
proofend;

theorem Th21: :: LOPCLSET:21
for BL being non trivial B_Lattice
for a, b being Element of BL holds (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)
proofend;

definition
let BL be non trivial B_Lattice;
:: original:UFilter
redefine func UFilter BL ->  Function of the carrier of BL,(bool (ultraset BL));
coherence
 UFilter BL is Function of the carrier of BL,(bool (ultraset BL))
proofend;
end;

definition
let BL be non trivial B_Lattice;
func StoneR BL ->  set  equals :: LOPCLSET:def 7
 rng (UFilter BL);
coherence
 rng (UFilter BL) is set ;
end;

:: deftheorem  defines StoneR LOPCLSET:def_7_:_
 for BL being non trivial B_Lattice holds StoneR BL = rng (UFilter BL);

registration
let BL be non trivial B_Lattice;
cluster StoneR BL ->  non empty ;
coherence
 not StoneR BL is empty ;
end;

theorem :: LOPCLSET:22
for BL being non trivial B_Lattice holds StoneR BL c= bool (ultraset BL) ;

theorem Th23: :: LOPCLSET:23
for x being set
for BL being non trivial B_Lattice holds
( x in StoneR BL iff ex a being Element of BL st (UFilter BL) . a = x )
proofend;

definition
let BL be non trivial B_Lattice;
func StoneSpace BL ->  strict TopSpace means :Def8: :: 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  }  );
existence
 ex b1 being strict TopSpace st
( the carrier of b1 = ultraset BL & the topology of b1 =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  )
proofend;
uniqueness
 for b1, b2 being strict TopSpace st the carrier of b1 = ultraset BL & the topology of b1 =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  & the carrier of b2 = ultraset BL & the topology of b2 =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  holds
b1 = b2 ;
end;

:: deftheorem Def8 defines StoneSpace LOPCLSET:def_8_:_
 for BL being non trivial B_Lattice
for b2 being strict TopSpace holds
( b2 = StoneSpace BL iff ( the carrier of b2 = ultraset BL & the topology of b2 =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  ) );

registration
let BL be non trivial B_Lattice;
cluster StoneSpace BL ->  non empty strict ;
coherence
 not StoneSpace BL is empty
proofend;
end;

theorem :: LOPCLSET:24
for BL being non trivial B_Lattice
for a being Element of BL
for F being Filter of BL st F is being_ultrafilter & not F in (UFilter BL) . a holds
not a in F by Th18;

theorem Th25: :: LOPCLSET:25
for BL being non trivial B_Lattice
for a being Element of BL holds (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a `)
proofend;

definition
let BL be non trivial B_Lattice;
func StoneBLattice BL ->  Lattice equals :: LOPCLSET:def 9
 OpenClosedSetLatt (StoneSpace BL);
coherence
 OpenClosedSetLatt (StoneSpace BL) is Lattice ;
end;

:: deftheorem  defines StoneBLattice LOPCLSET:def_9_:_
 for BL being non trivial B_Lattice holds StoneBLattice BL = OpenClosedSetLatt (StoneSpace BL);

Lm1:  for BL being non trivial B_Lattice
for p being Subset of (StoneSpace BL) st p in StoneR BL holds
p is open
proofend;

registration
let BL be non trivial B_Lattice;
cluster UFilter BL ->  one-to-one ;
coherence
 UFilter BL is one-to-one
proofend;
end;

theorem :: LOPCLSET:26
for BL being non trivial B_Lattice holds union (StoneR BL) = ultraset BL
proofend;

theorem Th27: :: LOPCLSET:27
for X being non empty set holds
not for Y being Finite_Subset of X holds Y is empty
proofend;

registration
let D be non empty set ;
cluster non empty finite for Element of Fin D;
existence
 not for b1 being Finite_Subset of D holds b1 is empty by Th27;
end;

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

theorem Th29: :: LOPCLSET:29
for L being 0_Lattice
for F being Filter of L holds
( not F is being_ultrafilter or not Bottom L in F )
proofend;

theorem Th30: :: LOPCLSET:30
for BL being non trivial B_Lattice holds (UFilter BL) . (Bottom BL) = {}
proofend;

theorem :: LOPCLSET:31
for BL being non trivial B_Lattice holds (UFilter BL) . (Top BL) = ultraset BL
proofend;

theorem Th32: :: LOPCLSET:32
for X being set
for BL being non trivial B_Lattice st ultraset BL = union X &amp; X is Subset of (StoneR BL) holds
ex Y being Finite_Subset of X st ultraset BL = union Y
proofend;

Lm2:  for BL being non trivial B_Lattice holds StoneR BL c= OpenClosedSet (StoneSpace BL)
proofend;

theorem Th33: :: LOPCLSET:33
for BL being non trivial B_Lattice holds StoneR BL = OpenClosedSet (StoneSpace BL)
proofend;

definition
let BL be non trivial B_Lattice;
:: original:UFilter
redefine func UFilter BL ->  Homomorphism of BL, StoneBLattice BL;
coherence
 UFilter BL is Homomorphism of BL, StoneBLattice BL
proofend;
end;

theorem Th34: :: LOPCLSET:34
for BL being non trivial B_Lattice holds rng (UFilter BL) = the carrier of (StoneBLattice BL)
proofend;

registration
let BL be non trivial B_Lattice;
cluster UFilter BL ->  bijective for Function of BL,(StoneBLattice BL);
coherence
 for b1 being Function of BL,(StoneBLattice BL) st b1 = UFilter BL holds
b1 is bijective
proofend;
end;

theorem Th35: :: LOPCLSET:35
for BL being non trivial B_Lattice holds BL, StoneBLattice BL are_isomorphic
proofend;

:: [WP: ] 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
proofend;