:: Representation Theorem for Boolean Algebras
:: by Jaros{\l}aw Stanis{\l}aw Walijewski
::
:: Received July 14, 1993
:: Copyright (c) 1993 Association of Mizar Users
:: deftheorem defines OpenClosedSet LOPCLSET:def 1 :
theorem :: LOPCLSET:1
canceled;
theorem Th2: :: LOPCLSET:2
theorem Th3: :: LOPCLSET:3
theorem Th4: :: LOPCLSET:4
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
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
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
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
end;
:: deftheorem Def2 defines T_join LOPCLSET:def 2 :
:: deftheorem Def3 defines T_meet LOPCLSET:def 3 :
theorem :: LOPCLSET:5
theorem :: LOPCLSET:6
theorem Th7: :: LOPCLSET:7
theorem Th8: :: LOPCLSET:8
theorem Th9: :: LOPCLSET:9
theorem Th10: :: LOPCLSET:10
:: deftheorem defines OpenClosedSetLatt LOPCLSET:def 4 :
theorem :: LOPCLSET:11
theorem :: LOPCLSET:12
theorem :: LOPCLSET:13
theorem Th14: :: LOPCLSET:14
theorem :: LOPCLSET:15
theorem :: LOPCLSET:16
:: deftheorem defines ultraset LOPCLSET:def 5 :
theorem :: LOPCLSET:17
canceled;
theorem :: LOPCLSET:18
theorem Th19: :: LOPCLSET:19
:: deftheorem Def6 defines UFilter LOPCLSET:def 6 :
theorem Th20: :: LOPCLSET:20
theorem Th21: :: LOPCLSET:21
theorem Th22: :: LOPCLSET:22
theorem Th23: :: LOPCLSET:23
theorem Th24: :: LOPCLSET:24
:: deftheorem defines StoneR LOPCLSET:def 7 :
theorem :: LOPCLSET:25
theorem Th26: :: LOPCLSET:26
:: deftheorem Def8 defines StoneSpace LOPCLSET:def 8 :
theorem :: LOPCLSET:27
theorem Th28: :: LOPCLSET:28
:: deftheorem defines StoneBLattice LOPCLSET:def 9 :
Lm1:
for BL being non trivial B_Lattice
for p being Subset of (StoneSpace BL) st p in StoneR BL holds
p is open
theorem Th29: :: LOPCLSET:29
theorem :: LOPCLSET:30
theorem :: LOPCLSET:31
canceled;
theorem Th32: :: LOPCLSET:32
theorem :: LOPCLSET:33
canceled;
theorem Th34: :: LOPCLSET:34
theorem Th35: :: LOPCLSET:35
theorem Th36: :: LOPCLSET:36
theorem :: LOPCLSET:37
theorem Th38: :: LOPCLSET:38
Lm2:
for BL being non trivial B_Lattice holds StoneR BL c= OpenClosedSet (StoneSpace BL)
theorem :: LOPCLSET:39
canceled;
theorem Th40: :: LOPCLSET:40
theorem Th41: :: LOPCLSET:41
theorem Th42: :: LOPCLSET:42
theorem Th43: :: LOPCLSET:43
theorem :: LOPCLSET:44