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

definition

let S be non empty set ;
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
ex b₁ being sequence of S st
for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b₁ . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b₁ . i = b ) )

proof end;

uniqueness
for b₁, b₂ being sequence of S st ( for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b₁ . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b₁ . i = b ) ) ) & ( for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b₂ . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b₂ . i = b ) ) ) holds
b₁ = b₂

proof end;

end;

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

scheme :: WAYBEL17:sch 1
FuncFraenkelS{ F₁() -> non empty TopRelStr , F₂() -> non empty TopRelStr , F₃( set ) -> Element of F₂(), F₄() -> Function, P₁[ set ] } :

F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] } = { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] }

provided

A1: the carrier of F₂() c= dom F₄()

proof end;

scheme :: WAYBEL17:sch 2
FuncFraenkelSL{ F₁() -> LATTICE, F₂() -> LATTICE, F₃( set ) -> Element of F₂(), F₄() -> Function, P₁[ set ] } :

F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] } = { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] }

provided

A1: the carrier of F₂() c= dom F₄()

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

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

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

proof end;

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 b₁ being Function of S,T st b₁ is directed-sups-preserving holds
b₁ 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

proof end;

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 b₁ being Function of S,T st b₁ is continuous holds
b₁ 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

proof end;

registration

let S be set ;
let T be reflexive RelStr ;

cluster S --> T -> reflexive-yielding ;

coherence
S --> T is reflexive-yielding

proof end;

end;

registration

let S be non empty set ;
let T be complete LATTICE;

cluster T |^ S -> complete ;

coherence
T |^ S is complete

proof end;

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 b₁ being strict full SubRelStr of MonMaps (S,T) st
for f being Function of S,T holds
( f in the carrier of b₁ iff f is continuous )

proof end;

uniqueness
for b₁, b₂ being strict full SubRelStr of MonMaps (S,T) st ( for f being Function of S,T holds
( f in the carrier of b₁ iff f is continuous ) ) & ( for f being Function of S,T holds
( f in the carrier of b₂ iff f is continuous ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines SCMaps WAYBEL17:def 2 :
for S, T being up-complete Scott TopLattice
for b₃ being strict full SubRelStr of MonMaps (S,T) holds
( b₃ = SCMaps (S,T) iff for f being Function of S,T holds
( f in the carrier of b₃ 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

proof end;

end;

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 b₁ being non empty strict NetStr over S st
( the carrier of b₁ = NAT & the mapping of b₁ = (a,b) ,... & ( for i, j being Element 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₁, b₂ being non empty strict NetStr over S st the carrier of b₁ = NAT & the mapping of b₁ = (a,b) ,... & ( for i, j being Element of b₁
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) & the carrier of b₂ = NAT & the mapping of b₂ = (a,b) ,... & ( for i, j being Element of b₂
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Net-Str WAYBEL17:def 3 :
for S being non empty RelStr
for a, b being Element of S
for b₄ being non empty strict NetStr over S holds
( b₄ = Net-Str (a,b) iff ( the carrier of b₄ = NAT & the mapping of b₄ = (a,b) ,... & ( for i, j being Element of 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;

cluster Net-Str (a,b) -> non empty reflexive transitive antisymmetric strict directed ;

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;

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 )

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

proof end;

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

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)

proof end;

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

proof end;

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 & Net-Str D is directed & Net-Str D is reflexive )

proof end;

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

proof end;

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

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

proof end;

scheme :: WAYBEL17:sch 3
NetFraenkelS{ F₁() -> non empty TopRelStr , F₂() -> non empty TopRelStr , F₃() -> non empty TopRelStr , F₄( set ) -> Element of F₃(), F₅() -> Function, P₁[ set ] } :

F₅() .: { F₄(x) where x is Element of F₁() : P₁[x] } = { (F₅() . F₄(x)) where x is Element of F₂() : P₁[x] }

provided

A1: the carrier of F₃() c= dom F₅() and
A2: the carrier of F₁() = the carrier of F₂()

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)

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

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

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)

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)

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)

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

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;

cluster f * 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)

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)

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

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 )

proof end;

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 b₁ being Function of S,T st b₁ is continuous holds
b₁ 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 b₁ being Function of S,T st b₁ is directed-sups-preserving holds
b₁ 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

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

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

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

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)

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

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

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;