begin
theorem Th1:
theorem Th2:
:: deftheorem defines Topology_of OPENLATT:def 1 :
definition
let T be non
empty TopSpace;
func Top_Union T -> BinOp of
(Topology_of T) means :
Def2:
for
P,
Q being
Element of
Topology_of T holds
it . P,
Q = P \/ Q;
existence
ex b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . P,Q = P \/ Q
uniqueness
for b1, b2 being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b1 . P,Q = P \/ Q ) & ( for P, Q being Element of Topology_of T holds b2 . P,Q = P \/ Q ) holds
b1 = b2
func Top_Meet T -> BinOp of
(Topology_of T) means :
Def3:
for
P,
Q being
Element of
Topology_of T holds
it . P,
Q = P /\ Q;
existence
ex b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . P,Q = P /\ Q
uniqueness
for b1, b2 being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b1 . P,Q = P /\ Q ) & ( for P, Q being Element of Topology_of T holds b2 . P,Q = P /\ Q ) holds
b1 = b2
end;
:: deftheorem Def2 defines Top_Union OPENLATT:def 2 :
:: deftheorem Def3 defines Top_Meet OPENLATT:def 3 :
theorem
canceled;
theorem Th4:
:: deftheorem defines Open_setLatt OPENLATT:def 4 :
theorem
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
:: deftheorem defines F_primeSet OPENLATT:def 5 :
theorem Th12:
:: deftheorem Def6 defines StoneH OPENLATT:def 6 :
theorem Th13:
theorem Th14:
:: deftheorem defines StoneS OPENLATT:def 7 :
theorem Th15:
theorem Th16:
theorem Th17:
:: deftheorem defines SF_have OPENLATT:def 8 :
theorem Th18:
Lm1:
for L being D_Lattice
for F being Filter of L
for b, a being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
definition
let L be
D_Lattice;
func Set_Union L -> BinOp of
(StoneS L) means :
Def9:
for
A,
B being
Element of
StoneS L holds
it . A,
B = A \/ B;
existence
ex b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . A,B = A \/ B
uniqueness
for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . A,B = A \/ B ) & ( for A, B being Element of StoneS L holds b2 . A,B = A \/ B ) holds
b1 = b2
func Set_Meet L -> BinOp of
(StoneS L) means :
Def10:
for
A,
B being
Element of
StoneS L holds
it . A,
B = A /\ B;
existence
ex b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . A,B = A /\ B
uniqueness
for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . A,B = A /\ B ) & ( for A, B being Element of StoneS L holds b2 . A,B = A /\ B ) holds
b1 = b2
end;
:: deftheorem Def9 defines Set_Union OPENLATT:def 9 :
:: deftheorem Def10 defines Set_Meet OPENLATT:def 10 :
theorem Th26:
:: deftheorem defines StoneLatt OPENLATT:def 11 :
theorem
theorem
theorem
theorem Th30:
theorem
theorem
theorem Th33:
theorem Th34:
theorem Th35:
:: deftheorem Def12 defines HTopSpace OPENLATT:def 12 :
theorem
theorem Th37:
theorem
canceled;
theorem Th39:
theorem
theorem
theorem