:: 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

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 func C \/ D -> Element of OpenClosedSet T;
coherence
C \/ D is Element of OpenClosedSet T

proof end;

:: original: /\
redefine func C /\ D -> Element of OpenClosedSet T;
coherence
C /\ D is Element of OpenClosedSet T

proof end;

end;

definition

let T be non empty TopSpace;
deffunc H₁( 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 b₁ being BinOp of (OpenClosedSet T) st
for A, B being Element of OpenClosedSet T holds b₁ . (A,B) = A \/ B

proof end;

uniqueness
for b₁, b₂ being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b₁ . (A,B) = A \/ B ) & ( for A, B being Element of OpenClosedSet T holds b₂ . (A,B) = A \/ B ) holds
b₁ = b₂

proof end;

deffunc H₂( 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 b₁ being BinOp of (OpenClosedSet T) st
for A, B being Element of OpenClosedSet T holds b₁ . (A,B) = A /\ B

proof end;

uniqueness
for b₁, b₂ being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b₁ . (A,B) = A /\ B ) & ( for A, B being Element of OpenClosedSet T holds b₂ . (A,B) = A /\ B ) holds
b₁ = b₂

proof end;

end;

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

:: deftheorem Def3 defines T_meet LOPCLSET:def 3 :
for T being non empty TopSpace
for b₂ being BinOp of (OpenClosedSet T) holds
( b₂ = T_meet T iff for A, B being Element of OpenClosedSet T holds b₂ . (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

proof end;

theorem Th9: :: LOPCLSET:9

for T being non empty TopSpace holds LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice

proof end;

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

proof end;

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 b₁ being B_Lattice holds b₁ is trivial

proof end;

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

proof end;

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

proof end;

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

proof end;

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 b₁ being Function st
( dom b₁ = the carrier of BL & ( for a being Element of BL holds b₁ . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = the carrier of BL & ( for a being Element of BL holds b₁ . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) & dom b₂ = the carrier of BL & ( for a being Element of BL holds b₂ . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines UFilter LOPCLSET:def 6 :
for BL being non trivial B_Lattice
for b₂ being Function holds
( b₂ = UFilter BL iff ( dom b₂ = the carrier of BL & ( for a being Element of BL holds b₂ . 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 ) )

proof end;

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 ) )

proof end;

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 ) )

proof end;

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)

proof end;

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)

proof end;

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))

proof end;

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 )

proof end;

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 b₁ being strict TopSpace st
( the carrier of b₁ = ultraset BL & the topology of b₁ = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } )

proof end;

uniqueness
for b₁, b₂ being strict TopSpace st the carrier of b₁ = ultraset BL & the topology of b₁ = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } & the carrier of b₂ = ultraset BL & the topology of b₂ = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } holds
b₁ = b₂ ;

end;

:: deftheorem Def8 defines StoneSpace LOPCLSET:def 8 :
for BL being non trivial B_Lattice
for b₂ being strict TopSpace holds
( b₂ = StoneSpace BL iff ( the carrier of b₂ = ultraset BL & the topology of b₂ = { (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

proof end;

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

proof end;

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

proof end;

registration

let BL be non trivial B_Lattice;

cluster UFilter BL -> one-to-one ;

coherence
UFilter BL is one-to-one

proof end;

end;

theorem :: LOPCLSET:26

for BL being non trivial B_Lattice holds union (StoneR BL) = ultraset BL

proof end;

theorem Th27: :: LOPCLSET:27

for X being non empty set holds
not for Y being Element of Fin X holds Y is empty

proof end;

registration

let D be non empty set ;

cluster non empty finite for Element of Fin D;

existence
not for b₁ being Element of Fin D holds b₁ 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 Element of Fin the carrier of L st
( B c= D & FinMeet B = Bottom L )

proof end;

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 )

proof end;

theorem Th30: :: LOPCLSET:30

for BL being non trivial B_Lattice holds (UFilter BL) . (Bottom BL) = {}

proof end;

theorem :: LOPCLSET:31

for BL being non trivial B_Lattice holds (UFilter BL) . (Top BL) = ultraset BL

proof end;

theorem Th32: :: LOPCLSET:32

for X being set
for BL being non trivial B_Lattice st ultraset BL = union X & X is Subset of (StoneR BL) holds
ex Y being Element of Fin X st ultraset BL = union Y

proof end;

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

proof end;

theorem Th33: :: LOPCLSET:33

for BL being non trivial B_Lattice holds StoneR BL = OpenClosedSet (StoneSpace BL)

proof end;

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)

proof end;

end;

theorem Th34: :: LOPCLSET:34

for BL being non trivial B_Lattice holds rng (UFilter BL) = the carrier of (StoneBLattice BL)

proof end;

registration

let BL be non trivial B_Lattice;

cluster UFilter BL -> bijective for Function of BL,(StoneBLattice BL);

coherence
for b₁ being Function of BL,(StoneBLattice BL) st b₁ = UFilter BL holds
b₁ is bijective

proof end;

end;

theorem Th35: :: LOPCLSET:35

for BL being non trivial B_Lattice holds BL, StoneBLattice BL are_isomorphic

proof end;

:: 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

proof end;