:: by Artur Korni{\l}owicz

::

:: Received January 6, 2000

:: Copyright (c) 2000-2018 Association of Mizar Users

theorem Th1: :: WAYBEL30:1

for x being set

for D being non empty set holds x /\ (union D) = union { (x /\ d) where d is Element of D : verum }

for D being non empty set holds x /\ (union D) = union { (x /\ d) where d is Element of D : verum }

proof end;

theorem Th2: :: WAYBEL30:2

for R being non empty reflexive transitive RelStr

for D being non empty directed Subset of (InclPoset (Ids R)) holds union D is Ideal of R

for D being non empty directed Subset of (InclPoset (Ids R)) holds union D is Ideal of R

proof end;

Lm1: now :: thesis: for R being non empty reflexive transitive RelStr

for D being non empty directed Subset of (InclPoset (Ids R))

for UD being Element of (InclPoset (Ids R)) st UD = union D holds

D is_<=_than UD

for D being non empty directed Subset of (InclPoset (Ids R))

for UD being Element of (InclPoset (Ids R)) st UD = union D holds

D is_<=_than UD

let R be non empty reflexive transitive RelStr ; :: thesis: for D being non empty directed Subset of (InclPoset (Ids R))

for UD being Element of (InclPoset (Ids R)) st UD = union D holds

D is_<=_than UD

let D be non empty directed Subset of (InclPoset (Ids R)); :: thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds

D is_<=_than UD

let UD be Element of (InclPoset (Ids R)); :: thesis: ( UD = union D implies D is_<=_than UD )

assume A1: UD = union D ; :: thesis: D is_<=_than UD

thus D is_<=_than UD :: thesis: verum

end;
for UD being Element of (InclPoset (Ids R)) st UD = union D holds

D is_<=_than UD

let D be non empty directed Subset of (InclPoset (Ids R)); :: thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds

D is_<=_than UD

let UD be Element of (InclPoset (Ids R)); :: thesis: ( UD = union D implies D is_<=_than UD )

assume A1: UD = union D ; :: thesis: D is_<=_than UD

thus D is_<=_than UD :: thesis: verum

proof

let d be Element of (InclPoset (Ids R)); :: according to LATTICE3:def 9 :: thesis: ( not d in D or d <= UD )

assume A2: d in D ; :: thesis: d <= UD

d c= UD by A1, A2, TARSKI:def 4;

hence d <= UD by YELLOW_1:3; :: thesis: verum

end;
assume A2: d in D ; :: thesis: d <= UD

d c= UD by A1, A2, TARSKI:def 4;

hence d <= UD by YELLOW_1:3; :: thesis: verum

Lm2: now :: thesis: for R being non empty reflexive transitive RelStr

for D being non empty directed Subset of (InclPoset (Ids R))

for UD being Element of (InclPoset (Ids R)) st UD = union D holds

for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b

for D being non empty directed Subset of (InclPoset (Ids R))

for UD being Element of (InclPoset (Ids R)) st UD = union D holds

for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b

let R be non empty reflexive transitive RelStr ; :: thesis: for D being non empty directed Subset of (InclPoset (Ids R))

for UD being Element of (InclPoset (Ids R)) st UD = union D holds

for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b

let D be non empty directed Subset of (InclPoset (Ids R)); :: thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds

for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b

let UD be Element of (InclPoset (Ids R)); :: thesis: ( UD = union D implies for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b )

assume A1: UD = union D ; :: thesis: for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b

thus for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b :: thesis: verum

end;
for UD being Element of (InclPoset (Ids R)) st UD = union D holds

for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b

let D be non empty directed Subset of (InclPoset (Ids R)); :: thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds

for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b

let UD be Element of (InclPoset (Ids R)); :: thesis: ( UD = union D implies for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b )

assume A1: UD = union D ; :: thesis: for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b

thus for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds

UD <= b :: thesis: verum

proof

let b be Element of (InclPoset (Ids R)); :: thesis: ( b is_>=_than D implies UD <= b )

assume A2: for a being Element of (InclPoset (Ids R)) st a in D holds

b >= a ; :: according to LATTICE3:def 9 :: thesis: UD <= b

UD c= b

end;
assume A2: for a being Element of (InclPoset (Ids R)) st a in D holds

b >= a ; :: according to LATTICE3:def 9 :: thesis: UD <= b

UD c= b

proof

hence
UD <= b
by YELLOW_1:3; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UD or x in b )

assume x in UD ; :: thesis: x in b

then consider Z being set such that

A3: x in Z and

A4: Z in D by A1, TARSKI:def 4;

reconsider Z = Z as Element of (InclPoset (Ids R)) by A4;

b >= Z by A2, A4;

then Z c= b by YELLOW_1:3;

hence x in b by A3; :: thesis: verum

end;
assume x in UD ; :: thesis: x in b

then consider Z being set such that

A3: x in Z and

A4: Z in D by A1, TARSKI:def 4;

reconsider Z = Z as Element of (InclPoset (Ids R)) by A4;

b >= Z by A2, A4;

then Z c= b by YELLOW_1:3;

hence x in b by A3; :: thesis: verum

:: Exercise 2.16 (i), p. 16

registration

let R be non empty reflexive transitive RelStr ;

coherence

InclPoset (Ids R) is up-complete

end;
coherence

InclPoset (Ids R) is up-complete

proof end;

theorem Th3: :: WAYBEL30:3

for R being non empty reflexive transitive RelStr

for D being non empty directed Subset of (InclPoset (Ids R)) holds sup D = union D

for D being non empty directed Subset of (InclPoset (Ids R)) holds sup D = union D

proof end;

theorem Th4: :: WAYBEL30:4

for R being Semilattice

for D being non empty directed Subset of (InclPoset (Ids R))

for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }

for D being non empty directed Subset of (InclPoset (Ids R))

for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }

proof end;

:: Exercise 4.8 (i), p. 33

registration

let R be 1 -element RelStr ;

coherence

for b_{1} being TopAugmentation of R holds b_{1} is trivial

end;
coherence

for b

proof end;

theorem :: WAYBEL30:5

for S being complete Scott TopLattice

for T being complete LATTICE

for A being Scott TopAugmentation of T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds

TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)

for T being complete LATTICE

for A being Scott TopAugmentation of T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds

TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)

proof end;

theorem :: WAYBEL30:6

for N being complete Lawson TopLattice

for T being complete LATTICE

for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds

TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)

for T being complete LATTICE

for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds

TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)

proof end;

theorem :: WAYBEL30:7

for N being complete Lawson TopLattice

for S being Scott TopAugmentation of N

for A being Subset of N

for J being Subset of S st A = J & J is closed holds

A is closed

for S being Scott TopAugmentation of N

for A being Subset of N

for J being Subset of S st A = J & J is closed holds

A is closed

proof end;

registration

let S be complete Scott TopLattice;

coherence

( InclPoset (sigma S) is complete & not InclPoset (sigma S) is trivial ) ;

end;
coherence

( InclPoset (sigma S) is complete & not InclPoset (sigma S) is trivial ) ;

registration

let N be complete Lawson TopLattice;

coherence

( InclPoset (sigma N) is complete & not InclPoset (sigma N) is trivial ) ;

coherence

( InclPoset (lambda N) is complete & not InclPoset (lambda N) is trivial )

end;
coherence

( InclPoset (sigma N) is complete & not InclPoset (sigma N) is trivial ) ;

coherence

( InclPoset (lambda N) is complete & not InclPoset (lambda N) is trivial )

proof end;

theorem Th8: :: WAYBEL30:8

for T being non empty reflexive RelStr holds sigma T c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }

proof end;

theorem :: WAYBEL30:11

for M, N being complete LATTICE st RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) holds

lambda M = lambda N

lambda M = lambda N

proof end;

registration

coherence

for b_{1} being 1 -element reflexive TopRelStr st b_{1} is TopSpace-like holds

b_{1} is Scott
by TDLAT_3:15;

end;
for b

b

registration

for b_{1} being complete TopLattice st b_{1} is trivial holds

b_{1} is Lawson
end;

cluster trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete -> complete Lawson for TopLattice;

coherence for b

b

proof end;

registration

ex b_{1} being complete TopLattice st

( b_{1} is strict & b_{1} is continuous & b_{1} is lower-bounded & b_{1} is meet-continuous & b_{1} is Scott )
end;

cluster non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V158() up-complete /\-complete with_suprema with_infima complete strict Scott continuous non void meet-continuous for TopLattice;

existence ex b

( b

proof end;

registration

ex b_{1} being complete TopLattice st

( b_{1} is strict & b_{1} is continuous & b_{1} is compact & b_{1} is Hausdorff & b_{1} is Lawson )
end;

cluster non empty TopSpace-like Hausdorff reflexive transitive antisymmetric lower-bounded upper-bounded V158() up-complete /\-complete with_suprema with_infima complete strict Lawson continuous non void compact for TopLattice;

existence ex b

( b

proof end;

theorem Th13: :: WAYBEL30:13

for N being meet-continuous LATTICE

for A being Subset of N st A is property(S) holds

uparrow A is property(S)

for A being Subset of N st A is property(S) holds

uparrow A is property(S)

proof end;

registration

let N be meet-continuous LATTICE;

let A be property(S) Subset of N;

coherence

uparrow A is property(S) by Th13;

end;
let A be property(S) Subset of N;

coherence

uparrow A is property(S) by Th13;

:: Proposition 2.1 (i), p. 153

theorem Th14: :: WAYBEL30:14

for N being complete Lawson meet-continuous TopLattice

for S being Scott TopAugmentation of N

for A being Subset of N st A in lambda N holds

uparrow A in sigma S

for S being Scott TopAugmentation of N

for A being Subset of N st A in lambda N holds

uparrow A in sigma S

proof end;

theorem Th15: :: WAYBEL30:15

for N being complete Lawson meet-continuous TopLattice

for S being Scott TopAugmentation of N

for A being Subset of N

for J being Subset of S st A = J & A is open holds

uparrow J is open

for S being Scott TopAugmentation of N

for A being Subset of N

for J being Subset of S st A = J & A is open holds

uparrow J is open

proof end;

theorem Th16: :: WAYBEL30:16

for N being complete Lawson meet-continuous TopLattice

for S being Scott TopAugmentation of N

for x being Point of S

for y being Point of N

for J being Basis of y st x = y holds

{ (uparrow A) where A is Subset of N : A in J } is Basis of x

for S being Scott TopAugmentation of N

for x being Point of S

for y being Point of N

for J being Basis of y st x = y holds

{ (uparrow A) where A is Subset of N : A in J } is Basis of x

proof end;

:: Proposition 2.1 (ii), p. 153

theorem Th17: :: WAYBEL30:17

for N being complete Lawson meet-continuous TopLattice

for S being Scott TopAugmentation of N

for X being upper Subset of N

for Y being Subset of S st X = Y holds

Int X = Int Y

for S being Scott TopAugmentation of N

for X being upper Subset of N

for Y being Subset of S st X = Y holds

Int X = Int Y

proof end;

:: Proposition 2.1 (iii), p. 153

theorem :: WAYBEL30:18

for N being complete Lawson meet-continuous TopLattice

for S being Scott TopAugmentation of N

for X being lower Subset of N

for Y being Subset of S st X = Y holds

Cl X = Cl Y

for S being Scott TopAugmentation of N

for X being lower Subset of N

for Y being Subset of S st X = Y holds

Cl X = Cl Y

proof end;

theorem Th19: :: WAYBEL30:19

for M, N being complete LATTICE

for LM being correct Lawson TopAugmentation of M

for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds

the topology of [:LM,LN:] = lambda [:M,N:]

for LM being correct Lawson TopAugmentation of M

for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds

the topology of [:LM,LN:] = lambda [:M,N:]

proof end;

:: Proposition 2.2, p. 153

theorem Th20: :: WAYBEL30:20

for M, N being complete LATTICE

for P being correct Lawson TopAugmentation of [:M,N:]

for Q being correct Lawson TopAugmentation of M

for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds

TopStruct(# the carrier of P, the topology of P #) = [:Q,R:]

for P being correct Lawson TopAugmentation of [:M,N:]

for Q being correct Lawson TopAugmentation of M

for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds

TopStruct(# the carrier of P, the topology of P #) = [:Q,R:]

proof end;

:: Theorem 2.3, p. 153, first conjunct

theorem Th21: :: WAYBEL30:21

for N being complete Lawson meet-continuous TopLattice

for x being Element of N holds x "/\" is continuous

for x being Element of N holds x "/\" is continuous

proof end;

registration

let N be complete Lawson meet-continuous TopLattice;

let x be Element of N;

coherence

x "/\" is continuous by Th21;

end;
let x be Element of N;

coherence

x "/\" is continuous by Th21;

:: Theorem 2.3, p. 153, second conjunct

theorem Th22: :: WAYBEL30:22

for N being complete Lawson meet-continuous TopLattice st InclPoset (sigma N) is continuous holds

N is topological_semilattice

N is topological_semilattice

proof end;

Lm3: now :: thesis: for S, T, x1, x2 being set st x1 in S & x2 in T holds

<:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1]

<:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1]

let S, T, x1, x2 be set ; :: thesis: ( x1 in S & x2 in T implies <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1] )

assume that

A1: x1 in S and

A2: x2 in T ; :: thesis: <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1]

A3: dom <:(pr2 (S,T)),(pr1 (S,T)):> = (dom (pr2 (S,T))) /\ (dom (pr1 (S,T))) by FUNCT_3:def 7

.= (dom (pr2 (S,T))) /\ [:S,T:] by FUNCT_3:def 4

.= [:S,T:] /\ [:S,T:] by FUNCT_3:def 5

.= [:S,T:] ;

[x1,x2] in [:S,T:] by A1, A2, ZFMISC_1:87;

hence <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))] by A3, FUNCT_3:def 7

.= [x2,((pr1 (S,T)) . (x1,x2))] by A1, A2, FUNCT_3:def 5

.= [x2,x1] by A1, A2, FUNCT_3:def 4 ;

:: thesis: verum

end;
assume that

A1: x1 in S and

A2: x2 in T ; :: thesis: <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1]

A3: dom <:(pr2 (S,T)),(pr1 (S,T)):> = (dom (pr2 (S,T))) /\ (dom (pr1 (S,T))) by FUNCT_3:def 7

.= (dom (pr2 (S,T))) /\ [:S,T:] by FUNCT_3:def 4

.= [:S,T:] /\ [:S,T:] by FUNCT_3:def 5

.= [:S,T:] ;

[x1,x2] in [:S,T:] by A1, A2, ZFMISC_1:87;

hence <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))] by A3, FUNCT_3:def 7

.= [x2,((pr1 (S,T)) . (x1,x2))] by A1, A2, FUNCT_3:def 5

.= [x2,x1] by A1, A2, FUNCT_3:def 4 ;

:: thesis: verum

:: Proposition 2.4, p. 153

theorem :: WAYBEL30:23

for N being complete Lawson meet-continuous TopLattice st InclPoset (sigma N) is continuous holds

( N is Hausdorff iff for X being Subset of [:N,N:] st X = the InternalRel of N holds

X is closed )

( N is Hausdorff iff for X being Subset of [:N,N:] st X = the InternalRel of N holds

X is closed )

proof end;

:: Definition 2.5, p. 154

definition

let N be non empty reflexive RelStr ;

let X be Subset of N;

{ u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds

X meets D } is Subset of N

end;
let X be Subset of N;

func X ^0 -> Subset of N equals :: WAYBEL30:def 1

{ u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds

X meets D } ;

coherence { u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds

X meets D } ;

{ u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds

X meets D } is Subset of N

proof end;

:: deftheorem defines ^0 WAYBEL30:def 1 :

for N being non empty reflexive RelStr

for X being Subset of N holds X ^0 = { u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds

X meets D } ;

for N being non empty reflexive RelStr

for X being Subset of N holds X ^0 = { u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds

X meets D } ;

registration

let N be non empty reflexive antisymmetric RelStr ;

let X be empty Subset of N;

coherence

X ^0 is empty

end;
let X be empty Subset of N;

coherence

X ^0 is empty

proof end;

:: Remark 2.6 (i), p. 154

:: Remark 2.6 (ii), p. 154

:: Lemma 2.7 (i), p. 154

theorem Th27: :: WAYBEL30:27

for N being non empty reflexive RelStr

for X, Y being Subset of N holds (X ^0) \/ (Y ^0) c= (X \/ Y) ^0

for X, Y being Subset of N holds (X ^0) \/ (Y ^0) c= (X \/ Y) ^0

proof end;

:: Lemma 2.7 (ii), p. 154

theorem Th28: :: WAYBEL30:28

for N being meet-continuous LATTICE

for X, Y being upper Subset of N holds (X ^0) \/ (Y ^0) = (X \/ Y) ^0

for X, Y being upper Subset of N holds (X ^0) \/ (Y ^0) = (X \/ Y) ^0

proof end;

:: Lemma 2.8, p. 154

theorem Th29: :: WAYBEL30:29

for S being Scott meet-continuous TopLattice

for F being finite Subset of S holds Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F }

for F being finite Subset of S holds Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F }

proof end;

:: Theorem 2.9, p. 154

theorem Th30: :: WAYBEL30:30

for N being complete Lawson TopLattice holds

( N is continuous iff ( N is meet-continuous & N is Hausdorff ) )

( N is continuous iff ( N is meet-continuous & N is Hausdorff ) )

proof end;

registration

for b_{1} being complete TopLattice st b_{1} is continuous & b_{1} is Lawson holds

b_{1} is Hausdorff
;

for b_{1} being complete TopLattice st b_{1} is meet-continuous & b_{1} is Lawson & b_{1} is Hausdorff holds

b_{1} is continuous
by Th30;

end;

cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson continuous -> Hausdorff complete for TopLattice;

coherence for b

b

cluster TopSpace-like Hausdorff reflexive transitive antisymmetric with_suprema with_infima complete Lawson meet-continuous -> complete continuous for TopLattice;

coherence for b

b

:: Definition 2.10, p. 155

definition

let N be non empty TopRelStr ;

end;
attr N is with_small_semilattices means :: WAYBEL30:def 2

for x being Point of N ex J being basis of x st

for A being Subset of N st A in J holds

subrelstr A is meet-inheriting ;

for x being Point of N ex J being basis of x st

for A being Subset of N st A in J holds

subrelstr A is meet-inheriting ;

attr N is with_compact_semilattices means :: WAYBEL30:def 3

for x being Point of N ex J being basis of x st

for A being Subset of N st A in J holds

( subrelstr A is meet-inheriting & A is compact );

for x being Point of N ex J being basis of x st

for A being Subset of N st A in J holds

( subrelstr A is meet-inheriting & A is compact );

attr N is with_open_semilattices means :Def4: :: WAYBEL30:def 4

for x being Point of N ex J being Basis of x st

for A being Subset of N st A in J holds

subrelstr A is meet-inheriting ;

for x being Point of N ex J being Basis of x st

for A being Subset of N st A in J holds

subrelstr A is meet-inheriting ;

:: deftheorem defines with_small_semilattices WAYBEL30:def 2 :

for N being non empty TopRelStr holds

( N is with_small_semilattices iff for x being Point of N ex J being basis of x st

for A being Subset of N st A in J holds

subrelstr A is meet-inheriting );

for N being non empty TopRelStr holds

( N is with_small_semilattices iff for x being Point of N ex J being basis of x st

for A being Subset of N st A in J holds

subrelstr A is meet-inheriting );

:: deftheorem defines with_compact_semilattices WAYBEL30:def 3 :

for N being non empty TopRelStr holds

( N is with_compact_semilattices iff for x being Point of N ex J being basis of x st

for A being Subset of N st A in J holds

( subrelstr A is meet-inheriting & A is compact ) );

for N being non empty TopRelStr holds

( N is with_compact_semilattices iff for x being Point of N ex J being basis of x st

for A being Subset of N st A in J holds

( subrelstr A is meet-inheriting & A is compact ) );

:: deftheorem Def4 defines with_open_semilattices WAYBEL30:def 4 :

for N being non empty TopRelStr holds

( N is with_open_semilattices iff for x being Point of N ex J being Basis of x st

for A being Subset of N st A in J holds

subrelstr A is meet-inheriting );

for N being non empty TopRelStr holds

( N is with_open_semilattices iff for x being Point of N ex J being Basis of x st

for A being Subset of N st A in J holds

subrelstr A is meet-inheriting );

registration

for b_{1} being non empty TopSpace-like TopRelStr st b_{1} is with_open_semilattices holds

b_{1} is with_small_semilattices

for b_{1} being non empty TopSpace-like TopRelStr st b_{1} is with_compact_semilattices holds

b_{1} is with_small_semilattices

for b_{1} being non empty TopRelStr st b_{1} is anti-discrete holds

( b_{1} is with_small_semilattices & b_{1} is with_open_semilattices )

for b_{1} being 1 -element TopRelStr st b_{1} is reflexive & b_{1} is TopSpace-like holds

b_{1} is with_compact_semilattices
end;

cluster non empty TopSpace-like with_open_semilattices -> non empty TopSpace-like with_small_semilattices for TopRelStr ;

coherence for b

b

proof end;

cluster non empty TopSpace-like with_compact_semilattices -> non empty TopSpace-like with_small_semilattices for TopRelStr ;

coherence for b

b

proof end;

cluster non empty anti-discrete -> non empty with_small_semilattices with_open_semilattices for TopRelStr ;

coherence for b

( b

proof end;

coherence for b

b

proof end;

registration

ex b_{1} being TopLattice st

( b_{1} is strict & b_{1} is trivial & b_{1} is lower )
end;

cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima strict lower non void for TopLattice;

existence ex b

( b

proof end;

theorem Th31: :: WAYBEL30:31

for N being with_infima topological_semilattice TopPoset

for C being Subset of N st subrelstr C is meet-inheriting holds

subrelstr (Cl C) is meet-inheriting

for C being Subset of N st subrelstr C is meet-inheriting holds

subrelstr (Cl C) is meet-inheriting

proof end;

:: Theorem 2.11, p. 155

theorem Th32: :: WAYBEL30:32

for N being complete Lawson meet-continuous TopLattice

for S being Scott TopAugmentation of N holds

( ( for x being Point of S ex J being Basis of x st

for W being Subset of S st W in J holds

W is Filter of S ) iff N is with_open_semilattices )

for S being Scott TopAugmentation of N holds

( ( for x being Point of S ex J being Basis of x st

for W being Subset of S st W in J holds

W is Filter of S ) iff N is with_open_semilattices )

proof end;

:: Theorem 2.12, p. 155, r => l

theorem Th33: :: WAYBEL30:33

for N being complete Lawson TopLattice

for S being Scott TopAugmentation of N

for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }

for S being Scott TopAugmentation of N

for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }

proof end;

:: Theorem 2.12, p. 155

theorem Th34: :: WAYBEL30:34

for N being complete Lawson meet-continuous TopLattice

for S being Scott TopAugmentation of N

for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }

for S being Scott TopAugmentation of N

for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }

proof end;

:: Theorem 2.13, p. 155, 1 <=> 2

theorem Th35: :: WAYBEL30:35

for N being complete Lawson meet-continuous TopLattice holds

( N is continuous iff ( N is with_open_semilattices & InclPoset (sigma N) is continuous ) )

( N is continuous iff ( N is with_open_semilattices & InclPoset (sigma N) is continuous ) )

proof end;

registration

for b_{1} being complete Lawson TopLattice st b_{1} is continuous holds

b_{1} is with_open_semilattices
by Th35;

end;

cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson continuous -> complete Lawson with_open_semilattices for TopLattice;

coherence for b

b

registration

let N be complete Lawson continuous TopLattice;

coherence

InclPoset (sigma N) is continuous by Th35;

end;
coherence

InclPoset (sigma N) is continuous by Th35;

:: Theorem 2.13, p. 155, 1 => 3

theorem :: WAYBEL30:36

for N being complete Lawson continuous TopLattice holds

( N is compact & N is Hausdorff & N is topological_semilattice & N is with_open_semilattices )

( N is compact & N is Hausdorff & N is topological_semilattice & N is with_open_semilattices )

proof end;

:: Theorem 2.13, p. 155, 3 => 3'

theorem :: WAYBEL30:37

for N being Hausdorff complete Lawson topological_semilattice with_open_semilattices TopLattice holds N is with_compact_semilattices

proof end;

:: Theorem 2.13, p. 155, 3' => 4

theorem :: WAYBEL30:38

for N being Hausdorff complete Lawson meet-continuous TopLattice

for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N)

for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N)

proof end;

:: Theorem 2.13, p. 155, 1 <=> 4

theorem :: WAYBEL30:39

for N being complete Lawson meet-continuous TopLattice holds

( N is continuous iff for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) )

( N is continuous iff for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) )

proof end;

:: Exercise 2.16, p. 156, 1 <=> 2

theorem Th40: :: WAYBEL30:40

for N being complete Lawson meet-continuous TopLattice holds

( N is algebraic iff ( N is with_open_semilattices & InclPoset (sigma N) is algebraic ) )

( N is algebraic iff ( N is with_open_semilattices & InclPoset (sigma N) is algebraic ) )

proof end;

registration

let N be complete algebraic Lawson meet-continuous TopLattice;

coherence

InclPoset (sigma N) is algebraic by Th40;

end;
coherence

InclPoset (sigma N) is algebraic by Th40;