begin
:: deftheorem Def1 defines lower WAYBEL19:def 1 :
for T being non empty TopRelStr holds
( T is lower iff { ((uparrow x) `) where x is Element of T : verum } is prebasis of T );
theorem Th1:
theorem Th2:
:: deftheorem Def2 defines omega WAYBEL19:def 2 :
for R being non empty RelStr
for b2 being Subset-Family of R holds
( b2 = omega R iff for T being correct lower TopAugmentation of R holds b2 = the topology of T );
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
theorem Th14:
theorem Th15:
theorem
theorem
begin
scheme
TopInd{
F1()
-> TopLattice,
P1[
set ] } :
for
A being
Subset of
F1() st
A is
open holds
P1[
A]
provided
A1:
ex
K being
prebasis of
F1() st
for
A being
Subset of
F1() st
A in K holds
P1[
A]
and A2:
for
F being
Subset-Family of
F1() st ( for
A being
Subset of
F1() st
A in F holds
P1[
A] ) holds
P1[
union F]
and A3:
for
A1,
A2 being
Subset of
F1() st
P1[
A1] &
P1[
A2] holds
P1[
A1 /\ A2]
and A4:
P1[
[#] F1()]
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
begin
:: deftheorem Def3 defines Lawson WAYBEL19:def 3 :
for T being non empty reflexive TopRelStr holds
( T is Lawson iff (omega T) \/ (sigma T) is prebasis of T );
theorem Th29:
theorem Th30:
theorem
theorem
:: deftheorem Def4 defines lambda WAYBEL19:def 4 :
for T being complete LATTICE
for b2 being Subset-Family of T holds
( b2 = lambda T iff for S being correct Lawson TopAugmentation of T holds b2 = the topology of S );
theorem Th33:
theorem
Lm2:
for T being LATTICE
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A is property(S) ) holds
union F is property(S)
Lm3:
for T being LATTICE
for A1, A2 being Subset of T st A1 is property(S) & A2 is property(S) holds
A1 /\ A2 is property(S)
Lm4:
for T being LATTICE holds [#] T is property(S)
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem
theorem
theorem