let S, T be 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)
let f be continuous Function of S,T; for N being net of S holds f . (lim_inf N) <= lim_inf (f * N)
let N be net of S; 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)
; 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 } ;
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 } ;
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; verum