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