:: Scott-Continuous Functions
:: by Adam Grabowski
::
:: Received February 13, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

definition
let S be non empty set ;
let a, b be Element of S;
func(a,b) ,...  ->  Function of NAT,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
 ex b1 being Function of NAT,S st
for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b1 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b1 . i = b ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,S st ( for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b1 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b1 . i = b ) ) ) & ( for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b2 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b2 . i = b ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines ,... WAYBEL17:def_1_:_
 for S being non empty set
for a, b being Element of S
for b4 being Function of NAT,S holds
( b4 = (a,b) ,... iff for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b4 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b4 . i = b ) ) );

scheme :: WAYBEL17:sch 1
FuncFraenkelS{ F1() ->  non empty TopRelStr , F2() ->  non empty TopRelStr , F3( set ) ->  Element of F2(), F4() ->  Function, P1[ set ] } :
 F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  =  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }
provided
A1: the carrier of F2() c= dom F4()
proofend;

scheme :: WAYBEL17:sch 2
FuncFraenkelSL{ F1() ->  LATTICE, F2() ->  LATTICE, F3( set ) ->  Element of F2(), F4() ->  Function, P1[ set ] } :
 F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  =  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }
provided
A1: the carrier of F2() c= dom F4()
proofend;

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
proofend;

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
proofend;

Lm1:  for T being up-complete LATTICE
for x being Element of T holds downarrow x is directly_closed
proofend;

Lm2:  for T being up-complete Scott TopLattice
for x being Element of T holds Cl {x} = downarrow x
proofend;

Lm3:  for T being up-complete Scott TopLattice
for x being Element of T holds downarrow x is closed
proofend;

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
proofend;

registration
let S, T be non empty reflexive antisymmetric RelStr ;
cluster Function-like quasi_total directed-sups-preserving  ->  monotone for Element of K32(K33( the carrier of S, the carrier of T));
coherence
 for b1 being Function of S,T st b1 is directed-sups-preserving holds
b1 is monotone by Th3;
end;

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
proofend;

registration
let S, T be up-complete Scott TopLattice;
cluster Function-like quasi_total continuous  ->  monotone for Element of K32(K33( the carrier of S, the carrier of T));
correctness
coherence
for b1 being Function of S,T st b1 is continuous holds
b1 is monotone ;
by Th4;
end;

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
proofend;

begin

registration
let S be set ;
let T be reflexive RelStr ;
clusterS --> T ->  reflexive-yielding ;
coherence
 S --> T is reflexive-yielding
proofend;
end;

registration
let S be non empty set ;
let T be complete LATTICE;
clusterT |^ S ->  complete ;
coherence
 T |^ S is complete
proofend;
end;

definition
let S, T be up-complete Scott TopLattice;
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
 ex b1 being strict full SubRelStr of MonMaps (S,T) st
for f being Function of S,T holds
( f in the carrier of b1 iff f is continuous )
proofend;
uniqueness
 for b1, b2 being strict full SubRelStr of MonMaps (S,T) st ( for f being Function of S,T holds
( f in the carrier of b1 iff f is continuous ) ) & ( for f being Function of S,T holds
( f in the carrier of b2 iff f is continuous ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines SCMaps WAYBEL17:def_2_:_
 for S, T being up-complete Scott TopLattice
for b3 being strict full SubRelStr of MonMaps (S,T) holds
( b3 = SCMaps (S,T) iff for f being Function of S,T holds
( f in the carrier of b3 iff f is continuous ) );

registration
let S, T be up-complete Scott TopLattice;
cluster SCMaps (S,T) ->  non empty strict full ;
coherence
 not SCMaps (S,T) is empty
proofend;
end;

begin

definition
let S be non empty RelStr ;
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
 ex b1 being non empty strict NetStr over S st
( the carrier of b1 = NAT &amp; the mapping of b1 = (a,b) ,... &amp; ( for i, j being Element of b1
for i9, j9 being Element of NAT st i = i9 &amp; j = j9 holds
( i <= j iff i9 <= j9 ) ) )
proofend;
uniqueness
 for b1, b2 being non empty strict NetStr over S st the carrier of b1 = NAT &amp; the mapping of b1 = (a,b) ,... &amp; ( for i, j being Element of b1
for i9, j9 being Element of NAT st i = i9 &amp; j = j9 holds
( i <= j iff i9 <= j9 ) ) &amp; the carrier of b2 = NAT &amp; the mapping of b2 = (a,b) ,... &amp; ( for i, j being Element of b2
for i9, j9 being Element of NAT st i = i9 &amp; j = j9 holds
( i <= j iff i9 <= j9 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Net-Str WAYBEL17:def_3_:_
 for S being non empty RelStr
for a, b being Element of S
for b4 being non empty strict NetStr over S holds
( b4 = Net-Str (a,b) iff ( the carrier of b4 = NAT &amp; the mapping of b4 = (a,b) ,... &amp; ( for i, j being Element of b4
for i9, j9 being Element of NAT st i = i9 &amp; j = j9 holds
( i <= j iff i9 <= j9 ) ) ) );

registration
let S be non empty RelStr ;
let a, b be Element of S;
cluster Net-Str (a,b) ->  non empty reflexive transitive antisymmetric strict directed ;
coherence
 ( Net-Str (a,b) is reflexive &amp; Net-Str (a,b) is transitive &amp; Net-Str (a,b) is directed &amp; Net-Str (a,b) is antisymmetric )
proofend;
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 )
proofend;

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 &amp; j9 = i9 + 1 &amp; j9 = j holds
( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) &amp; ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )
proofend;

theorem Th7: :: WAYBEL17:7
for S being with_infima Poset
for a, b being Element of S holds lim_inf (Net-Str (a,b)) = a "/\" b
proofend;

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
proofend;

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)
proofend;

definition
let S be non empty RelStr ;
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
coherence
NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #) is strict NetStr over S;
;
end;

:: 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) #);

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))
proofend;

registration
let S be non empty reflexive RelStr ;
let D be non empty directed Subset of S;
cluster Net-Str D ->  non empty reflexive strict directed ;
coherence
 ( not Net-Str D is empty &amp; Net-Str D is directed &amp; Net-Str D is reflexive )
proofend;
end;

registration
let S be non empty reflexive transitive RelStr ;
let D be non empty directed Subset of S;
cluster Net-Str D ->  transitive strict ;
coherence
 Net-Str D is transitive ;
end;

registration
let S be non empty reflexive RelStr ;
let D be non empty directed Subset of S;
cluster Net-Str D ->  strict monotone ;
coherence
 Net-Str D is monotone
proofend;
end;

Lm6:  for R being up-complete LATTICE
for N being reflexive monotone net of R holds lim_inf N = sup N
proofend;

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
proofend;

begin

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
proofend;

scheme :: WAYBEL17:sch 3
NetFraenkelS{ F1() ->  non empty TopRelStr , F2() ->  non empty TopRelStr , F3() ->  non empty TopRelStr , F4( set ) ->  Element of F3(), F5() ->  Function, P1[ set ] } :
 F5() .:  {  F4(x) where x is Element of F1() : P1[x]  }  =  {  (F5() . F4(x)) where x is Element of F2() : P1[x]  }
provided
A1: the carrier of F3() c= dom F5() and
A2: the carrier of F1() = the carrier of F2()
proofend;

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)
proofend;

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
proofend;

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 &amp; y << f . w ) )
proofend;

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 &amp; ex_sup_of f .: D,T ) or ( S is complete &amp; S is antisymmetric &amp; T is complete &amp; T is antisymmetric ) ) &amp; f is monotone holds
sup (f .: D) <= f . (sup D)
proofend;

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 &amp; ex_sup_of f .: D,T ) or ( S is up-complete &amp; T is up-complete ) ) &amp; f is monotone holds
sup (f .: D) <= f . (sup D)
proofend;

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 &amp; ex_inf_of f .: D,T ) or ( S is complete &amp; S is antisymmetric &amp; T is complete &amp; T is antisymmetric ) ) &amp; f is monotone holds
f . (inf D) <= inf (f .: D)
proofend;

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)
proofend;

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
proofend;

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;
clusterf * N ->  monotone ;
coherence
 f * N is monotone by Th18;
end;

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)
proofend;

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
proofend;

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 &amp; 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)
proofend;

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)
proofend;

Lm10:  for L being continuous Scott TopLattice
for p being Element of L
for S being Subset of L st S is open &amp; p in S holds
ex q being Element of L st
( q << p &amp; q in S )
proofend;

Lm11:  for L being lower-bounded continuous Scott TopLattice
for x being Element of L holds wayabove x is open
proofend;

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
proofend;

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

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  }
proofend;

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 &amp; y << f . w ) ) ) holds
f is continuous
proofend;

begin

:: Proposition 2.1, p. 112, (1) <=> (2)
theorem :: WAYBEL17:21
for S, T being complete Scott TopLattice
for f being Function of S,T holds
( f is continuous iff for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) by Lm4, Lm8, Lm9;

:: 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 )
proofend;

registration
let S, T be complete Scott TopLattice;
cluster Function-like quasi_total continuous  ->  directed-sups-preserving for Element of K32(K33( the carrier of S, the carrier of T));
coherence
 for b1 being Function of S,T st b1 is continuous holds
b1 is directed-sups-preserving by Th22;
cluster Function-like quasi_total directed-sups-preserving  ->  continuous for Element of K32(K33( the carrier of S, the carrier of T));
coherence
 for b1 being Function of S,T st b1 is directed-sups-preserving holds
b1 is continuous by Th22;
end;

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
proofend;

:: 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 &amp; y << f . w ) ) )
proofend;

:: 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) )
proofend;

Lm17:  for S, T being complete Scott TopLattice
for f being Function of S,T st S is algebraic &amp; T is algebraic &amp; ( 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 &amp; 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) &amp; j <= x &amp; k <= f . j ) )
proofend;

Lm18:  for S, T being complete Scott TopLattice
for f being Function of S,T st T is algebraic &amp; ( 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) &amp; j <= x &amp; 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 &amp; y << f . w ) )
proofend;

Lm19:  for S, T being complete Scott TopLattice
for f being Function of S,T st S is algebraic &amp; T is algebraic &amp; ( 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 &amp; w is compact )  }  ,T)
proofend;

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 &amp; w is compact )  }  ,T) ) holds
f is monotone
proofend;

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 &amp; 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)
proofend;

:: 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 &amp; 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) &amp; j <= x &amp; k <= f . j ) ) )
proofend;

:: 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 &amp; 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 &amp; w is compact )  }  ,T) )
proofend;

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;