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

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 A1: f . (lim_inf N) in (downarrow (lim_inf (f * N))) ` by XBOOLE_0:def 5;

A2: downarrow (lim_inf (f * N)) is closed by Lm3;

set U1 = f " ((downarrow (lim_inf (f * N))) `);

A3: f " ((downarrow (lim_inf (f * N))) `) is open by A2, TOPS_2:43;

set D = { ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) where j is Element of N : verum } ;

reconsider D = D as non empty directed Subset of S by WAYBEL11:30;

A4: lim_inf N in f " ((downarrow (lim_inf (f * N))) `) by A1, FUNCT_2:38;

f " ((downarrow (lim_inf (f * N))) `) is property(S) by A3, WAYBEL11:15;

then consider y being Element of S such that

A5: y in D and

A6: for x being Element of S st x in D & x >= y holds

x in f " ((downarrow (lim_inf (f * N))) `) by A4;

consider j being Element of N such that

A7: y = "/\" ( { (N . k) where k is Element of N : k >= j } ,S) by A5;

y <= y ;

then A8: y in f " ((downarrow (lim_inf (f * N))) `) by A5, A6;

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

A9: 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 } ;

A10: f . y <= "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j9 } ,T) by A7, 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 A10, ORDERS_2:3;

then f . y in downarrow (lim_inf (f * N)) by WAYBEL_0:17;

then A11: y in f " (downarrow (lim_inf (f * N))) by A9, 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 A12: y in (f " ((downarrow (lim_inf (f * N))) `)) /\ ((f " ((downarrow (lim_inf (f * N))) `)) `) by A8, A11, XBOOLE_0:def 4;

f " ((downarrow (lim_inf (f * N))) `) misses (f " ((downarrow (lim_inf (f * N))) `)) ` by XBOOLE_1:79;

hence contradiction by A12; :: thesis: verum

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

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 A1: f . (lim_inf N) in (downarrow (lim_inf (f * N))) ` by XBOOLE_0:def 5;

A2: downarrow (lim_inf (f * N)) is closed by Lm3;

set U1 = f " ((downarrow (lim_inf (f * N))) `);

A3: f " ((downarrow (lim_inf (f * N))) `) is open by A2, 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 object 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

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;f in the carrier of S

let f be object ; :: 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;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

reconsider D = D as non empty directed Subset of S by WAYBEL11:30;

A4: lim_inf N in f " ((downarrow (lim_inf (f * N))) `) by A1, FUNCT_2:38;

f " ((downarrow (lim_inf (f * N))) `) is property(S) by A3, WAYBEL11:15;

then consider y being Element of S such that

A5: y in D and

A6: for x being Element of S st x in D & x >= y holds

x in f " ((downarrow (lim_inf (f * N))) `) by A4;

consider j being Element of N such that

A7: y = "/\" ( { (N . k) where k is Element of N : k >= j } ,S) by A5;

y <= y ;

then A8: y in f " ((downarrow (lim_inf (f * N))) `) by A5, A6;

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

A9: 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 object 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

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;g in the carrier of T

let g be object ; :: 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;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

A10: f . y <= "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j9 } ,T) by A7, 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 A10, ORDERS_2:3;

then f . y in downarrow (lim_inf (f * N)) by WAYBEL_0:17;

then A11: y in f " (downarrow (lim_inf (f * N))) by A9, 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 A12: y in (f " ((downarrow (lim_inf (f * N))) `)) /\ ((f " ((downarrow (lim_inf (f * N))) `)) `) by A8, A11, XBOOLE_0:def 4;

f " ((downarrow (lim_inf (f * N))) `) misses (f " ((downarrow (lim_inf (f * N))) `)) ` by XBOOLE_1:79;

hence contradiction by A12; :: thesis: verum