begin
:: deftheorem defines OpenClosedSet LOPCLSET:def 1 :
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
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:
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:
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
theorem
theorem
theorem
theorem Th9:
theorem Th10:
:: deftheorem defines OpenClosedSetLatt LOPCLSET:def 4 :
theorem
theorem
theorem
theorem Th14:
theorem
theorem
:: deftheorem defines ultraset LOPCLSET:def 5 :
theorem
canceled;
theorem
theorem Th19:
:: deftheorem Def6 defines UFilter LOPCLSET:def 6 :
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
:: deftheorem defines StoneR LOPCLSET:def 7 :
theorem
theorem Th26:
:: deftheorem Def8 defines StoneSpace LOPCLSET:def 8 :
theorem
theorem Th28:
:: 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:
theorem
theorem
canceled;
theorem Th32:
theorem
canceled;
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
Lm2:
for BL being non trivial B_Lattice holds StoneR BL c= OpenClosedSet (StoneSpace BL)
theorem
canceled;
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem