begin
:: 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 ) } ;
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 :
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
theorem
theorem
theorem
theorem Th9:
theorem Th10:
:: 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
theorem
theorem
theorem
canceled;
theorem
theorem
:: 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 } ;
theorem
canceled;
theorem
theorem Th19:
:: 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 Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
:: deftheorem defines StoneR LOPCLSET:def 7 :
for BL being non trivial B_Lattice holds StoneR BL = rng (UFilter BL);
theorem
theorem Th26:
:: 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 } ) );
theorem
theorem Th28:
:: 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
theorem
canceled;
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
canceled;
theorem Th43:
theorem