:: by Adam Grabowski

::

:: Received February 13, 1998

:: Copyright (c) 1998-2019 Association of Mizar Users

definition

let S be non empty set ;

let a, b be Element of S;

ex b_{1} being sequence of S st

for i being Element of NAT holds

( ( ex k being Element of NAT st i = 2 * k implies b_{1} . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b_{1} . i = b ) )

for b_{1}, b_{2} being sequence of S st ( for i being Element of NAT holds

( ( ex k being Element of NAT st i = 2 * k implies b_{1} . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b_{1} . i = b ) ) ) & ( for i being Element of NAT holds

( ( ex k being Element of NAT st i = 2 * k implies b_{2} . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b_{2} . i = b ) ) ) holds

b_{1} = b_{2}

end;
let a, b be Element of S;

func (a,b) ,... -> sequence of S means :Def1: :: WAYBEL17:def 1

for i being Element of NAT holds

( ( ex k being Element of NAT st i = 2 * k implies it . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies it . i = b ) );

existence for i being Element of NAT holds

( ( ex k being Element of NAT st i = 2 * k implies it . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies it . i = b ) );

ex b

for i being Element of NAT holds

( ( ex k being Element of NAT st i = 2 * k implies b

proof end;

uniqueness for b

( ( ex k being Element of NAT st i = 2 * k implies b

( ( ex k being Element of NAT st i = 2 * k implies b

b

proof end;

:: deftheorem Def1 defines ,... WAYBEL17:def 1 :

for S being non empty set

for a, b being Element of S

for b_{4} being sequence of S holds

( b_{4} = (a,b) ,... iff for i being Element of NAT holds

( ( ex k being Element of NAT st i = 2 * k implies b_{4} . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b_{4} . i = b ) ) );

for S being non empty set

for a, b being Element of S

for b

( b

( ( ex k being Element of NAT st i = 2 * k implies b

scheme :: WAYBEL17:sch 1

FuncFraenkelS{ F_{1}() -> non empty TopRelStr , F_{2}() -> non empty TopRelStr , F_{3}( set ) -> Element of F_{2}(), F_{4}() -> Function, P_{1}[ set ] } :

FuncFraenkelS{ F

F_{4}() .: { F_{3}(x) where x is Element of F_{1}() : P_{1}[x] } = { (F_{4}() . F_{3}(x)) where x is Element of F_{1}() : P_{1}[x] }

provided
proof end;

scheme :: WAYBEL17:sch 2

FuncFraenkelSL{ F_{1}() -> LATTICE, F_{2}() -> LATTICE, F_{3}( set ) -> Element of F_{2}(), F_{4}() -> Function, P_{1}[ set ] } :

FuncFraenkelSL{ F

F_{4}() .: { F_{3}(x) where x is Element of F_{1}() : P_{1}[x] } = { (F_{4}() . F_{3}(x)) where x is Element of F_{1}() : P_{1}[x] }

provided
proof end;

theorem Th1: :: WAYBEL17:1

for S, T being non empty reflexive RelStr

for f being Function of S,T

for P being lower Subset of T st f is monotone holds

f " P is lower

for f being Function of S,T

for P being lower Subset of T st f is monotone holds

f " P is lower

proof end;

theorem :: WAYBEL17:2

for S, T being non empty reflexive RelStr

for f being Function of S,T

for P being upper Subset of T st f is monotone holds

f " P is upper

for f being Function of S,T

for P being upper Subset of T st f is monotone holds

f " P is upper

proof end;

Lm1: for T being up-complete LATTICE

for x being Element of T holds downarrow x is directly_closed

proof end;

Lm2: for T being up-complete Scott TopLattice

for x being Element of T holds Cl {x} = downarrow x

proof end;

Lm3: for T being up-complete Scott TopLattice

for x being Element of T holds downarrow x is closed

proof end;

theorem Th3: :: WAYBEL17:3

for S, T being non empty reflexive antisymmetric RelStr

for f being Function of S,T st f is directed-sups-preserving holds

f is monotone

for f being Function of S,T st f is directed-sups-preserving holds

f is monotone

proof end;

registration

let S, T be non empty reflexive antisymmetric RelStr ;

for b_{1} being Function of S,T st b_{1} is directed-sups-preserving holds

b_{1} is monotone
by Th3;

end;
cluster Function-like quasi_total directed-sups-preserving -> monotone for Element of K32(K33( the carrier of S, the carrier of T));

coherence for b

b

theorem Th4: :: WAYBEL17:4

for S, T being up-complete Scott TopLattice

for f being Function of S,T st f is continuous holds

f is monotone

for f being Function of S,T st f is continuous holds

f is monotone

proof end;

registration

let S, T be up-complete Scott TopLattice;

coherence

for b_{1} being Function of S,T st b_{1} is continuous holds

b_{1} is monotone ;

by Th4;

end;
cluster Function-like quasi_total continuous -> monotone for Element of K32(K33( the carrier of S, the carrier of T));

correctness coherence

for b

b

by Th4;

Lm4: for S, T being non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr

for f being Function of S,T st f is directed-sups-preserving holds

f is continuous

proof end;

registration
end;

registration
end;

definition

let S, T be up-complete Scott TopLattice;

ex b_{1} being strict full SubRelStr of MonMaps (S,T) st

for f being Function of S,T holds

( f in the carrier of b_{1} iff f is continuous )

for b_{1}, b_{2} being strict full SubRelStr of MonMaps (S,T) st ( for f being Function of S,T holds

( f in the carrier of b_{1} iff f is continuous ) ) & ( for f being Function of S,T holds

( f in the carrier of b_{2} iff f is continuous ) ) holds

b_{1} = b_{2}

end;
func SCMaps (S,T) -> strict full SubRelStr of MonMaps (S,T) means :Def2: :: WAYBEL17:def 2

for f being Function of S,T holds

( f in the carrier of it iff f is continuous );

existence for f being Function of S,T holds

( f in the carrier of it iff f is continuous );

ex b

for f being Function of S,T holds

( f in the carrier of b

proof end;

uniqueness for b

( f in the carrier of b

( f in the carrier of b

b

proof end;

:: deftheorem Def2 defines SCMaps WAYBEL17:def 2 :

for S, T being up-complete Scott TopLattice

for b_{3} being strict full SubRelStr of MonMaps (S,T) holds

( b_{3} = SCMaps (S,T) iff for f being Function of S,T holds

( f in the carrier of b_{3} iff f is continuous ) );

for S, T being up-complete Scott TopLattice

for b

( b

( f in the carrier of b

registration
end;

definition

let S be non empty RelStr ;

let a, b be Element of S;

ex b_{1} being non empty strict NetStr over S st

( the carrier of b_{1} = NAT & the mapping of b_{1} = (a,b) ,... & ( for i, j being Element of b_{1}

for i9, j9 being Element of NAT st i = i9 & j = j9 holds

( i <= j iff i9 <= j9 ) ) )

for b_{1}, b_{2} being non empty strict NetStr over S st the carrier of b_{1} = NAT & the mapping of b_{1} = (a,b) ,... & ( for i, j being Element of b_{1}

for i9, j9 being Element of NAT st i = i9 & j = j9 holds

( i <= j iff i9 <= j9 ) ) & the carrier of b_{2} = NAT & the mapping of b_{2} = (a,b) ,... & ( for i, j being Element of b_{2}

for i9, j9 being Element of NAT st i = i9 & j = j9 holds

( i <= j iff i9 <= j9 ) ) holds

b_{1} = b_{2}

end;
let a, b be Element of S;

func Net-Str (a,b) -> non empty strict NetStr over S means :Def3: :: WAYBEL17:def 3

( the carrier of it = NAT & the mapping of it = (a,b) ,... & ( for i, j being Element of it

for i9, j9 being Element of NAT st i = i9 & j = j9 holds

( i <= j iff i9 <= j9 ) ) );

existence ( the carrier of it = NAT & the mapping of it = (a,b) ,... & ( for i, j being Element of it

for i9, j9 being Element of NAT st i = i9 & j = j9 holds

( i <= j iff i9 <= j9 ) ) );

ex b

( the carrier of b

for i9, j9 being Element of NAT st i = i9 & j = j9 holds

( i <= j iff i9 <= j9 ) ) )

proof end;

uniqueness for b

for i9, j9 being Element of NAT st i = i9 & j = j9 holds

( i <= j iff i9 <= j9 ) ) & the carrier of b

for i9, j9 being Element of NAT st i = i9 & j = j9 holds

( i <= j iff i9 <= j9 ) ) holds

b

proof end;

:: deftheorem Def3 defines Net-Str WAYBEL17:def 3 :

for S being non empty RelStr

for a, b being Element of S

for b_{4} being non empty strict NetStr over S holds

( b_{4} = Net-Str (a,b) iff ( the carrier of b_{4} = NAT & the mapping of b_{4} = (a,b) ,... & ( for i, j being Element of b_{4}

for i9, j9 being Element of NAT st i = i9 & j = j9 holds

( i <= j iff i9 <= j9 ) ) ) );

for S being non empty RelStr

for a, b being Element of S

for b

( b

for i9, j9 being Element of NAT st i = i9 & j = j9 holds

( i <= j iff i9 <= j9 ) ) ) );

registration

let S be non empty RelStr ;

let a, b be Element of S;

coherence

( Net-Str (a,b) is reflexive & Net-Str (a,b) is transitive & Net-Str (a,b) is directed & Net-Str (a,b) is antisymmetric )

end;
let a, b be Element of S;

coherence

( Net-Str (a,b) is reflexive & Net-Str (a,b) is transitive & Net-Str (a,b) is directed & Net-Str (a,b) is antisymmetric )

proof end;

theorem Th5: :: WAYBEL17:5

for S being non empty RelStr

for a, b being Element of S

for i being Element of (Net-Str (a,b)) holds

( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )

for a, b being Element of S

for i being Element of (Net-Str (a,b)) holds

( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )

proof end;

theorem Th6: :: WAYBEL17:6

for S being non empty RelStr

for a, b being Element of S

for i, j being Element of (Net-Str (a,b))

for i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = j holds

( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )

for a, b being Element of S

for i, j being Element of (Net-Str (a,b))

for i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = j holds

( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )

proof end;

Lm5: for S being with_infima Poset

for a, b being Element of S st a <= b holds

lim_inf (Net-Str (a,b)) = a

proof end;

theorem Th8: :: WAYBEL17:8

for S, T being with_infima Poset

for a, b being Element of S

for f being Function of S,T holds lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)

for a, b being Element of S

for f being Function of S,T holds lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)

proof end;

definition

let S be non empty RelStr ;

let D be non empty Subset of S;

coherence

NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #) is strict NetStr over S;

;

end;
let D be non empty Subset of S;

func Net-Str D -> strict NetStr over S equals :: WAYBEL17:def 4

NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #);

correctness NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #);

coherence

NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #) is strict NetStr over S;

;

:: deftheorem defines Net-Str WAYBEL17:def 4 :

for S being non empty RelStr

for D being non empty Subset of S holds Net-Str D = NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #);

for S being non empty RelStr

for D being non empty Subset of S holds Net-Str D = NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #);

theorem Th9: :: WAYBEL17:9

for S being non empty reflexive RelStr

for D being non empty Subset of S holds Net-Str D = Net-Str (D,((id the carrier of S) | D))

for D being non empty Subset of S holds Net-Str D = Net-Str (D,((id the carrier of S) | D))

proof end;

registration

let S be non empty reflexive RelStr ;

let D be non empty directed Subset of S;

coherence

( not Net-Str D is empty & Net-Str D is directed & Net-Str D is reflexive )

end;
let D be non empty directed Subset of S;

coherence

( not Net-Str D is empty & Net-Str D is directed & Net-Str D is reflexive )

proof end;

registration

let S be non empty reflexive transitive RelStr ;

let D be non empty directed Subset of S;

coherence

Net-Str D is transitive ;

end;
let D be non empty directed Subset of S;

coherence

Net-Str D is transitive ;

registration

let S be non empty reflexive RelStr ;

let D be non empty directed Subset of S;

coherence

Net-Str D is monotone

end;
let D be non empty directed Subset of S;

coherence

Net-Str D is monotone

proof end;

Lm6: for R being up-complete LATTICE

for N being reflexive monotone net of R holds lim_inf N = sup N

proof end;

theorem Th10: :: WAYBEL17:10

for S being up-complete LATTICE

for D being non empty directed Subset of S holds lim_inf (Net-Str D) = sup D

for D being non empty directed Subset of S holds lim_inf (Net-Str D) = sup D

proof end;

theorem Th11: :: WAYBEL17:11

for S, T being LATTICE

for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds

f is monotone

for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds

f is monotone

proof end;

scheme :: WAYBEL17:sch 3

NetFraenkelS{ F_{1}() -> non empty TopRelStr , F_{2}() -> non empty TopRelStr , F_{3}() -> non empty TopRelStr , F_{4}( set ) -> Element of F_{3}(), F_{5}() -> Function, P_{1}[ set ] } :

NetFraenkelS{ F

F_{5}() .: { F_{4}(x) where x is Element of F_{1}() : P_{1}[x] } = { (F_{5}() . F_{4}(x)) where x is Element of F_{2}() : P_{1}[x] }

provided
proof end;

theorem Th12: :: WAYBEL17:12

for S, T being lower-bounded continuous LATTICE

for f being Function of S,T st f is directed-sups-preserving holds

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)

for f being Function of S,T st f is directed-sups-preserving holds

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)

proof end;

theorem Th13: :: WAYBEL17:13

for S being LATTICE

for T being lower-bounded up-complete LATTICE

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

f is monotone

for T being lower-bounded up-complete LATTICE

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

f is monotone

proof end;

theorem Th14: :: WAYBEL17:14

for S being lower-bounded up-complete LATTICE

for T being lower-bounded continuous LATTICE

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

for T being lower-bounded continuous LATTICE

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

proof end;

theorem Th15: :: WAYBEL17:15

for S, T being non empty RelStr

for D being Subset of S

for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds

sup (f .: D) <= f . (sup D)

for D being Subset of S

for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds

sup (f .: D) <= f . (sup D)

proof end;

theorem Th16: :: WAYBEL17:16

for S, T being non empty reflexive antisymmetric RelStr

for D being non empty directed Subset of S

for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) & f is monotone holds

sup (f .: D) <= f . (sup D)

for D being non empty directed Subset of S

for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) & f is monotone holds

sup (f .: D) <= f . (sup D)

proof end;

theorem :: WAYBEL17:17

for S, T being non empty RelStr

for D being Subset of S

for f being Function of S,T st ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds

f . (inf D) <= inf (f .: D)

for D being Subset of S

for f being Function of S,T st ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds

f . (inf D) <= inf (f .: D)

proof end;

Lm7: for S, T being complete LATTICE

for D being Subset of S

for f being Function of S,T st f is monotone holds

f . ("/\" (D,S)) <= inf (f .: D)

proof end;

theorem Th18: :: WAYBEL17:18

for S, T being up-complete LATTICE

for f being Function of S,T

for N being non empty monotone NetStr over S st f is monotone holds

f * N is monotone

for f being Function of S,T

for N being non empty monotone NetStr over S st f is monotone holds

f * N is monotone

proof end;

registration

let S, T be up-complete LATTICE;

let f be monotone Function of S,T;

let N be non empty monotone NetStr over S;

coherence

f * N is monotone by Th18;

end;
let f be monotone Function of S,T;

let N be non empty monotone NetStr over S;

coherence

f * N is monotone by Th18;

theorem :: WAYBEL17:19

for S, T being up-complete LATTICE

for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds

for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D)

for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds

for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D)

proof end;

Lm8: for S, T being complete LATTICE

for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds

f is directed-sups-preserving

proof end;

theorem Th20: :: WAYBEL17:20

for S, T being complete LATTICE

for f being Function of S,T

for N being net of S

for j being Element of N

for j9 being Element of (f * N) st j9 = j & f is monotone holds

f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)

for f being Function of S,T

for N being net of S

for j being Element of N

for j9 being Element of (f * N) st j9 = j & f is monotone holds

f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)

proof end;

Lm9: for S, T being complete Scott TopLattice

for f being continuous Function of S,T

for N being net of S holds f . (lim_inf N) <= lim_inf (f * N)

proof end;

Lm10: for L being continuous Scott TopLattice

for p being Element of L

for S being Subset of L st S is open & p in S holds

ex q being Element of L st

( q << p & q in S )

proof end;

Lm11: for L being lower-bounded continuous Scott TopLattice

for x being Element of L holds wayabove x is open

proof end;

Lm12: for L being lower-bounded continuous Scott TopLattice

for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of

proof end;

Lm13: for T being lower-bounded continuous Scott TopLattice holds { (wayabove x) where x is Element of T : verum } is Basis of T

proof end;

Lm14: for T being lower-bounded continuous Scott TopLattice

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

proof end;

Lm15: for S, T being lower-bounded continuous Scott TopLattice

for f being Function of S,T st ( for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ) holds

f is continuous

proof end;

:: Proposition 2.1, p. 112, (1) <=> (2)

theorem :: WAYBEL17:21

:: Proposition 2.1, p. 112, (1) <=> (3)

theorem Th22: :: WAYBEL17:22

for S, T being complete Scott TopLattice

for f being Function of S,T holds

( f is continuous iff f is directed-sups-preserving )

for f being Function of S,T holds

( f is continuous iff f is directed-sups-preserving )

proof end;

registration

let S, T be complete Scott TopLattice;

for b_{1} being Function of S,T st b_{1} is continuous holds

b_{1} is directed-sups-preserving
by Th22;

for b_{1} being Function of S,T st b_{1} is directed-sups-preserving holds

b_{1} is continuous
by Th22;

end;
cluster Function-like quasi_total continuous -> directed-sups-preserving for Element of K32(K33( the carrier of S, the carrier of T));

coherence for b

b

cluster Function-like quasi_total directed-sups-preserving -> continuous for Element of K32(K33( the carrier of S, the carrier of T));

coherence for b

b

Lm16: for S, T being complete continuous Scott TopLattice

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

f is directed-sups-preserving

proof end;

:: Proposition 2.1, p. 112, (1) <=> (4)

theorem Th23: :: WAYBEL17:23

for S, T being complete continuous Scott TopLattice

for f being Function of S,T holds

( f is continuous iff for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) )

for f being Function of S,T holds

( f is continuous iff for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) )

proof end;

:: Proposition 2.1, p. 112, (1) <=> (5)

theorem Th24: :: WAYBEL17:24

for S, T being complete continuous Scott TopLattice

for f being Function of S,T holds

( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) )

for f being Function of S,T holds

( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) )

proof end;

Lm17: for S, T being complete Scott TopLattice

for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ) holds

for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )

proof end;

Lm18: for S, T being complete Scott TopLattice

for f being Function of S,T st T is algebraic & ( for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) holds

for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) )

proof end;

Lm19: for S, T being complete Scott TopLattice

for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)

proof end;

theorem Th25: :: WAYBEL17:25

for S being LATTICE

for T being complete LATTICE

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) holds

f is monotone

for T being complete LATTICE

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) holds

f is monotone

proof end;

theorem Th26: :: WAYBEL17:26

for S, T being complete Scott TopLattice

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) holds

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) holds

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)

proof end;

:: Proposition 2.1, p. 112, (1) <=> (6)

theorem :: WAYBEL17:27

for S, T being complete Scott TopLattice

for f being Function of S,T st S is algebraic & T is algebraic holds

( f is continuous iff for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )

for f being Function of S,T st S is algebraic & T is algebraic holds

( f is continuous iff for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )

proof end;

:: Proposition 2.1, p. 112, (1) <=> (7)

theorem :: WAYBEL17:28

for S, T being complete Scott TopLattice

for f being Function of S,T st S is algebraic & T is algebraic holds

( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )

for f being Function of S,T st S is algebraic & T is algebraic holds

( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )

proof end;

theorem :: WAYBEL17:29

for S, T being non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr

for f being Function of S,T st f is directed-sups-preserving holds

f is continuous by Lm4;

for f being Function of S,T st f is directed-sups-preserving holds

f is continuous by Lm4;