:: WAYBEL17 semantic presentation 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 ) ) proof defpred S1[ set ] means ex k being Element of NAT st \$1 = 2 * k; deffunc H1( set ) -> Element of S = b; deffunc H2( set ) -> Element of S = a; consider f being Function such that A1: ( dom f = NAT & ( for x being set st x in NAT holds ( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) ) ) from PARTFUN1:sch_1(); A2: rng f c= {a,b} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in {a,b} ) assume x in rng f ; ::_thesis: x in {a,b} then consider y being set such that A3: y in dom f and A4: x = f . y by FUNCT_1:def_3; percases ( S1[y] or not S1[y] ) ; suppose S1[y] ; ::_thesis: x in {a,b} then f . y = a by A1; hence x in {a,b} by A4, TARSKI:def_2; ::_thesis: verum end; suppose not S1[y] ; ::_thesis: x in {a,b} then f . y = b by A1, A3; hence x in {a,b} by A4, TARSKI:def_2; ::_thesis: verum end; end; end; for y being set st y in {a,b} holds ex x being set st ( x in dom f & y = f . x ) proof let y be set ; ::_thesis: ( y in {a,b} implies ex x being set st ( x in dom f & y = f . x ) ) assume A5: y in {a,b} ; ::_thesis: ex x being set st ( x in dom f & y = f . x ) percases ( y = a or y = b ) by A5, TARSKI:def_2; supposeA6: y = a ; ::_thesis: ex x being set st ( x in dom f & y = f . x ) take 2 ; ::_thesis: ( 2 in dom f & y = f . 2 ) S1[2] proof take 1 ; ::_thesis: 2 = 2 * 1 thus 2 = 2 * 1 ; ::_thesis: verum end; hence ( 2 in dom f & y = f . 2 ) by A1, A6; ::_thesis: verum end; supposeA7: y = b ; ::_thesis: ex x being set st ( x in dom f & y = f . x ) take 1 ; ::_thesis: ( 1 in dom f & y = f . 1 ) for k being Element of NAT holds 1 <> 2 * k by NAT_1:15; hence ( 1 in dom f & y = f . 1 ) by A1, A7; ::_thesis: verum end; end; end; then {a,b} c= rng f by FUNCT_1:9; then rng f = {a,b} by A2, XBOOLE_0:def_10; then reconsider f = f as Function of NAT,S by A1, FUNCT_2:def_1, RELSET_1:4; take f ; ::_thesis: for i being Element of NAT holds ( ( ex k being Element of NAT st i = 2 * k implies f . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f . i = b ) ) let i be Element of NAT ; ::_thesis: ( ( ex k being Element of NAT st i = 2 * k implies f . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f . i = b ) ) thus ( ( ex k being Element of NAT st i = 2 * k implies f . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f . i = b ) ) by A1; ::_thesis: verum end; 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 proof let f1, f2 be Function of NAT,S; ::_thesis: ( ( for i being Element of NAT holds ( ( ex k being Element of NAT st i = 2 * k implies f1 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f1 . i = b ) ) ) & ( for i being Element of NAT holds ( ( ex k being Element of NAT st i = 2 * k implies f2 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f2 . i = b ) ) ) implies f1 = f2 ) A8: dom f1 = NAT by FUNCT_2:def_1; A9: dom f2 = NAT by FUNCT_2:def_1; assume that A10: for i being Element of NAT holds ( ( ex k being Element of NAT st i = 2 * k implies f1 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f1 . i = b ) ) and A11: for i being Element of NAT holds ( ( ex k being Element of NAT st i = 2 * k implies f2 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f2 . i = b ) ) ; ::_thesis: f1 = f2 for k being set st k in NAT holds f1 . k = f2 . k proof let k be set ; ::_thesis: ( k in NAT implies f1 . k = f2 . k ) assume k in NAT ; ::_thesis: f1 . k = f2 . k then reconsider k9 = k as Element of NAT ; percases ( ex l being Element of NAT st k = 2 * l or for l being Element of NAT holds not k = 2 * l ) ; supposeA12: ex l being Element of NAT st k = 2 * l ; ::_thesis: f1 . k = f2 . k then f1 . k = a by A10 .= f2 . k by A11, A12 ; hence f1 . k = f2 . k ; ::_thesis: verum end; supposeA13: for l being Element of NAT holds not k = 2 * l ; ::_thesis: f1 . k = f2 . k then f1 . k9 = b by A10 .= f2 . k9 by A11, A13 ; hence f1 . k = f2 . k ; ::_thesis: verum end; end; end; hence f1 = f2 by A8, A9, FUNCT_1:2; ::_thesis: verum end; 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() proof set f = F4(); thus F4() .: { F3(x) where x is Element of F1() : P1[x] } c= { (F4() . F3(x)) where x is Element of F1() : P1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { (F4() . F3(x)) where x is Element of F1() : P1[x] } c= F4() .: { F3(x) where x is Element of F1() : P1[x] } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F4() .: { F3(x) where x is Element of F1() : P1[x] } or y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ) assume y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } then consider z being set such that z in dom F4() and A2: z in { F3(x) where x is Element of F1() : P1[x] } and A3: y = F4() . z by FUNCT_1:def_6; ex x being Element of F1() st ( z = F3(x) & P1[x] ) by A2; hence y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } by A3; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } or y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ) assume y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ; ::_thesis: y in F4() .: { F3(x) where x is Element of F1() : P1[x] } then consider x being Element of F1() such that A4: y = F4() . F3(x) and A5: P1[x] ; A6: F3(x) in the carrier of F2() ; F3(x) in { F3(z) where z is Element of F1() : P1[z] } by A5; hence y in F4() .: { F3(x) where x is Element of F1() : P1[x] } by A1, A4, A6, FUNCT_1:def_6; ::_thesis: verum end; 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() proof set f = F4(); thus F4() .: { F3(x) where x is Element of F1() : P1[x] } c= { (F4() . F3(x)) where x is Element of F1() : P1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { (F4() . F3(x)) where x is Element of F1() : P1[x] } c= F4() .: { F3(x) where x is Element of F1() : P1[x] } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F4() .: { F3(x) where x is Element of F1() : P1[x] } or y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ) assume y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } then consider z being set such that z in dom F4() and A2: z in { F3(x) where x is Element of F1() : P1[x] } and A3: y = F4() . z by FUNCT_1:def_6; ex x being Element of F1() st ( z = F3(x) & P1[x] ) by A2; hence y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } by A3; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } or y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ) assume y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ; ::_thesis: y in F4() .: { F3(x) where x is Element of F1() : P1[x] } then consider x being Element of F1() such that A4: y = F4() . F3(x) and A5: P1[x] ; A6: F3(x) in the carrier of F2() ; F3(x) in { F3(z) where z is Element of F1() : P1[z] } by A5; hence y in F4() .: { F3(x) where x is Element of F1() : P1[x] } by A1, A4, A6, FUNCT_1:def_6; ::_thesis: verum 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 let S, T be non empty reflexive RelStr ; ::_thesis: for f being Function of S,T for P being lower Subset of T st f is monotone holds f " P is lower let f be Function of S,T; ::_thesis: for P being lower Subset of T st f is monotone holds f " P is lower let P be lower Subset of T; ::_thesis: ( f is monotone implies f " P is lower ) assume A1: f is monotone ; ::_thesis: f " P is lower for x, y being Element of S st x in f " P & y <= x holds y in f " P proof let x, y be Element of S; ::_thesis: ( x in f " P & y <= x implies y in f " P ) assume that A2: x in f " P and A3: y <= x ; ::_thesis: y in f " P A4: f . y <= f . x by A1, A3, WAYBEL_1:def_2; reconsider fy = f . y, fx = f . x as Element of T ; fx in P by A2, FUNCT_2:38; then fy in P by A4, WAYBEL_0:def_19; hence y in f " P by FUNCT_2:38; ::_thesis: verum end; hence f " P is lower by WAYBEL_0:def_19; ::_thesis: verum 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 let S, T be non empty reflexive RelStr ; ::_thesis: for f being Function of S,T for P being upper Subset of T st f is monotone holds f " P is upper let f be Function of S,T; ::_thesis: for P being upper Subset of T st f is monotone holds f " P is upper let P be upper Subset of T; ::_thesis: ( f is monotone implies f " P is upper ) assume A1: f is monotone ; ::_thesis: f " P is upper for x, y being Element of S st x in f " P & y >= x holds y in f " P proof let x, y be Element of S; ::_thesis: ( x in f " P & y >= x implies y in f " P ) assume that A2: x in f " P and A3: y >= x ; ::_thesis: y in f " P A4: f . y >= f . x by A1, A3, WAYBEL_1:def_2; reconsider fy = f . y, fx = f . x as Element of T ; fx in P by A2, FUNCT_2:38; then fy in P by A4, WAYBEL_0:def_20; hence y in f " P by FUNCT_2:38; ::_thesis: verum end; hence f " P is upper by WAYBEL_0:def_20; ::_thesis: verum end; Lm1: for T being up-complete LATTICE for x being Element of T holds downarrow x is directly_closed proof let T be up-complete LATTICE; ::_thesis: for x being Element of T holds downarrow x is directly_closed let x be Element of T; ::_thesis: downarrow x is directly_closed let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( not D c= downarrow x or "\/" (D,T) in downarrow x ) assume A1: D c= downarrow x ; ::_thesis: "\/" (D,T) in downarrow x A2: ex_sup_of D,T by WAYBEL_0:75; x is_>=_than D proof let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in D or b <= x ) assume b in D ; ::_thesis: b <= x hence b <= x by A1, WAYBEL_0:17; ::_thesis: verum end; then sup D <= x by A2, YELLOW_0:30; hence "\/" (D,T) in downarrow x by WAYBEL_0:17; ::_thesis: verum end; Lm2: for T being up-complete Scott TopLattice for x being Element of T holds Cl {x} = downarrow x proof let T be up-complete Scott TopLattice; ::_thesis: for x being Element of T holds Cl {x} = downarrow x let x be Element of T; ::_thesis: Cl {x} = downarrow x downarrow x is directly_closed by Lm1; then A1: downarrow x is closed by WAYBEL11:7; x <= x ; then x in downarrow x by WAYBEL_0:17; then A2: {x} c= downarrow x by ZFMISC_1:31; now__::_thesis:_for_C_being_Subset_of_T_st_{x}_c=_C_&_C_is_closed_holds_ downarrow_x_c=_C let C be Subset of T; ::_thesis: ( {x} c= C & C is closed implies downarrow x c= C ) assume A3: {x} c= C ; ::_thesis: ( C is closed implies downarrow x c= C ) reconsider D = C as Subset of T ; assume C is closed ; ::_thesis: downarrow x c= C then A4: D is lower by WAYBEL11:7; x in C by A3, ZFMISC_1:31; hence downarrow x c= C by A4, WAYBEL11:6; ::_thesis: verum end; hence Cl {x} = downarrow x by A1, A2, YELLOW_8:8; ::_thesis: verum end; Lm3: for T being up-complete Scott TopLattice for x being Element of T holds downarrow x is closed proof let T be up-complete Scott TopLattice; ::_thesis: for x being Element of T holds downarrow x is closed let x be Element of T; ::_thesis: downarrow x is closed Cl {x} = downarrow x by Lm2; hence downarrow x is closed ; ::_thesis: verum 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 let S, T be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of S,T st f is directed-sups-preserving holds f is monotone let f be Function of S,T; ::_thesis: ( f is directed-sups-preserving implies f is monotone ) assume A1: f is directed-sups-preserving ; ::_thesis: f is monotone let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y ) assume A2: x <= y ; ::_thesis: f . x <= f . y y <= y ; then A3: {x,y} is_<=_than y by A2, YELLOW_0:8; A4: for b being Element of S st {x,y} is_<=_than b holds y <= b by YELLOW_0:8; then A5: y = sup {x,y} by A3, YELLOW_0:30; A6: ex_sup_of {x,y},S by A3, A4, YELLOW_0:30; for a, b being Element of S st a in {x,y} & b in {x,y} holds ex z being Element of S st ( z in {x,y} & a <= z & b <= z ) proof let a, b be Element of S; ::_thesis: ( a in {x,y} & b in {x,y} implies ex z being Element of S st ( z in {x,y} & a <= z & b <= z ) ) assume that A7: a in {x,y} and A8: b in {x,y} ; ::_thesis: ex z being Element of S st ( z in {x,y} & a <= z & b <= z ) take y ; ::_thesis: ( y in {x,y} & a <= y & b <= y ) thus y in {x,y} by TARSKI:def_2; ::_thesis: ( a <= y & b <= y ) thus ( a <= y & b <= y ) by A2, A7, A8, TARSKI:def_2; ::_thesis: verum end; then ( {x,y} is directed & not {x,y} is empty ) by WAYBEL_0:def_1; then A9: f preserves_sup_of {x,y} by A1, WAYBEL_0:def_37; then A10: sup (f .: {x,y}) = f . y by A5, A6, WAYBEL_0:def_31; A11: dom f = the carrier of S by FUNCT_2:def_1; then A12: f . y = sup {(f . x),(f . y)} by A10, FUNCT_1:60; f .: {x,y} = {(f . x),(f . y)} by A11, FUNCT_1:60; then ex_sup_of {(f . x),(f . y)},T by A6, A9, WAYBEL_0:def_31; then {(f . x),(f . y)} is_<=_than f . y by A12, YELLOW_0:def_9; hence f . x <= f . y by YELLOW_0:8; ::_thesis: verum 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 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 proof let S, T be up-complete Scott TopLattice; ::_thesis: for f being Function of S,T st f is continuous holds f is monotone let f be Function of S,T; ::_thesis: ( f is continuous implies f is monotone ) assume A1: f is continuous ; ::_thesis: f is monotone let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y ) A2: dom f = the carrier of S by FUNCT_2:def_1; assume A3: x <= y ; ::_thesis: f . x <= f . y A4: [#] T <> {} ; f . x <= f . y proof set V = (downarrow (f . y)) ` ; set U1 = f " ((downarrow (f . y)) `); assume not f . x <= f . y ; ::_thesis: contradiction then not f . x in downarrow (f . y) by WAYBEL_0:17; then A5: f . x in (downarrow (f . y)) ` by XBOOLE_0:def_5; f . y <= f . y ; then A6: f . y in downarrow (f . y) by WAYBEL_0:17; downarrow (f . y) is closed by Lm3; then f " ((downarrow (f . y)) `) is open by A1, A4, TOPS_2:43; then reconsider U1 = f " ((downarrow (f . y)) `) as upper Subset of S by WAYBEL11:def_4; x in U1 by A2, A5, FUNCT_1:def_7; then y in U1 by A3, WAYBEL_0:def_20; then f . y in (downarrow (f . y)) ` by FUNCT_1:def_7; hence contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum end; hence f . x <= f . y ; ::_thesis: verum 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 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 proof let S, T be non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: for f being Function of S,T st f is directed-sups-preserving holds f is continuous let f be Function of S,T; ::_thesis: ( f is directed-sups-preserving implies f is continuous ) assume A1: f is directed-sups-preserving ; ::_thesis: f is continuous thus f is continuous ::_thesis: verum proof let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f " P1 is closed ) reconsider P19 = P1 as Subset of T ; assume P1 is closed ; ::_thesis: f " P1 is closed then A2: ( P19 is directly_closed & P19 is lower ) by WAYBEL11:7; now__::_thesis:_for_D_being_non_empty_directed_Subset_of_S_st_D_c=_f_"_P1_holds_ sup_D_in_f_"_P1 let D be non empty directed Subset of S; ::_thesis: ( D c= f " P1 implies sup D in f " P1 ) assume A3: D c= f " P1 ; ::_thesis: sup D in f " P1 A4: f preserves_sup_of D by A1, WAYBEL_0:def_37; ex_sup_of D,S by WAYBEL_0:75; then A5: sup (f .: D) = f . (sup D) by A4, WAYBEL_0:def_31; reconsider fD = f .: D as directed Subset of T by A1, YELLOW_2:15; fD c= P1 by A3, EQREL_1:46; then sup fD in P19 by A2, WAYBEL11:def_2; hence sup D in f " P1 by A5, FUNCT_2:38; ::_thesis: verum end; then ( f " P1 is directly_closed & f " P1 is lower ) by A1, A2, Th1, WAYBEL11:def_2; hence f " P1 is closed by WAYBEL11:7; ::_thesis: verum end; end; begin registration let S be set ; let T be reflexive RelStr ; clusterS --> T -> reflexive-yielding ; coherence S --> T is reflexive-yielding proof set f = S --> T; let W be RelStr ; :: according to WAYBEL_3:def_8 ::_thesis: ( not W in rng (S --> T) or W is reflexive ) assume W in rng (S --> T) ; ::_thesis: W is reflexive hence W is reflexive by TARSKI:def_1; ::_thesis: verum end; end; registration let S be non empty set ; let T be complete LATTICE; clusterT |^ S -> complete ; coherence T |^ S is complete proof A1: T |^ S = product (S --> T) by YELLOW_1:def_5; for i being Element of S holds (S --> T) . i is complete LATTICE by FUNCOP_1:7; hence T |^ S is complete by A1, WAYBEL_3:31; ::_thesis: verum 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 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 ) proof defpred S1[ set ] means ex f being Function of S,T st ( \$1 = f & f is continuous ); consider X being set such that A1: for a being set holds ( a in X iff ( a in the carrier of (MonMaps (S,T)) & S1[a] ) ) from XBOOLE_0:sch_1(); X c= the carrier of (MonMaps (S,T)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in the carrier of (MonMaps (S,T)) ) assume a in X ; ::_thesis: a in the carrier of (MonMaps (S,T)) hence a in the carrier of (MonMaps (S,T)) by A1; ::_thesis: verum end; then reconsider X = X as Subset of (MonMaps (S,T)) ; take SX = subrelstr X; ::_thesis: for f being Function of S,T holds ( f in the carrier of SX iff f is continuous ) let f be Function of S,T; ::_thesis: ( f in the carrier of SX iff f is continuous ) hereby ::_thesis: ( f is continuous implies f in the carrier of SX ) assume f in the carrier of SX ; ::_thesis: f is continuous then f in X by YELLOW_0:def_15; then ex f9 being Function of S,T st ( f9 = f & f9 is continuous ) by A1; hence f is continuous ; ::_thesis: verum end; assume A2: f is continuous ; ::_thesis: f in the carrier of SX f in Funcs ( the carrier of S, the carrier of T) by FUNCT_2:8; then f in the carrier of (MonMaps (S,T)) by A2, YELLOW_1:def_6; then f in X by A1, A2; hence f in the carrier of SX by YELLOW_0:def_15; ::_thesis: verum end; 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 proof let A1, A2 be strict full SubRelStr of MonMaps (S,T); ::_thesis: ( ( for f being Function of S,T holds ( f in the carrier of A1 iff f is continuous ) ) & ( for f being Function of S,T holds ( f in the carrier of A2 iff f is continuous ) ) implies A1 = A2 ) assume that A3: for f being Function of S,T holds ( f in the carrier of A1 iff f is continuous ) and A4: for f being Function of S,T holds ( f in the carrier of A2 iff f is continuous ) ; ::_thesis: A1 = A2 A5: the carrier of A1 c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13; A6: the carrier of A2 c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13; the carrier of A1 = the carrier of A2 proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of A2 c= the carrier of A1 let x be set ; ::_thesis: ( x in the carrier of A1 implies x in the carrier of A2 ) assume A7: x in the carrier of A1 ; ::_thesis: x in the carrier of A2 then reconsider y = x as Element of A1 ; reconsider y = y as Function of S,T by A5, A7, WAYBEL10:9; y is continuous by A3, A7; hence x in the carrier of A2 by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A2 or x in the carrier of A1 ) assume A8: x in the carrier of A2 ; ::_thesis: x in the carrier of A1 then reconsider y = x as Element of A2 ; reconsider y = y as Function of S,T by A6, A8, WAYBEL10:9; y is continuous by A4, A8; hence x in the carrier of A1 by A3; ::_thesis: verum end; hence A1 = A2 by YELLOW_0:57; ::_thesis: verum end; 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 proof set f = the continuous Function of S,T; the continuous Function of S,T in the carrier of (SCMaps (S,T)) by Def2; hence not SCMaps (S,T) is empty ; ::_thesis: verum end; 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 & the mapping of b1 = (a,b) ,... & ( for i, j being Element of b1 for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) ) ) proof defpred S1[ set , set ] means for i, j being Element of NAT st i = \$1 & j = \$2 holds i <= j; consider R being Relation of NAT,NAT such that A1: for x, y being Element of NAT holds ( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2(); reconsider R = R as Relation of NAT ; take N = NetStr(# NAT,R,((a,b) ,...) #); ::_thesis: ( the carrier of N = NAT & the mapping of N = (a,b) ,... & ( for i, j being Element of N for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) ) ) thus the carrier of N = NAT ; ::_thesis: ( the mapping of N = (a,b) ,... & ( for i, j being Element of N for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) ) ) thus the mapping of N = (a,b) ,... ; ::_thesis: for i, j being Element of N for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) let i, j be Element of N; ::_thesis: for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) let i9, j9 be Element of NAT ; ::_thesis: ( i = i9 & j = j9 implies ( i <= j iff i9 <= j9 ) ) assume that A2: i = i9 and A3: j = j9 ; ::_thesis: ( i <= j iff i9 <= j9 ) reconsider x = i, y = j as Element of NAT ; ( [x,y] in the InternalRel of N iff S1[x,y] ) by A1; hence ( i <= j iff i9 <= j9 ) by A2, A3, ORDERS_2:def_5; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict NetStr over S st the carrier of b1 = NAT & the mapping of b1 = (a,b) ,... & ( for i, j being Element of b1 for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) ) & the carrier of b2 = NAT & the mapping of b2 = (a,b) ,... & ( for i, j being Element of b2 for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) ) holds b1 = b2 proof let it1, it2 be non empty strict NetStr over S; ::_thesis: ( the carrier of it1 = NAT & the mapping of it1 = (a,b) ,... & ( for i, j being Element of it1 for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) ) & the carrier of it2 = NAT & the mapping of it2 = (a,b) ,... & ( for i, j being Element of it2 for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) ) implies it1 = it2 ) assume that A4: the carrier of it1 = NAT and A5: the mapping of it1 = (a,b) ,... and A6: for i, j being Element of it1 for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) and A7: the carrier of it2 = NAT and A8: the mapping of it2 = (a,b) ,... and A9: for i, j being Element of it2 for i9, j9 being Element of NAT st i = i9 & j = j9 holds ( i <= j iff i9 <= j9 ) ; ::_thesis: it1 = it2 the InternalRel of it1 = the InternalRel of it2 proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of it1 or [x,y] in the InternalRel of it2 ) & ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 ) ) hereby ::_thesis: ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 ) assume A10: [x,y] in the InternalRel of it1 ; ::_thesis: [x,y] in the InternalRel of it2 then reconsider i = x, j = y as Element of it1 by ZFMISC_1:87; reconsider i1 = i, i2 = j as Element of NAT by A4; reconsider i9 = x, j9 = y as Element of it2 by A4, A7, A10, ZFMISC_1:87; i <= j by A10, ORDERS_2:def_5; then i1 <= i2 by A6; then i9 <= j9 by A9; hence [x,y] in the InternalRel of it2 by ORDERS_2:def_5; ::_thesis: verum end; assume A11: [x,y] in the InternalRel of it2 ; ::_thesis: [x,y] in the InternalRel of it1 then reconsider i = x, j = y as Element of it2 by ZFMISC_1:87; reconsider i9 = x, j9 = y as Element of it1 by A4, A7, A11, ZFMISC_1:87; reconsider i1 = i, i2 = j as Element of NAT by A7; i <= j by A11, ORDERS_2:def_5; then i1 <= i2 by A9; then i9 <= j9 by A6; hence [x,y] in the InternalRel of it1 by ORDERS_2:def_5; ::_thesis: verum end; hence it1 = it2 by A4, A5, A7, A8; ::_thesis: verum end; 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 & the mapping of b4 = (a,b) ,... & ( for i, j being Element of b4 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 set L = Net-Str (a,b); thus Net-Str (a,b) is reflexive ::_thesis: ( Net-Str (a,b) is transitive & Net-Str (a,b) is directed & Net-Str (a,b) is antisymmetric ) proof let x be Element of (Net-Str (a,b)); :: according to YELLOW_0:def_1 ::_thesis: x <= x reconsider x9 = x as Element of NAT by Def3; x9 <= x9 ; hence x <= x by Def3; ::_thesis: verum end; thus Net-Str (a,b) is transitive ::_thesis: ( Net-Str (a,b) is directed & Net-Str (a,b) is antisymmetric ) proof let x, y, z be Element of (Net-Str (a,b)); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume that A1: x <= y and A2: y <= z ; ::_thesis: x <= z reconsider x9 = x, y9 = y, z9 = z as Element of NAT by Def3; A3: x9 <= y9 by A1, Def3; y9 <= z9 by A2, Def3; then x9 <= z9 by A3, XXREAL_0:2; hence x <= z by Def3; ::_thesis: verum end; [#] (Net-Str (a,b)) is directed proof let x, y be Element of (Net-Str (a,b)); :: according to WAYBEL_0:def_1 ::_thesis: ( not x in [#] (Net-Str (a,b)) or not y in [#] (Net-Str (a,b)) or ex b1 being Element of the carrier of (Net-Str (a,b)) st ( b1 in [#] (Net-Str (a,b)) & x <= b1 & y <= b1 ) ) assume that x in [#] (Net-Str (a,b)) and y in [#] (Net-Str (a,b)) ; ::_thesis: ex b1 being Element of the carrier of (Net-Str (a,b)) st ( b1 in [#] (Net-Str (a,b)) & x <= b1 & y <= b1 ) reconsider x9 = x, y9 = y as Element of NAT by Def3; set z9 = x9 + y9; reconsider z = x9 + y9 as Element of (Net-Str (a,b)) by Def3; reconsider z = z as Element of (Net-Str (a,b)) ; take z ; ::_thesis: ( z in [#] (Net-Str (a,b)) & x <= z & y <= z ) A4: x9 <= x9 + y9 by NAT_1:11; y9 <= x9 + y9 by NAT_1:11; hence ( z in [#] (Net-Str (a,b)) & x <= z & y <= z ) by A4, Def3; ::_thesis: verum end; hence Net-Str (a,b) is directed by WAYBEL_0:def_6; ::_thesis: Net-Str (a,b) is antisymmetric thus Net-Str (a,b) is antisymmetric ::_thesis: verum proof let x, y be Element of (Net-Str (a,b)); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y ) reconsider x9 = x, y9 = y as Element of NAT by Def3; assume that A5: x <= y and A6: y <= x ; ::_thesis: x = y A7: x9 <= y9 by A5, Def3; y9 <= x9 by A6, Def3; hence x = y by A7, XXREAL_0:1; ::_thesis: verum end; 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 let S be non empty RelStr ; ::_thesis: 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 ) let a, b be Element of S; ::_thesis: for i being Element of (Net-Str (a,b)) holds ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b ) let i be Element of (Net-Str (a,b)); ::_thesis: ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b ) set N = Net-Str (a,b); reconsider I = i as Element of NAT by Def3; A1: (Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3; defpred S1[ Element of NAT ] means ex k being Element of NAT st \$1 = 2 * k; percases ( S1[I] or not S1[I] ) ; suppose S1[I] ; ::_thesis: ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b ) hence ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b ) by A1, Def1; ::_thesis: verum end; suppose not S1[I] ; ::_thesis: ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b ) hence ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b ) by A1, Def1; ::_thesis: verum end; end; 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 let S be non empty RelStr ; ::_thesis: 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 ) ) let a, b be Element of S; ::_thesis: 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 ) ) let i, j be Element of (Net-Str (a,b)); ::_thesis: 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 ) ) let i9, j9 be Element of NAT ; ::_thesis: ( i9 = i & j9 = i9 + 1 & j9 = j implies ( ( (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 ) ) ) assume that A1: i9 = i and A2: j9 = i9 + 1 and A3: j9 = j ; ::_thesis: ( ( (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 ) ) percases ( a <> b or a = b ) ; supposeA4: a <> b ; ::_thesis: ( ( (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 ) ) defpred S1[ Element of NAT ] means ex k being Element of NAT st \$1 = 2 * k; thus ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) ::_thesis: ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) proof assume A5: (Net-Str (a,b)) . i = a ; ::_thesis: (Net-Str (a,b)) . j = b S1[i9] proof assume A6: not S1[i9] ; ::_thesis: contradiction (Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3 .= b by A1, A6, Def1 ; hence contradiction by A4, A5; ::_thesis: verum end; then A7: for k being Element of NAT holds j9 <> 2 * k by A2; (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3 .= b by A3, A7, Def1 ; hence (Net-Str (a,b)) . j = b ; ::_thesis: verum end; assume A8: (Net-Str (a,b)) . i = b ; ::_thesis: (Net-Str (a,b)) . j = a A9: not S1[i9] proof assume A10: S1[i9] ; ::_thesis: contradiction (Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3 .= a by A1, A10, Def1 ; hence contradiction by A4, A8; ::_thesis: verum end; A11: S1[j9] proof assume not S1[j9] ; ::_thesis: contradiction then ex kl being Element of NAT st j9 = (2 * kl) + 1 by SCHEME1:1; hence contradiction by A2, A9; ::_thesis: verum end; (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3 .= a by A3, A11, Def1 ; hence (Net-Str (a,b)) . j = a ; ::_thesis: verum end; suppose a = b ; ::_thesis: ( ( (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 ) ) hence ( ( (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 ) ) by Th5; ::_thesis: verum end; end; 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 let S be with_infima Poset; ::_thesis: for a, b being Element of S holds lim_inf (Net-Str (a,b)) = a "/\" b let a, b be Element of S; ::_thesis: lim_inf (Net-Str (a,b)) = a "/\" b set N = Net-Str (a,b); A1: for j being Element of (Net-Str (a,b)) holds { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } = {a,b} proof let j be Element of (Net-Str (a,b)); ::_thesis: { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } = {a,b} thus { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } c= {a,b} :: according to XBOOLE_0:def_10 ::_thesis: {a,b} c= { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } or x in {a,b} ) assume x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } ; ::_thesis: x in {a,b} then consider i1 being Element of (Net-Str (a,b)) such that A2: x = (Net-Str (a,b)) . i1 and i1 >= j ; ( (Net-Str (a,b)) . i1 = a or (Net-Str (a,b)) . i1 = b ) by Th5; hence x in {a,b} by A2, TARSKI:def_2; ::_thesis: verum end; thus {a,b} c= { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} or x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } ) assume A3: x in {a,b} ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } reconsider J = j as Element of NAT by Def3; defpred S1[ Element of NAT ] means ex k being Element of NAT st \$1 = 2 * k; percases ( x = a or x = b ) by A3, TARSKI:def_2; supposeA4: x = a ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } now__::_thesis:_x_in__{__((Net-Str_(a,b))_._i)_where_i_is_Element_of_(Net-Str_(a,b))_:_i_>=_j__}_ percases ( S1[J] or not S1[J] ) ; supposeA5: S1[J] ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } A6: (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3 .= a by A5, Def1 ; j <= j ; hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } by A4, A6; ::_thesis: verum end; supposeA7: not S1[J] ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } A8: (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3 .= b by A7, Def1 ; reconsider k = J + 1 as Element of (Net-Str (a,b)) by Def3; A9: (Net-Str (a,b)) . k = a by A8, Th6; J + 1 >= J by NAT_1:11; then k >= j by Def3; hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } by A4, A9; ::_thesis: verum end; end; end; hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } ; ::_thesis: verum end; supposeA10: x = b ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } now__::_thesis:_x_in__{__((Net-Str_(a,b))_._i)_where_i_is_Element_of_(Net-Str_(a,b))_:_i_>=_j__}_ percases ( not S1[J] or S1[J] ) ; supposeA11: not S1[J] ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } A12: (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3 .= b by A11, Def1 ; j <= j ; hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } by A10, A12; ::_thesis: verum end; supposeA13: S1[J] ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } A14: (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3 .= a by A13, Def1 ; reconsider k = J + 1 as Element of (Net-Str (a,b)) by Def3; A15: (Net-Str (a,b)) . k = b by A14, Th6; J + 1 >= J by NAT_1:11; then k >= j by Def3; hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } by A10, A15; ::_thesis: verum end; end; end; hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } ; ::_thesis: verum end; end; end; end; defpred S1[ Element of (Net-Str (a,b)), Element of (Net-Str (a,b))] means \$1 >= \$2; deffunc H1( Element of (Net-Str (a,b))) -> set = { ((Net-Str (a,b)) . i1) where i1 is Element of (Net-Str (a,b)) : S1[i1,\$1] } ; defpred S2[ set ] means verum; deffunc H2( Element of (Net-Str (a,b))) -> Element of K32( the carrier of S) = {a,b}; deffunc H3( Element of (Net-Str (a,b))) -> Element of the carrier of S = "/\" (H1(\$1),S); deffunc H4( Element of (Net-Str (a,b))) -> Element of the carrier of S = "/\" (H2(\$1),S); deffunc H5( set ) -> Element of the carrier of S = a "/\" b; A16: for jj being Element of (Net-Str (a,b)) holds H3(jj) = H5(jj) proof let jj be Element of (Net-Str (a,b)); ::_thesis: H3(jj) = H5(jj) H3(jj) = H4(jj) by A1 .= a "/\" b by YELLOW_0:40 ; hence H3(jj) = H5(jj) ; ::_thesis: verum end; A17: { H3(j3) where j3 is Element of (Net-Str (a,b)) : S2[j3] } = { H5(j4) where j4 is Element of (Net-Str (a,b)) : S2[j4] } from FRAENKEL:sch_5(A16); A18: { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } c= {(a "/\" b)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } or x in {(a "/\" b)} ) assume x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } ; ::_thesis: x in {(a "/\" b)} then ex q being Element of (Net-Str (a,b)) st ( x = a "/\" b & S2[q] ) ; hence x in {(a "/\" b)} by TARSKI:def_1; ::_thesis: verum end; {(a "/\" b)} c= { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(a "/\" b)} or x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } ) assume x in {(a "/\" b)} ; ::_thesis: x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } then x = a "/\" b by TARSKI:def_1; hence x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } ; ::_thesis: verum end; then { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } = {(a "/\" b)} by A18, XBOOLE_0:def_10; hence lim_inf (Net-Str (a,b)) = a "/\" b by A17, YELLOW_0:39; ::_thesis: verum 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 let S be with_infima Poset; ::_thesis: for a, b being Element of S st a <= b holds lim_inf (Net-Str (a,b)) = a let a, b be Element of S; ::_thesis: ( a <= b implies lim_inf (Net-Str (a,b)) = a ) assume A1: a <= b ; ::_thesis: lim_inf (Net-Str (a,b)) = a reconsider a9 = a, b9 = b as Element of S ; lim_inf (Net-Str (a,b)) = a9 "/\" b9 by Th7 .= a9 by A1, YELLOW_0:25 ; hence lim_inf (Net-Str (a,b)) = a ; ::_thesis: verum 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 let S, T be with_infima Poset; ::_thesis: 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) let a, b be Element of S; ::_thesis: for f being Function of S,T holds lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b) let f be Function of S,T; ::_thesis: lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b) set N = Net-Str (a,b); set fN = f * (Net-Str (a,b)); A1: RelStr(# the carrier of (f * (Net-Str (a,b))), the InternalRel of (f * (Net-Str (a,b))) #) = RelStr(# the carrier of (Net-Str (a,b)), the InternalRel of (Net-Str (a,b)) #) by WAYBEL_9:def_8; A2: for j being Element of (f * (Net-Str (a,b))) holds { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } = {(f . a),(f . b)} proof let j be Element of (f * (Net-Str (a,b))); ::_thesis: { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } = {(f . a),(f . b)} reconsider jj = j as Element of (Net-Str (a,b)) by A1; thus { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } c= {(f . a),(f . b)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . a),(f . b)} c= { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } or x in {(f . a),(f . b)} ) assume x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } ; ::_thesis: x in {(f . a),(f . b)} then consider i1 being Element of (f * (Net-Str (a,b))) such that A3: x = (f * (Net-Str (a,b))) . i1 and i1 >= j ; reconsider I1 = i1 as Element of (Net-Str (a,b)) by A1; i1 in the carrier of (Net-Str (a,b)) by A1; then A4: i1 in dom the mapping of (Net-Str (a,b)) by FUNCT_2:def_1; (f * (Net-Str (a,b))) . i1 = (f * the mapping of (Net-Str (a,b))) . i1 by WAYBEL_9:def_8 .= f . ((Net-Str (a,b)) . I1) by A4, FUNCT_1:13 ; then ( (f * (Net-Str (a,b))) . i1 = f . a or (f * (Net-Str (a,b))) . i1 = f . b ) by Th5; hence x in {(f . a),(f . b)} by A3, TARSKI:def_2; ::_thesis: verum end; thus {(f . a),(f . b)} c= { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(f . a),(f . b)} or x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } ) assume A5: x in {(f . a),(f . b)} ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } A6: j in the carrier of (Net-Str (a,b)) by A1; reconsider J = j as Element of NAT by A1, Def3; A7: j in dom the mapping of (Net-Str (a,b)) by A6, FUNCT_2:def_1; defpred S1[ Element of NAT ] means ex k being Element of NAT st \$1 = 2 * k; percases ( x = f . a or x = f . b ) by A5, TARSKI:def_2; supposeA8: x = f . a ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } reconsider jj = j as Element of (Net-Str (a,b)) by A1; now__::_thesis:_x_in__{__((f_*_(Net-Str_(a,b)))_._i)_where_i_is_Element_of_(f_*_(Net-Str_(a,b)))_:_i_>=_j__}_ percases ( S1[J] or not S1[J] ) ; supposeA9: S1[J] ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } A10: (f * (Net-Str (a,b))) . j = (f * the mapping of (Net-Str (a,b))) . j by WAYBEL_9:def_8 .= f . ( the mapping of (Net-Str (a,b)) . j) by A7, FUNCT_1:13 .= f . (((a,b) ,...) . j) by Def3 .= f . a by A9, Def1 ; j <= j ; hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } by A8, A10; ::_thesis: verum end; supposeA11: not S1[J] ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } A12: (Net-Str (a,b)) . jj = ((a,b) ,...) . jj by Def3 .= b by A11, Def1 ; reconsider k = J + 1 as Element of (f * (Net-Str (a,b))) by A1, Def3; reconsider kk = k as Element of (Net-Str (a,b)) by A1; kk in the carrier of (Net-Str (a,b)) ; then A13: kk in dom the mapping of (Net-Str (a,b)) by FUNCT_2:def_1; A14: (f * (Net-Str (a,b))) . k = (f * the mapping of (Net-Str (a,b))) . k by WAYBEL_9:def_8 .= f . ((Net-Str (a,b)) . kk) by A13, FUNCT_1:13 .= f . a by A12, Th6 ; J + 1 >= J by NAT_1:11; then kk >= jj by Def3; then [jj,kk] in the InternalRel of (Net-Str (a,b)) by ORDERS_2:def_5; then k >= j by A1, ORDERS_2:def_5; hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } by A8, A14; ::_thesis: verum end; end; end; hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } ; ::_thesis: verum end; supposeA15: x = f . b ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } now__::_thesis:_x_in__{__((f_*_(Net-Str_(a,b)))_._i)_where_i_is_Element_of_(f_*_(Net-Str_(a,b)))_:_i_>=_j__}_ percases ( not S1[J] or S1[J] ) ; supposeA16: not S1[J] ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } A17: (f * (Net-Str (a,b))) . j = (f * the mapping of (Net-Str (a,b))) . j by WAYBEL_9:def_8 .= f . ( the mapping of (Net-Str (a,b)) . j) by A7, FUNCT_1:13 .= f . (((a,b) ,...) . j) by Def3 .= f . b by A16, Def1 ; j <= j ; hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } by A15, A17; ::_thesis: verum end; supposeA18: S1[J] ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } A19: (Net-Str (a,b)) . jj = ((a,b) ,...) . j by Def3 .= a by A18, Def1 ; reconsider k = J + 1 as Element of (f * (Net-Str (a,b))) by A1, Def3; reconsider kk = k as Element of (Net-Str (a,b)) by Def3; kk in the carrier of (Net-Str (a,b)) ; then A20: kk in dom the mapping of (Net-Str (a,b)) by FUNCT_2:def_1; A21: (f * (Net-Str (a,b))) . k = (f * the mapping of (Net-Str (a,b))) . k by WAYBEL_9:def_8 .= f . ((Net-Str (a,b)) . kk) by A20, FUNCT_1:13 .= f . b by A19, Th6 ; J + 1 >= J by NAT_1:11; then kk >= jj by Def3; then [jj,kk] in the InternalRel of (Net-Str (a,b)) by ORDERS_2:def_5; then k >= j by A1, ORDERS_2:def_5; hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } by A15, A21; ::_thesis: verum end; end; end; hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } ; ::_thesis: verum end; end; end; end; defpred S1[ Element of (f * (Net-Str (a,b))), Element of (f * (Net-Str (a,b)))] means \$1 >= \$2; deffunc H1( Element of (f * (Net-Str (a,b)))) -> set = { ((f * (Net-Str (a,b))) . i1) where i1 is Element of (f * (Net-Str (a,b))) : S1[i1,\$1] } ; defpred S2[ set ] means verum; deffunc H2( Element of (f * (Net-Str (a,b)))) -> Element of K32( the carrier of T) = {(f . a),(f . b)}; deffunc H3( Element of (f * (Net-Str (a,b)))) -> Element of the carrier of T = "/\" (H1(\$1),T); deffunc H4( Element of (f * (Net-Str (a,b)))) -> Element of the carrier of T = "/\" (H2(\$1),T); deffunc H5( set ) -> Element of the carrier of T = (f . a) "/\" (f . b); A22: for jj being Element of (f * (Net-Str (a,b))) holds H3(jj) = H5(jj) proof let jj be Element of (f * (Net-Str (a,b))); ::_thesis: H3(jj) = H5(jj) H3(jj) = H4(jj) by A2 .= (f . a) "/\" (f . b) by YELLOW_0:40 ; hence H3(jj) = H5(jj) ; ::_thesis: verum end; A23: { H3(j3) where j3 is Element of (f * (Net-Str (a,b))) : S2[j3] } = { H5(j4) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } from FRAENKEL:sch_5(A22); A24: { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } c= {((f . a) "/\" (f . b))} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } or x in {((f . a) "/\" (f . b))} ) assume x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } ; ::_thesis: x in {((f . a) "/\" (f . b))} then ex q being Element of (f * (Net-Str (a,b))) st ( x = (f . a) "/\" (f . b) & S2[q] ) ; hence x in {((f . a) "/\" (f . b))} by TARSKI:def_1; ::_thesis: verum end; {((f . a) "/\" (f . b))} c= { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {((f . a) "/\" (f . b))} or x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } ) assume x in {((f . a) "/\" (f . b))} ; ::_thesis: x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } then x = (f . a) "/\" (f . b) by TARSKI:def_1; hence x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } ; ::_thesis: verum end; then { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } = {((f . a) "/\" (f . b))} by A24, XBOOLE_0:def_10; hence lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b) by A23, YELLOW_0:39; ::_thesis: verum 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 let S be non empty reflexive RelStr ; ::_thesis: for D being non empty Subset of S holds Net-Str D = Net-Str (D,((id the carrier of S) | D)) let D be non empty Subset of S; ::_thesis: Net-Str D = Net-Str (D,((id the carrier of S) | D)) set M = Net-Str (D,((id the carrier of S) | D)); A1: D = the carrier of (Net-Str (D,((id the carrier of S) | D))) by WAYBEL11:def_10; A2: (id the carrier of S) | D = the mapping of (Net-Str (D,((id the carrier of S) | D))) by WAYBEL11:def_10; A3: (id the carrier of S) | D = id D by FUNCT_3:1; A4: the InternalRel of S |_2 D c= the InternalRel of S by XBOOLE_1:17; now__::_thesis:_for_x,_y_being_set_holds_ (_(_[x,y]_in_the_InternalRel_of_S_|_2_D_implies_[x,y]_in_the_InternalRel_of_(Net-Str_(D,((id_the_carrier_of_S)_|_D)))_)_&_(_[x,y]_in_the_InternalRel_of_(Net-Str_(D,((id_the_carrier_of_S)_|_D)))_implies_[x,y]_in_the_InternalRel_of_S_|_2_D_)_) let x, y be set ; ::_thesis: ( ( [x,y] in the InternalRel of S |_2 D implies [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) ) & ( [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) implies [x,y] in the InternalRel of S |_2 D ) ) hereby ::_thesis: ( [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) implies [x,y] in the InternalRel of S |_2 D ) assume A5: [x,y] in the InternalRel of S |_2 D ; ::_thesis: [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) then A6: x in D by ZFMISC_1:87; A7: y in D by A5, ZFMISC_1:87; reconsider x9 = x, y9 = y as Element of (Net-Str (D,((id the carrier of S) | D))) by A1, A5, ZFMISC_1:87; A8: x9 = ((id the carrier of S) | D) . x9 by A3, A6, FUNCT_1:18; y9 = ((id the carrier of S) | D) . y9 by A3, A7, FUNCT_1:18; then (Net-Str (D,((id the carrier of S) | D))) . x9 <= (Net-Str (D,((id the carrier of S) | D))) . y9 by A2, A4, A5, A8, ORDERS_2:def_5; then x9 <= y9 by WAYBEL11:def_10; hence [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) by ORDERS_2:def_5; ::_thesis: verum end; assume A9: [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) ; ::_thesis: [x,y] in the InternalRel of S |_2 D then reconsider x9 = x, y9 = y as Element of (Net-Str (D,((id the carrier of S) | D))) by ZFMISC_1:87; x9 <= y9 by A9, ORDERS_2:def_5; then (Net-Str (D,((id the carrier of S) | D))) . x9 <= (Net-Str (D,((id the carrier of S) | D))) . y9 by WAYBEL11:def_10; then A10: [((Net-Str (D,((id the carrier of S) | D))) . x9),((Net-Str (D,((id the carrier of S) | D))) . y9)] in the InternalRel of S by ORDERS_2:def_5; A11: x9 = ((id the carrier of S) | D) . x9 by A1, A3, FUNCT_1:18; y9 = ((id the carrier of S) | D) . y9 by A1, A3, FUNCT_1:18; hence [x,y] in the InternalRel of S |_2 D by A1, A2, A9, A10, A11, XBOOLE_0:def_4; ::_thesis: verum end; hence Net-Str D = Net-Str (D,((id the carrier of S) | D)) by A1, A2, RELAT_1:def_2; ::_thesis: verum 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 Net-Str D = Net-Str (D,((id the carrier of S) | D)) by Th9; hence ( not Net-Str D is empty & Net-Str D is directed & Net-Str D is reflexive ) ; ::_thesis: verum 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 Net-Str D = Net-Str (D,((id the carrier of S) | D)) by Th9; hence Net-Str D is monotone ; ::_thesis: verum end; end; Lm6: for R being up-complete LATTICE for N being reflexive monotone net of R holds lim_inf N = sup N proof let R be up-complete LATTICE; ::_thesis: for N being reflexive monotone net of R holds lim_inf N = sup N let N be reflexive monotone net of R; ::_thesis: lim_inf N = sup N defpred S1[ set ] means verum; deffunc H1( Element of N) -> Element of the carrier of R = N . \$1; deffunc H2( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= \$1 } ,R); A1: for j being Element of N holds H1(j) = H2(j) proof let j be Element of N; ::_thesis: H1(j) = H2(j) set Y = { (N . i) where i is Element of N : i >= j } ; A2: N . j is_<=_than { (N . i) where i is Element of N : i >= j } proof let y be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not y in { (N . i) where i is Element of N : i >= j } or N . j <= y ) assume y in { (N . i) where i is Element of N : i >= j } ; ::_thesis: N . j <= y then ex i being Element of N st ( y = N . i & j <= i ) ; hence N . j <= y by WAYBEL11:def_9; ::_thesis: verum end; for b being Element of R st b is_<=_than { (N . i) where i is Element of N : i >= j } holds N . j >= b proof let b be Element of R; ::_thesis: ( b is_<=_than { (N . i) where i is Element of N : i >= j } implies N . j >= b ) assume A3: b is_<=_than { (N . i) where i is Element of N : i >= j } ; ::_thesis: N . j >= b reconsider j9 = j as Element of N ; j9 <= j9 ; then N . j9 in { (N . i) where i is Element of N : i >= j } ; hence N . j >= b by A3, LATTICE3:def_8; ::_thesis: verum end; hence H1(j) = H2(j) by A2, YELLOW_0:31; ::_thesis: verum end; rng the mapping of N = { H1(j) where j is Element of N : S1[j] } by WAYBEL11:19 .= { H2(j) where j is Element of N : S1[j] } from FRAENKEL:sch_5(A1) ; hence lim_inf N = Sup by YELLOW_2:def_5 .= sup N by WAYBEL_2:def_1 ; ::_thesis: verum 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 let S be up-complete LATTICE; ::_thesis: for D being non empty directed Subset of S holds lim_inf (Net-Str D) = sup D let D be non empty directed Subset of S; ::_thesis: lim_inf (Net-Str D) = sup D set F = (id the carrier of S) | D; A1: (id the carrier of S) | D = id D by FUNCT_3:1; lim_inf (Net-Str D) = sup (Net-Str D) by Lm6 .= Sup by WAYBEL_2:def_1 .= "\/" ((rng ((id the carrier of S) | D)),S) by YELLOW_2:def_5 .= sup D by A1, RELAT_1:45 ; hence lim_inf (Net-Str D) = sup D ; ::_thesis: verum end; 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 proof let S, T be LATTICE; ::_thesis: 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 let f be Function of S,T; ::_thesis: ( ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) implies f is monotone ) assume A1: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ; ::_thesis: f is monotone now__::_thesis:_for_a,_b_being_Element_of_S_st_a_<=_b_holds_ f_._a_<=_f_._b let a, b be Element of S; ::_thesis: ( a <= b implies f . a <= f . b ) assume A2: a <= b ; ::_thesis: f . a <= f . b set N = Net-Str (a,b); A3: f . (lim_inf (Net-Str (a,b))) = f . a by A2, Lm5; lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b) by Th8; then A4: f . a <= (f . a) "/\" (f . b) by A1, A3; f . a >= (f . a) "/\" (f . b) by YELLOW_0:23; then f . a = (f . a) "/\" (f . b) by A4, ORDERS_2:2; hence f . a <= f . b by YELLOW_0:25; ::_thesis: verum end; hence f is monotone by WAYBEL_1:def_2; ::_thesis: verum end; 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() proof set f = F5(); thus F5() .: { F4(x) where x is Element of F1() : P1[x] } c= { (F5() . F4(x)) where x is Element of F2() : P1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { (F5() . F4(x)) where x is Element of F2() : P1[x] } c= F5() .: { F4(x) where x is Element of F1() : P1[x] } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F5() .: { F4(x) where x is Element of F1() : P1[x] } or y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } ) assume y in F5() .: { F4(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } then consider z being set such that z in dom F5() and A3: z in { F4(x) where x is Element of F1() : P1[x] } and A4: y = F5() . z by FUNCT_1:def_6; consider x being Element of F1() such that A5: z = F4(x) and A6: P1[x] by A3; reconsider x = x as Element of F2() by A2; y = F5() . F4(x) by A4, A5; hence y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } by A6; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } or y in F5() .: { F4(x) where x is Element of F1() : P1[x] } ) assume y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } ; ::_thesis: y in F5() .: { F4(x) where x is Element of F1() : P1[x] } then consider x being Element of F2() such that A7: y = F5() . F4(x) and A8: P1[x] ; reconsider x = x as Element of F1() by A2; A9: F4(x) in the carrier of F3() ; F4(x) in { F4(z) where z is Element of F1() : P1[z] } by A8; hence y in F5() .: { F4(x) where x is Element of F1() : P1[x] } by A1, A7, A9, FUNCT_1:def_6; ::_thesis: verum 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 let S, T be lower-bounded continuous LATTICE; ::_thesis: 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) let f be Function of S,T; ::_thesis: ( f is directed-sups-preserving implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) assume A1: f is directed-sups-preserving ; ::_thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) let x be Element of S; ::_thesis: f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) defpred S1[ Element of S] means \$1 << x; deffunc H1( Element of S) -> Element of S = \$1; A2: f preserves_sup_of waybelow x by A1, WAYBEL_0:def_37; A3: ex_sup_of waybelow x,S by YELLOW_0:17; A4: the carrier of S c= dom f by FUNCT_2:def_1; A5: f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL17:sch_2(A4); f . x = f . (sup (waybelow x)) by WAYBEL_3:def_5 .= "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A2, A3, A5, WAYBEL_0:def_31 ; hence f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: verum 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 let S be LATTICE; ::_thesis: 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 let T be lower-bounded up-complete LATTICE; ::_thesis: 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 let f be Function of S,T; ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies f is monotone ) assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: f is monotone let X, Y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not X <= Y or f . X <= f . Y ) deffunc H1( Element of S) -> Element of S = \$1; defpred S1[ Element of S] means \$1 << X; defpred S2[ Element of S] means \$1 << Y; assume X <= Y ; ::_thesis: f . X <= f . Y then A2: waybelow X c= waybelow Y by WAYBEL_3:12; A3: f . X = "\/" ( { (f . w) where w is Element of S : w << X } ,T) by A1; A4: the carrier of S c= dom f by FUNCT_2:def_1; A5: f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL17:sch_2(A4); f .: { H1(w) where w is Element of S : S2[w] } = { (f . H1(w)) where w is Element of S : S2[w] } from WAYBEL17:sch_2(A4); then A6: f . Y = "\/" ((f .: (waybelow Y)),T) by A1; A7: ex_sup_of f .: (waybelow X),T by YELLOW_0:17; ex_sup_of f .: (waybelow Y),T by YELLOW_0:17; hence f . X <= f . Y by A2, A3, A5, A6, A7, RELAT_1:123, YELLOW_0:34; ::_thesis: verum 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 let S be lower-bounded up-complete LATTICE; ::_thesis: 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 ) ) let T be lower-bounded continuous LATTICE; ::_thesis: 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 ) ) let f be Function of S,T; ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies 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 ) ) ) assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: 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 ) ) then A2: f is monotone by Th13; let x be Element of S; ::_thesis: for y being Element of T holds ( y << f . x iff ex w being Element of S st ( w << x & y << f . w ) ) let y be Element of T; ::_thesis: ( y << f . x iff ex w being Element of S st ( w << x & y << f . w ) ) hereby ::_thesis: ( ex w being Element of S st ( w << x & y << f . w ) implies y << f . x ) assume A3: y << f . x ; ::_thesis: ex v being Element of S st ( v << x & y << f . v ) reconsider D = f .: (waybelow x) as non empty directed Subset of T by A1, Th13, YELLOW_2:15; A4: f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A1; A5: the carrier of S c= dom f by FUNCT_2:def_1; defpred S1[ Element of S] means \$1 << x; deffunc H1( Element of S) -> Element of S = \$1; f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL17:sch_2(A5); then consider w being Element of T such that A6: w in D and A7: y << w by A3, A4, WAYBEL_4:53; consider v being set such that A8: v in the carrier of S and A9: v in waybelow x and A10: w = f . v by A6, FUNCT_2:64; reconsider v = v as Element of S by A8; take v = v; ::_thesis: ( v << x & y << f . v ) thus ( v << x & y << f . v ) by A7, A9, A10, WAYBEL_3:7; ::_thesis: verum end; given w being Element of S such that A11: w << x and A12: y << f . w ; ::_thesis: y << f . x w <= x by A11, WAYBEL_3:1; then f . w <= f . x by A2, WAYBEL_1:def_2; hence y << f . x by A12, WAYBEL_3:2; ::_thesis: verum 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 let S, T be non empty RelStr ; ::_thesis: 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) let D be Subset of S; ::_thesis: 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) let f be Function of S,T; ::_thesis: ( ( ( 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 implies sup (f .: D) <= f . (sup D) ) assume A1: ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) ; ::_thesis: ( not f is monotone or sup (f .: D) <= f . (sup D) ) A2: ex_sup_of D,S by A1, YELLOW_0:17; A3: ex_sup_of f .: D,T by A1, YELLOW_0:17; assume A4: f is monotone ; ::_thesis: sup (f .: D) <= f . (sup D) D is_<=_than sup D by A2, YELLOW_0:def_9; then f .: D is_<=_than f . (sup D) by A4, YELLOW_2:14; hence sup (f .: D) <= f . (sup D) by A3, YELLOW_0:def_9; ::_thesis: verum 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 let S, T be non empty reflexive antisymmetric RelStr ; ::_thesis: 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) let D be non empty directed Subset of S; ::_thesis: 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) let f be Function of S,T; ::_thesis: ( ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) & f is monotone implies sup (f .: D) <= f . (sup D) ) assume A1: ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) ; ::_thesis: ( not f is monotone or sup (f .: D) <= f . (sup D) ) assume A2: f is monotone ; ::_thesis: sup (f .: D) <= f . (sup D) then reconsider fD = f .: D as non empty directed Subset of T by YELLOW_2:15; A3: ex_sup_of fD,T by A1, WAYBEL_0:75; ex_sup_of D,S by A1, WAYBEL_0:75; then D is_<=_than sup D by YELLOW_0:30; then f .: D is_<=_than f . (sup D) by A2, YELLOW_2:14; hence sup (f .: D) <= f . (sup D) by A3, YELLOW_0:30; ::_thesis: verum 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 let S, T be non empty RelStr ; ::_thesis: 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) let D be Subset of S; ::_thesis: 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) let f be Function of S,T; ::_thesis: ( ( ( 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 implies f . (inf D) <= inf (f .: D) ) assume A1: ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) ; ::_thesis: ( not f is monotone or f . (inf D) <= inf (f .: D) ) A2: ex_inf_of D,S by A1, YELLOW_0:17; A3: ex_inf_of f .: D,T by A1, YELLOW_0:17; assume A4: f is monotone ; ::_thesis: f . (inf D) <= inf (f .: D) inf D is_<=_than D by A2, YELLOW_0:def_10; then f . (inf D) is_<=_than f .: D by A4, YELLOW_2:13; hence f . (inf D) <= inf (f .: D) by A3, YELLOW_0:def_10; ::_thesis: verum 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 let S, T be complete LATTICE; ::_thesis: for D being Subset of S for f being Function of S,T st f is monotone holds f . ("/\" (D,S)) <= inf (f .: D) let D be Subset of S; ::_thesis: for f being Function of S,T st f is monotone holds f . ("/\" (D,S)) <= inf (f .: D) let f be Function of S,T; ::_thesis: ( f is monotone implies f . ("/\" (D,S)) <= inf (f .: D) ) reconsider D9 = D as Subset of S ; set infD = "/\" (D,S); assume A1: f is monotone ; ::_thesis: f . ("/\" (D,S)) <= inf (f .: D) "/\" (D,S) is_<=_than D by YELLOW_0:33; then f . ("/\" (D,S)) is_<=_than f .: D9 by A1, YELLOW_2:13; hence f . ("/\" (D,S)) <= inf (f .: D) by YELLOW_0:33; ::_thesis: verum 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 let S, T be up-complete LATTICE; ::_thesis: 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 let f be Function of S,T; ::_thesis: for N being non empty monotone NetStr over S st f is monotone holds f * N is monotone let N be non empty monotone NetStr over S; ::_thesis: ( f is monotone implies f * N is monotone ) assume A1: f is monotone ; ::_thesis: f * N is monotone A2: netmap (N,S) is monotone by WAYBEL_0:def_9; A3: netmap ((f * N),T) = f * (netmap (N,S)) by WAYBEL_9:def_8; set g = netmap ((f * N),T); now__::_thesis:_for_x,_y_being_Element_of_(f_*_N)_st_x_<=_y_holds_ (netmap_((f_*_N),T))_._x_<=_(netmap_((f_*_N),T))_._y let x, y be Element of (f * N); ::_thesis: ( x <= y implies (netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y ) assume A4: x <= y ; ::_thesis: (netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y A5: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by WAYBEL_9:def_8; then reconsider x9 = x, y9 = y as Element of N ; A6: dom (netmap (N,S)) = the carrier of (f * N) by A5, FUNCT_2:def_1; then A7: (netmap ((f * N),T)) . x = f . ((netmap (N,S)) . x) by A3, FUNCT_1:13; A8: (netmap ((f * N),T)) . y = f . ((netmap (N,S)) . y) by A3, A6, FUNCT_1:13; [x,y] in the InternalRel of (f * N) by A4, ORDERS_2:def_5; then x9 <= y9 by A5, ORDERS_2:def_5; then (netmap (N,S)) . x9 <= (netmap (N,S)) . y9 by A2, WAYBEL_1:def_2; hence (netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y by A1, A7, A8, WAYBEL_1:def_2; ::_thesis: verum end; then netmap ((f * N),T) is monotone by WAYBEL_1:def_2; hence f * N is monotone by WAYBEL_0:def_9; ::_thesis: verum 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; 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) proof let S, T be up-complete LATTICE; ::_thesis: 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) let f be Function of S,T; ::_thesis: ( ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) implies for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D) ) assume A1: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ; ::_thesis: for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D) let D be non empty directed Subset of S; ::_thesis: sup (f .: D) = f . (sup D) A2: f is monotone by A1, Th11; then A3: sup (f .: D) <= f . (sup D) by Th16; f . (sup D) <= sup (f .: D) proof sup D = lim_inf (Net-Str D) by Th10; then A4: f . (sup D) <= lim_inf (f * (Net-Str D)) by A1; reconsider fN = f * (Net-Str D) as reflexive monotone net of T by A2; A5: sup fN = Sup by WAYBEL_2:def_1 .= Sup by WAYBEL_9:def_8 .= sup (rng (f * ((id the carrier of S) | D))) by YELLOW_2:def_5 ; rng (f * ((id the carrier of S) | D)) = rng (f * (id D)) by FUNCT_3:1 .= rng (f | D) by RELAT_1:65 .= f .: D by RELAT_1:115 ; hence f . (sup D) <= sup (f .: D) by A4, A5, Lm6; ::_thesis: verum end; hence sup (f .: D) = f . (sup D) by A3, ORDERS_2:2; ::_thesis: verum 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 let S, T be complete LATTICE; ::_thesis: 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 let f be Function of S,T; ::_thesis: ( ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) implies f is directed-sups-preserving ) assume A1: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ; ::_thesis: f is directed-sups-preserving thus f is directed-sups-preserving ::_thesis: verum proof let D be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or f preserves_sup_of D ) assume ( not D is empty & D is directed ) ; ::_thesis: f preserves_sup_of D then reconsider D = D as non empty directed Subset of S ; A2: f is monotone by A1, Th11; then A3: sup (f .: D) <= f . (sup D) by Th15; A4: f . (sup D) <= sup (f .: D) proof sup D = lim_inf (Net-Str D) by Th10; then A5: f . (sup D) <= lim_inf (f * (Net-Str D)) by A1; reconsider fN = f * (Net-Str D) as reflexive monotone net of T by A2; A6: sup fN = Sup by WAYBEL_2:def_1 .= Sup by WAYBEL_9:def_8 .= sup (rng (f * ((id the carrier of S) | D))) by YELLOW_2:def_5 ; rng (f * ((id the carrier of S) | D)) = rng (f * (id D)) by FUNCT_3:1 .= rng (f | D) by RELAT_1:65 .= f .: D by RELAT_1:115 ; hence f . (sup D) <= sup (f .: D) by A5, A6, WAYBEL11:22; ::_thesis: verum end; f preserves_sup_of D proof assume ex_sup_of D,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: D,T & "\/" ((f .: D),T) = f . ("\/" (D,S)) ) thus ( ex_sup_of f .: D,T & "\/" ((f .: D),T) = f . ("\/" (D,S)) ) by A3, A4, ORDERS_2:2, YELLOW_0:17; ::_thesis: verum end; hence f preserves_sup_of D ; ::_thesis: verum end; 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 let S, T be complete LATTICE; ::_thesis: 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) let f be Function of S,T; ::_thesis: 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) let N be net of S; ::_thesis: 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) let j be Element of N; ::_thesis: 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) let j9 be Element of (f * N); ::_thesis: ( j9 = j & f is monotone implies 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) ) assume A1: j9 = j ; ::_thesis: ( not f is monotone or 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) ) assume A2: f is monotone ; ::_thesis: 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) A3: dom f = the carrier of S by FUNCT_2:def_1; A4: RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by WAYBEL_9:def_8; A5: dom the mapping of N = the carrier of N by FUNCT_2:def_1; A6: { ((f * N) . l) where l is Element of (f * N) : l >= j9 } c= f .: { (N . l1) where l1 is Element of N : l1 >= j } proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } or s in f .: { (N . l1) where l1 is Element of N : l1 >= j } ) assume s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ; ::_thesis: s in f .: { (N . l1) where l1 is Element of N : l1 >= j } then consider x being Element of (f * N) such that A7: s = (f * N) . x and A8: x >= j9 ; reconsider x = x as Element of N by A4; [j9,x] in the InternalRel of (f * N) by A8, ORDERS_2:def_5; then A9: x >= j by A1, A4, ORDERS_2:def_5; A10: s = (f * the mapping of N) . x by A7, WAYBEL_9:def_8 .= f . (N . x) by A5, FUNCT_1:13 ; N . x in { (N . z) where z is Element of N : z >= j } by A9; hence s in f .: { (N . l1) where l1 is Element of N : l1 >= j } by A3, A10, FUNCT_1:def_6; ::_thesis: verum end; A11: f .: { (N . l1) where l1 is Element of N : l1 >= j } c= { ((f * N) . l) where l is Element of (f * N) : l >= j9 } proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in f .: { (N . l1) where l1 is Element of N : l1 >= j } or s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ) assume s in f .: { (N . l1) where l1 is Element of N : l1 >= j } ; ::_thesis: s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } then consider x being set such that x in dom f and A12: x in { (N . l1) where l1 is Element of N : l1 >= j } and A13: s = f . x by FUNCT_1:def_6; consider l2 being Element of N such that A14: x = N . l2 and A15: l2 >= j by A12; reconsider l29 = l2 as Element of (f * N) by A4; A16: s = (f * the mapping of N) . l2 by A5, A13, A14, FUNCT_1:13 .= (f * N) . l29 by WAYBEL_9:def_8 ; [j,l2] in the InternalRel of N by A15, ORDERS_2:def_5; then l29 >= j9 by A1, A4, ORDERS_2:def_5; hence s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } by A16; ::_thesis: verum end; set K = { (N . k) where k is Element of N : k >= j } ; { (N . k) where k is Element of N : k >= j } c= the carrier of S proof let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in { (N . k) where k is Element of N : k >= j } or r in the carrier of S ) assume r in { (N . k) where k is Element of N : k >= j } ; ::_thesis: r in the carrier of S then ex f being Element of N st ( r = N . f & f >= j ) ; hence r in the carrier of S ; ::_thesis: verum end; then reconsider K = { (N . k) where k is Element of N : k >= j } as Subset of S ; { ((f * N) . l) where l is Element of (f * N) : l >= j9 } = f .: K by A6, A11, XBOOLE_0:def_10; hence 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) by A2, Lm7; ::_thesis: verum 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 let S, T be complete Scott TopLattice; ::_thesis: for f being continuous Function of S,T for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) let f be continuous Function of S,T; ::_thesis: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) let N be net of S; ::_thesis: f . (lim_inf N) <= lim_inf (f * N) set x = lim_inf N; set t = lim_inf (f * N); A1: [#] T <> {} ; assume not f . (lim_inf N) <= lim_inf (f * N) ; ::_thesis: contradiction then not f . (lim_inf N) in downarrow (lim_inf (f * N)) by WAYBEL_0:17; then A2: f . (lim_inf N) in (downarrow (lim_inf (f * N))) ` by XBOOLE_0:def_5; A3: downarrow (lim_inf (f * N)) is closed by Lm3; set U1 = f " ((downarrow (lim_inf (f * N))) `); A4: f " ((downarrow (lim_inf (f * N))) `) is open by A1, A3, TOPS_2:43; set D = { ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) where j is Element of N : verum } ; now__::_thesis:_for_f_being_set_st_f_in__{__("/\"_(_{__(N_._k)_where_k_is_Element_of_N_:_k_>=_j__}__,S))_where_j_is_Element_of_N_:_verum__}__holds_ f_in_the_carrier_of_S let f be set ; ::_thesis: ( f in { ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) where j is Element of N : verum } implies f in the carrier of S ) assume f in { ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) where j is Element of N : verum } ; ::_thesis: f in the carrier of S then ex j being Element of N st f = "/\" ( { (N . k) where k is Element of N : k >= j } ,S) ; hence f in the carrier of S ; ::_thesis: verum end; then reconsider D = { ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) where j is Element of N : verum } as Subset of S by TARSKI:def_3; reconsider D = D as non empty directed Subset of S by WAYBEL11:30; A5: lim_inf N in f " ((downarrow (lim_inf (f * N))) `) by A2, FUNCT_2:38; f " ((downarrow (lim_inf (f * N))) `) is property(S) by A4, WAYBEL11:15; then consider y being Element of S such that A6: y in D and A7: for x being Element of S st x in D & x >= y holds x in f " ((downarrow (lim_inf (f * N))) `) by A5, WAYBEL11:def_3; consider j being Element of N such that A8: y = "/\" ( { (N . k) where k is Element of N : k >= j } ,S) by A6; y <= y ; then A9: y in f " ((downarrow (lim_inf (f * N))) `) by A6, A7; RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by WAYBEL_9:def_8; then reconsider j9 = j as Element of (f * N) ; A10: dom f = the carrier of S by FUNCT_2:def_1; set fy = "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j9 } ,T); set fD = { ("/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T)) where j1 is Element of (f * N) : verum } ; now__::_thesis:_for_g_being_set_st_g_in__{__("/\"_(_{__((f_*_N)_._k)_where_k_is_Element_of_(f_*_N)_:_k_>=_j1__}__,T))_where_j1_is_Element_of_(f_*_N)_:_verum__}__holds_ g_in_the_carrier_of_T let g be set ; ::_thesis: ( g in { ("/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T)) where j1 is Element of (f * N) : verum } implies g in the carrier of T ) assume g in { ("/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T)) where j1 is Element of (f * N) : verum } ; ::_thesis: g in the carrier of T then ex j being Element of (f * N) st g = "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j } ,T) ; hence g in the carrier of T ; ::_thesis: verum end; then reconsider fD = { ("/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T)) where j1 is Element of (f * N) : verum } as Subset of T by TARSKI:def_3; A11: f . y <= "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j9 } ,T) by A8, Th20; "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j9 } ,T) in fD ; then "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j9 } ,T) <= sup fD by YELLOW_2:22; then f . y <= lim_inf (f * N) by A11, ORDERS_2:3; then f . y in downarrow (lim_inf (f * N)) by WAYBEL_0:17; then A12: y in f " (downarrow (lim_inf (f * N))) by A10, FUNCT_1:def_7; f " ((downarrow (lim_inf (f * N))) `) = (f " ([#] T)) \ (f " (downarrow (lim_inf (f * N)))) by FUNCT_1:69 .= ([#] S) \ (f " (downarrow (lim_inf (f * N)))) by TOPS_2:41 .= (f " (downarrow (lim_inf (f * N)))) ` ; then A13: y in (f " ((downarrow (lim_inf (f * N))) `)) /\ ((f " ((downarrow (lim_inf (f * N))) `)) `) by A9, A12, XBOOLE_0:def_4; f " ((downarrow (lim_inf (f * N))) `) misses (f " ((downarrow (lim_inf (f * N))) `)) ` by XBOOLE_1:79; hence contradiction by A13, XBOOLE_0:4; ::_thesis: verum 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 let L be continuous Scott TopLattice; ::_thesis: 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 ) let p be Element of L; ::_thesis: 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 ) let S be Subset of L; ::_thesis: ( S is open & p in S implies ex q being Element of L st ( q << p & q in S ) ) assume that A1: S is open and A2: p in S ; ::_thesis: ex q being Element of L st ( q << p & q in S ) A3: S is inaccessible by A1, WAYBEL11:def_4; sup (waybelow p) = p by WAYBEL_3:def_5; then waybelow p meets S by A2, A3, WAYBEL11:def_1; then (waybelow p) /\ S <> {} by XBOOLE_0:def_7; then consider u being set such that A4: u in (waybelow p) /\ S by XBOOLE_0:def_1; A5: u in waybelow p by A4, XBOOLE_0:def_4; reconsider u = u as Element of L by A4; take u ; ::_thesis: ( u << p & u in S ) thus u << p by A5, WAYBEL_3:7; ::_thesis: u in S thus u in S by A4, XBOOLE_0:def_4; ::_thesis: verum end; Lm11: for L being lower-bounded continuous Scott TopLattice for x being Element of L holds wayabove x is open proof let L be lower-bounded continuous Scott TopLattice; ::_thesis: for x being Element of L holds wayabove x is open let x be Element of L; ::_thesis: wayabove x is open set W = wayabove x; wayabove x is inaccessible proof let D be non empty directed Subset of L; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,L) in wayabove x or not D misses wayabove x ) assume sup D in wayabove x ; ::_thesis: not D misses wayabove x then x << sup D by WAYBEL_3:8; then consider d being Element of L such that A1: d in D and A2: x << d by WAYBEL_4:53; d in wayabove x by A2; hence not D misses wayabove x by A1, XBOOLE_0:3; ::_thesis: verum end; hence wayabove x is open by WAYBEL11:def_4; ::_thesis: verum 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 let L be lower-bounded continuous Scott TopLattice; ::_thesis: for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of let p be Element of L; ::_thesis: { (wayabove q) where q is Element of L : q << p } is Basis of set X = { (wayabove q) where q is Element of L : q << p } ; { (wayabove q) where q is Element of L : q << p } c= bool the carrier of L proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (wayabove q) where q is Element of L : q << p } or e in bool the carrier of L ) assume e in { (wayabove q) where q is Element of L : q << p } ; ::_thesis: e in bool the carrier of L then ex q being Element of L st ( e = wayabove q & q << p ) ; hence e in bool the carrier of L ; ::_thesis: verum end; then reconsider X = { (wayabove q) where q is Element of L : q << p } as Subset-Family of L ; X is Basis of proof A1: X is open proof let e be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not e in X or e is open ) assume e in X ; ::_thesis: e is open then consider q being Element of L such that A2: e = wayabove q and q << p ; wayabove q is open by Lm11; hence e is open by A2; ::_thesis: verum end; X is p -quasi_basis proof for Y being set st Y in X holds p in Y proof let e be set ; ::_thesis: ( e in X implies p in e ) assume e in X ; ::_thesis: p in e then ex q being Element of L st ( e = wayabove q & q << p ) ; hence p in e ; ::_thesis: verum end; hence p in Intersect X by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of K32( the carrier of L) holds ( not b1 is open or not p in b1 or ex b2 being Element of K32( the carrier of L) st ( b2 in X & b2 c= b1 ) ) let S be Subset of L; ::_thesis: ( not S is open or not p in S or ex b1 being Element of K32( the carrier of L) st ( b1 in X & b1 c= S ) ) assume that A3: S is open and A4: p in S ; ::_thesis: ex b1 being Element of K32( the carrier of L) st ( b1 in X & b1 c= S ) consider u being Element of L such that A5: u << p and A6: u in S by A3, A4, Lm10; take V = wayabove u; ::_thesis: ( V in X & V c= S ) thus V in X by A5; ::_thesis: V c= S A7: S is upper by A3, WAYBEL11:def_4; A8: wayabove u c= uparrow u by WAYBEL_3:11; uparrow u c= S by A6, A7, WAYBEL11:42; hence V c= S by A8, XBOOLE_1:1; ::_thesis: verum end; hence X is Basis of by A1; ::_thesis: verum end; hence { (wayabove q) where q is Element of L : q << p } is Basis of ; ::_thesis: verum 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 let T be lower-bounded continuous Scott TopLattice; ::_thesis: { (wayabove x) where x is Element of T : verum } is Basis of T set B = { (wayabove x) where x is Element of T : verum } ; A1: { (wayabove x) where x is Element of T : verum } c= the topology of T proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (wayabove x) where x is Element of T : verum } or e in the topology of T ) assume e in { (wayabove x) where x is Element of T : verum } ; ::_thesis: e in the topology of T then consider x being Element of T such that A2: e = wayabove x ; wayabove x is open by Lm11; hence e in the topology of T by A2, PRE_TOPC:def_2; ::_thesis: verum end; then reconsider P = { (wayabove x) where x is Element of T : verum } as Subset-Family of T by XBOOLE_1:1; for x being Point of T ex B being Basis of st B c= P proof let x be Point of T; ::_thesis: ex B being Basis of st B c= P reconsider p = x as Element of T ; reconsider A = { (wayabove q) where q is Element of T : q << p } as Basis of by Lm12; take A ; ::_thesis: A c= P let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in A or u in P ) assume u in A ; ::_thesis: u in P then ex q being Element of T st ( u = wayabove q & q << p ) ; hence u in P ; ::_thesis: verum end; hence { (wayabove x) where x is Element of T : verum } is Basis of T by A1, YELLOW_8:14; ::_thesis: verum 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 let T be lower-bounded continuous Scott TopLattice; ::_thesis: for S being Subset of T holds Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } let S be Subset of T; ::_thesis: Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } set B = { (wayabove x) where x is Element of T : verum } ; set I = { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ; set P = { (wayabove x) where x is Element of T : wayabove x c= S } ; A1: { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } = { (wayabove x) where x is Element of T : wayabove x c= S } proof thus { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } c= { (wayabove x) where x is Element of T : wayabove x c= S } :: according to XBOOLE_0:def_10 ::_thesis: { (wayabove x) where x is Element of T : wayabove x c= S } c= { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } or e in { (wayabove x) where x is Element of T : wayabove x c= S } ) assume e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ; ::_thesis: e in { (wayabove x) where x is Element of T : wayabove x c= S } then consider G being Subset of T such that A2: e = G and A3: G in { (wayabove x) where x is Element of T : verum } and A4: G c= S ; ex x being Element of T st G = wayabove x by A3; hence e in { (wayabove x) where x is Element of T : wayabove x c= S } by A2, A4; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (wayabove x) where x is Element of T : wayabove x c= S } or e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ) assume e in { (wayabove x) where x is Element of T : wayabove x c= S } ; ::_thesis: e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } then consider x being Element of T such that A5: e = wayabove x and A6: wayabove x c= S ; wayabove x in { (wayabove x) where x is Element of T : verum } ; hence e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } by A5, A6; ::_thesis: verum end; { (wayabove x) where x is Element of T : verum } is Basis of T by Lm13; hence Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } by A1, YELLOW_8:11; ::_thesis: verum 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 let S, T be lower-bounded continuous Scott TopLattice; ::_thesis: 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 let f be Function of S,T; ::_thesis: ( ( 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 ) ) ) implies f is continuous ) assume A1: 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 ) ) ; ::_thesis: f is continuous A2: [#] T <> {} ; now__::_thesis:_for_U1_being_Subset_of_T_st_U1_is_open_holds_ f_"_U1_is_open let U1 be Subset of T; ::_thesis: ( U1 is open implies f " U1 is open ) assume A3: U1 is open ; ::_thesis: f " U1 is open set U19 = U1; A4: U1 is upper by A3, WAYBEL11:def_4; reconsider fU = f " U1 as Subset of S ; A5: Int fU c= fU by TOPS_1:16; fU c= Int fU proof let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in fU or xx in Int fU ) assume A6: xx in fU ; ::_thesis: xx in Int fU then reconsider x = xx as Element of S ; A7: f . x in U1 by A6, FUNCT_1:def_7; reconsider p = f . x as Element of T ; consider u being Element of T such that A8: u << p and A9: u in U1 by A3, A7, Lm10; consider w being Element of S such that A10: w << x and A11: u << f . w by A1, A8; f .: (wayabove w) c= U1 proof let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in f .: (wayabove w) or h in U1 ) assume h in f .: (wayabove w) ; ::_thesis: h in U1 then consider z being set such that A12: z in dom f and A13: z in wayabove w and A14: h = f . z by FUNCT_1:def_6; reconsider z = z as Element of S by A12; w << z by A13, WAYBEL_3:8; then u << f . z by A1, A11; then u <= f . z by WAYBEL_3:1; hence h in U1 by A4, A9, A14, WAYBEL_0:def_20; ::_thesis: verum end; then A15: f " (f .: (wayabove w)) c= f " U1 by RELAT_1:143; wayabove w c= f " (f .: (wayabove w)) by FUNCT_2:42; then A16: wayabove w c= f " U1 by A15, XBOOLE_1:1; A17: Int fU = union { (wayabove g) where g is Element of S : wayabove g c= fU } by Lm14; A18: x in wayabove w by A10; wayabove w in { (wayabove g) where g is Element of S : wayabove g c= fU } by A16; hence xx in Int fU by A17, A18, TARSKI:def_4; ::_thesis: verum end; hence f " U1 is open by A5, XBOOLE_0:def_10; ::_thesis: verum end; hence f is continuous by A2, TOPS_2:43; ::_thesis: verum end; begin 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; 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 let S, T be complete Scott TopLattice; ::_thesis: for f being Function of S,T holds ( f is continuous iff f is directed-sups-preserving ) let f be Function of S,T; ::_thesis: ( f is continuous iff f is directed-sups-preserving ) thus ( f is continuous implies f is directed-sups-preserving ) ::_thesis: ( f is directed-sups-preserving implies f is continuous ) proof assume f is continuous ; ::_thesis: f is directed-sups-preserving then for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) by Lm9; hence f is directed-sups-preserving by Lm8; ::_thesis: verum end; thus ( f is directed-sups-preserving implies f is continuous ) by Lm4; ::_thesis: verum 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 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 proof let S, T be complete continuous Scott TopLattice; ::_thesis: 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 let f be Function of S,T; ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies f is directed-sups-preserving ) assume for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: f is directed-sups-preserving then 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 ) ) by Th14; then f is continuous by Lm15; hence f is directed-sups-preserving ; ::_thesis: verum end; 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 let S, T be complete continuous Scott TopLattice; ::_thesis: 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 ) ) ) let f be Function of S,T; ::_thesis: ( 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 ) ) ) hereby ::_thesis: ( ( 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 ) ) ) implies f is continuous ) assume f is continuous ; ::_thesis: 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 ) ) then for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by Th12; hence 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 ) ) by Th14; ::_thesis: verum end; thus ( ( 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 ) ) ) implies f is continuous ) by Lm15; ::_thesis: verum end; 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 let S, T be complete continuous Scott TopLattice; ::_thesis: 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) ) let f be Function of S,T; ::_thesis: ( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) thus ( f is continuous implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) by Th12; ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies f is continuous ) assume for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: f is continuous then f is directed-sups-preserving by Lm16; hence f is continuous ; ::_thesis: verum 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 let S, T be complete Scott TopLattice; ::_thesis: 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 ) ) let f be Function of S,T; ::_thesis: ( 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 ) ) ) implies 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 ) ) ) assume that A1: S is algebraic and A2: T is algebraic ; ::_thesis: ( ex x being Element of S ex y being Element of T st ( ( y << f . x implies ex w being Element of S st ( w << x & y << f . w ) ) implies ( ex w being Element of S st ( w << x & y << f . w ) & not y << f . x ) ) or 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 ) ) ) A3: S is continuous by A1, WAYBEL_8:7; A4: T is continuous by A2, WAYBEL_8:7; assume A5: 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 ) ) ; ::_thesis: 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 ) ) then A6: f is continuous by A3, A4, Th23; let x be Element of S; ::_thesis: 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 ) ) let k be Element of T; ::_thesis: ( k in the carrier of (CompactSublatt T) implies ( k <= f . x iff ex j being Element of S st ( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) assume A7: k in the carrier of (CompactSublatt T) ; ::_thesis: ( k <= f . x iff ex j being Element of S st ( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) hereby ::_thesis: ( ex j being Element of S st ( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) implies k <= f . x ) assume k <= f . x ; ::_thesis: ex w1 being Element of S st ( w1 in the carrier of (CompactSublatt S) & w1 <= x & k <= f . w1 ) then k << f . x by A7, WAYBEL_8:1; then consider w being Element of S such that A8: w << x and A9: k << f . w by A5; consider w1 being Element of S such that A10: w1 in the carrier of (CompactSublatt S) and A11: w <= w1 and A12: w1 <= x by A1, A8, WAYBEL_8:7; A13: k <= f . w by A9, WAYBEL_3:1; take w1 = w1; ::_thesis: ( w1 in the carrier of (CompactSublatt S) & w1 <= x & k <= f . w1 ) thus w1 in the carrier of (CompactSublatt S) by A10; ::_thesis: ( w1 <= x & k <= f . w1 ) thus w1 <= x by A12; ::_thesis: k <= f . w1 f . w <= f . w1 by A6, A11, WAYBEL_1:def_2; hence k <= f . w1 by A13, ORDERS_2:3; ::_thesis: verum end; given j being Element of S such that j in the carrier of (CompactSublatt S) and A14: j <= x and A15: k <= f . j ; ::_thesis: k <= f . x f is continuous by A3, A4, A5, Lm15; then f . j <= f . x by A14, WAYBEL_1:def_2; hence k <= f . x by A15, ORDERS_2:3; ::_thesis: verum 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 let S, T be complete Scott TopLattice; ::_thesis: 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 ) ) let f be Function of S,T; ::_thesis: ( 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 ) ) ) implies 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 ) ) ) assume A1: T is algebraic ; ::_thesis: ( ex x being Element of S ex k being Element of T st ( k in the carrier of (CompactSublatt T) & not ( k <= f . x iff ex j being Element of S st ( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) or 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 ) ) ) assume A2: 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 ) ) ; ::_thesis: 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 ) ) let x be Element of S; ::_thesis: for y being Element of T holds ( y << f . x iff ex w being Element of S st ( w << x & y << f . w ) ) let y be Element of T; ::_thesis: ( y << f . x iff ex w being Element of S st ( w << x & y << f . w ) ) hereby ::_thesis: ( ex w being Element of S st ( w << x & y << f . w ) implies y << f . x ) assume y << f . x ; ::_thesis: ex j being Element of S st ( j << x & y << f . j ) then consider w being Element of T such that A3: w in the carrier of (CompactSublatt T) and A4: y <= w and A5: w <= f . x by A1, WAYBEL_8:7; consider j being Element of S such that A6: j in the carrier of (CompactSublatt S) and A7: j <= x and A8: w <= f . j by A2, A3, A5; take j = j; ::_thesis: ( j << x & y << f . j ) thus j << x by A6, A7, WAYBEL_8:1; ::_thesis: y << f . j thus y << f . j by A3, A4, A8, WAYBEL_8:1; ::_thesis: verum end; given w being Element of S such that A9: w << x and A10: y << f . w ; ::_thesis: y << f . x consider h being Element of T such that A11: h in the carrier of (CompactSublatt T) and A12: y <= h and A13: h <= f . w by A1, A10, WAYBEL_8:7; consider j being Element of S such that A14: j in the carrier of (CompactSublatt S) and A15: j <= w and A16: h <= f . j by A2, A11, A13; j << x by A9, A15, WAYBEL_3:2; then j <= x by WAYBEL_3:1; then h <= f . x by A2, A11, A14, A16; hence y << f . x by A11, A12, WAYBEL_8:1; ::_thesis: verum 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 let S, T be complete Scott TopLattice; ::_thesis: 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) let f be Function of S,T; ::_thesis: ( 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) ) implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) assume that A1: S is algebraic and A2: T is algebraic ; ::_thesis: ( ex x being Element of S st not f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) or for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) A3: S is continuous by A1, WAYBEL_8:7; A4: T is continuous by A2, WAYBEL_8:7; assume A5: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) let x be Element of S; ::_thesis: f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) A6: the carrier of S c= dom f by FUNCT_2:def_1; defpred S1[ Element of S] means ( \$1 <= x & \$1 is compact ); deffunc H1( Element of S) -> Element of S = \$1; A7: f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL17:sch_1(A6); A8: f .: { w where w is Element of S : ( w <= x & w is compact ) } = f .: (compactbelow x) by WAYBEL_8:def_2; reconsider D = compactbelow x as non empty directed Subset of S by A1, WAYBEL_8:def_4; f is directed-sups-preserving by A3, A4, A5, Lm16; then A9: f preserves_sup_of D by WAYBEL_0:def_37; A10: ex_sup_of D,S by YELLOW_0:17; S is satisfying_axiom_K by A1, WAYBEL_8:def_4; then f . x = f . (sup D) by WAYBEL_8:def_3 .= "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) by A7, A8, A9, A10, WAYBEL_0:def_31 ; hence f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ; ::_thesis: verum 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 let S be LATTICE; ::_thesis: 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 let T be complete LATTICE; ::_thesis: 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 let f be Function of S,T; ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) implies f is monotone ) assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ; ::_thesis: f is monotone thus f is monotone ::_thesis: verum proof let X, Y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not X <= Y or f . X <= f . Y ) assume X <= Y ; ::_thesis: f . X <= f . Y then A2: compactbelow X c= compactbelow Y by WAYBEL13:1; A3: f . X = "\/" ( { (f . w) where w is Element of S : ( w <= X & w is compact ) } ,T) by A1; A4: f . Y = "\/" ( { (f . w) where w is Element of S : ( w <= Y & w is compact ) } ,T) by A1; A5: the carrier of S c= dom f by FUNCT_2:def_1; defpred S1[ Element of S] means ( \$1 <= X & \$1 is compact ); defpred S2[ Element of S] means ( \$1 <= Y & \$1 is compact ); deffunc H1( Element of S) -> Element of S = \$1; f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL17:sch_2(A5); then A6: f . X = "\/" ((f .: (compactbelow X)),T) by A3, WAYBEL_8:def_2; f .: { H1(w) where w is Element of S : S2[w] } = { (f . H1(w)) where w is Element of S : S2[w] } from WAYBEL17:sch_2(A5); then A7: f . Y = "\/" ((f .: (compactbelow Y)),T) by A4, WAYBEL_8:def_2; A8: ex_sup_of f .: (compactbelow X),T by YELLOW_0:17; ex_sup_of f .: (compactbelow Y),T by YELLOW_0:17; hence f . X <= f . Y by A2, A6, A7, A8, RELAT_1:123, YELLOW_0:34; ::_thesis: verum end; 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 let S, T be complete Scott TopLattice; ::_thesis: 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) let f be Function of S,T; ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ; ::_thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) then A2: f is monotone by Th25; let x be Element of S; ::_thesis: f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) A3: f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) by A1; set FW = { (f . w) where w is Element of S : ( w <= x & w is compact ) } ; set FX = { (f . w) where w is Element of S : w << x } ; set fx = f . x; A4: { (f . w) where w is Element of S : ( w <= x & w is compact ) } c= { (f . w) where w is Element of S : w << x } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (f . w) where w is Element of S : ( w <= x & w is compact ) } or a in { (f . w) where w is Element of S : w << x } ) assume a in { (f . w) where w is Element of S : ( w <= x & w is compact ) } ; ::_thesis: a in { (f . w) where w is Element of S : w << x } then consider w being Element of S such that A5: a = f . w and A6: w <= x and A7: w is compact ; w << w by A7, WAYBEL_3:def_2; then w << x by A6, WAYBEL_3:2; hence a in { (f . w) where w is Element of S : w << x } by A5; ::_thesis: verum end; A8: f . x is_>=_than { (f . w) where w is Element of S : w << x } proof let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in { (f . w) where w is Element of S : w << x } or b <= f . x ) assume b in { (f . w) where w is Element of S : w << x } ; ::_thesis: b <= f . x then consider ww being Element of S such that A9: b = f . ww and A10: ww << x ; ww <= x by A10, WAYBEL_3:1; hence b <= f . x by A2, A9, WAYBEL_1:def_2; ::_thesis: verum end; for b being Element of T st b is_>=_than { (f . w) where w is Element of S : w << x } holds f . x <= b proof let b be Element of T; ::_thesis: ( b is_>=_than { (f . w) where w is Element of S : w << x } implies f . x <= b ) assume b is_>=_than { (f . w) where w is Element of S : w << x } ; ::_thesis: f . x <= b then b is_>=_than { (f . w) where w is Element of S : ( w <= x & w is compact ) } by A4, YELLOW_0:9; hence f . x <= b by A3, YELLOW_0:32; ::_thesis: verum end; hence f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A8, YELLOW_0:30; ::_thesis: verum end; 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 let S, T be complete Scott TopLattice; ::_thesis: 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 ) ) ) let f be Function of S,T; ::_thesis: ( S is algebraic & T is algebraic implies ( 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 ) ) ) ) assume that A1: S is algebraic and A2: T is algebraic ; ::_thesis: ( 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 ) ) ) A3: S is continuous by A1, WAYBEL_8:7; A4: T is continuous by A2, WAYBEL_8:7; hereby ::_thesis: ( ( 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 ) ) ) implies f is continuous ) assume f is continuous ; ::_thesis: 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 ) ) then 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 ) ) by A3, A4, Th23; hence 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 ) ) by A1, A2, Lm17; ::_thesis: verum end; assume 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 ) ) ; ::_thesis: f is continuous then 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 ) ) by A2, Lm18; hence f is continuous by A3, A4, Th23; ::_thesis: verum end; 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 let S, T be complete Scott TopLattice; ::_thesis: 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) ) let f be Function of S,T; ::_thesis: ( S is algebraic & T is algebraic implies ( 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) ) ) assume that A1: S is algebraic and A2: T is algebraic ; ::_thesis: ( 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) ) A3: S is continuous by A1, WAYBEL_8:7; A4: T is continuous by A2, WAYBEL_8:7; hereby ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) implies f is continuous ) assume f is continuous ; ::_thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) then for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A3, A4, Th24; hence for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) by A1, A2, Lm19; ::_thesis: verum end; assume for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ; ::_thesis: f is continuous then for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by Th26; hence f is continuous by A3, A4, Th24; ::_thesis: verum 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;