let L be continuous complete LATTICE; :: thesis: lim_inf-Convergence L is (DIVERGENCE)

let N be net of L; :: according to YELLOW_6:def 22 :: thesis: for b_{1} being Element of the carrier of L holds

( not N in NetUniv L or [N,b_{1}] in lim_inf-Convergence L or ex b_{2} being subnet of N st

( b_{2} in NetUniv L & ( for b_{3} being subnet of b_{2} holds not [b_{3},b_{1}] in lim_inf-Convergence L ) ) )

let x be Element of L; :: thesis: ( not N in NetUniv L or [N,x] in lim_inf-Convergence L or ex b_{1} being subnet of N st

( b_{1} in NetUniv L & ( for b_{2} being subnet of b_{1} holds not [b_{2},x] in lim_inf-Convergence L ) ) )

assume that

A1: N in NetUniv L and

A2: not [N,x] in lim_inf-Convergence L ; :: thesis: ex b_{1} being subnet of N st

( b_{1} in NetUniv L & ( for b_{2} being subnet of b_{1} holds not [b_{2},x] in lim_inf-Convergence L ) )

A3: ex N1 being strict net of L st

( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by A1, YELLOW_6:def 11;

not for M being subnet of N holds x = lim_inf M by A1, A2, Def3;

then A4: ( not x = lim_inf N or ex p being greater_or_equal_to_id Function of N,N st not x >= inf (N * p) ) by Th14;

A5: lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def 18;

let N be net of L; :: according to YELLOW_6:def 22 :: thesis: for b

( not N in NetUniv L or [N,b

( b

let x be Element of L; :: thesis: ( not N in NetUniv L or [N,x] in lim_inf-Convergence L or ex b

( b

assume that

A1: N in NetUniv L and

A2: not [N,x] in lim_inf-Convergence L ; :: thesis: ex b

( b

A3: ex N1 being strict net of L st

( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by A1, YELLOW_6:def 11;

not for M being subnet of N holds x = lim_inf M by A1, A2, Def3;

then A4: ( not x = lim_inf N or ex p being greater_or_equal_to_id Function of N,N st not x >= inf (N * p) ) by Th14;

A5: lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def 18;

per cases
( ( not x = lim_inf N & x <= lim_inf N ) or ( not x = lim_inf N & not x <= lim_inf N ) or ex M being subnet of N st

( M in NetUniv L & not x >= inf M ) ) by A1, A4, Th10;

end;

( M in NetUniv L & not x >= inf M ) ) by A1, A4, Th10;

suppose A6:
( not x = lim_inf N & x <= lim_inf N )
; :: thesis: ex b_{1} being subnet of N st

( b_{1} in NetUniv L & ( for b_{2} being subnet of b_{1} holds not [b_{2},x] in lim_inf-Convergence L ) )

( b

reconsider N9 = N as subnet of N by YELLOW_6:14;

take N9 ; :: thesis: ( N9 in NetUniv L & ( for b_{1} being subnet of N9 holds not [b_{1},x] in lim_inf-Convergence L ) )

thus N9 in NetUniv L by A1; :: thesis: for b_{1} being subnet of N9 holds not [b_{1},x] in lim_inf-Convergence L

given M2 being subnet of N9 such that A7: [M2,x] in lim_inf-Convergence L ; :: thesis: contradiction

A8: lim_inf N <= lim_inf M2 by WAYBEL21:37;

A9: M2 is subnet of M2 by YELLOW_6:14;

M2 in NetUniv L by A5, A7, ZFMISC_1:87;

then lim_inf M2 = x by A7, A9, Def3;

hence contradiction by A6, A8, YELLOW_0:def 3; :: thesis: verum

end;take N9 ; :: thesis: ( N9 in NetUniv L & ( for b

thus N9 in NetUniv L by A1; :: thesis: for b

given M2 being subnet of N9 such that A7: [M2,x] in lim_inf-Convergence L ; :: thesis: contradiction

A8: lim_inf N <= lim_inf M2 by WAYBEL21:37;

A9: M2 is subnet of M2 by YELLOW_6:14;

M2 in NetUniv L by A5, A7, ZFMISC_1:87;

then lim_inf M2 = x by A7, A9, Def3;

hence contradiction by A6, A8, YELLOW_0:def 3; :: thesis: verum

suppose
( not x = lim_inf N & not x <= lim_inf N )
; :: thesis: ex b_{1} being subnet of N st

( b_{1} in NetUniv L & ( for b_{2} being subnet of b_{1} holds not [b_{2},x] in lim_inf-Convergence L ) )

( b

then
not x is_S-limit_of N
;

then not [N,x] in Scott-Convergence L by A1, A3, WAYBEL11:def 8;

then consider M being subnet of N such that

A10: M in NetUniv L and

A11: for M1 being subnet of M holds not [M1,x] in Scott-Convergence L by A1, YELLOW_6:def 22;

take M ; :: thesis: ( M in NetUniv L & ( for b_{1} being subnet of M holds not [b_{1},x] in lim_inf-Convergence L ) )

thus M in NetUniv L by A10; :: thesis: for b_{1} being subnet of M holds not [b_{1},x] in lim_inf-Convergence L

for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L_{1} being subnet of M holds not [b_{1},x] in lim_inf-Convergence L
; :: thesis: verum

end;then not [N,x] in Scott-Convergence L by A1, A3, WAYBEL11:def 8;

then consider M being subnet of N such that

A10: M in NetUniv L and

A11: for M1 being subnet of M holds not [M1,x] in Scott-Convergence L by A1, YELLOW_6:def 22;

take M ; :: thesis: ( M in NetUniv L & ( for b

thus M in NetUniv L by A10; :: thesis: for b

for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L

proof

hence
for b
let M1 be subnet of M; :: thesis: not [M1,x] in lim_inf-Convergence L

A12: not [M1,x] in Scott-Convergence L by A11;

assume A13: [M1,x] in lim_inf-Convergence L ; :: thesis: contradiction

then A14: M1 in NetUniv L by A5, ZFMISC_1:87;

then ex M11 being strict net of L st

( M11 = M1 & the carrier of M11 in the_universe_of the carrier of L ) by YELLOW_6:def 11;

then A15: not x is_S-limit_of M1 by A14, A12, WAYBEL11:def 8;

M1 is subnet of M1 by YELLOW_6:14;

then x = lim_inf M1 by A13, A14, Def3;

hence contradiction by A15; :: thesis: verum

end;A12: not [M1,x] in Scott-Convergence L by A11;

assume A13: [M1,x] in lim_inf-Convergence L ; :: thesis: contradiction

then A14: M1 in NetUniv L by A5, ZFMISC_1:87;

then ex M11 being strict net of L st

( M11 = M1 & the carrier of M11 in the_universe_of the carrier of L ) by YELLOW_6:def 11;

then A15: not x is_S-limit_of M1 by A14, A12, WAYBEL11:def 8;

M1 is subnet of M1 by YELLOW_6:14;

then x = lim_inf M1 by A13, A14, Def3;

hence contradiction by A15; :: thesis: verum

suppose
ex M being subnet of N st

( M in NetUniv L & not x >= inf M ) ; :: thesis: ex b_{1} being subnet of N st

( b_{1} in NetUniv L & ( for b_{2} being subnet of b_{1} holds not [b_{2},x] in lim_inf-Convergence L ) )

( M in NetUniv L & not x >= inf M ) ; :: thesis: ex b

( b

then consider M being subnet of N such that

A16: M in NetUniv L and

A17: not x >= inf M ;

take M ; :: thesis: ( M in NetUniv L & ( for b_{1} being subnet of M holds not [b_{1},x] in lim_inf-Convergence L ) )

thus M in NetUniv L by A16; :: thesis: for b_{1} being subnet of M holds not [b_{1},x] in lim_inf-Convergence L

for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L_{1} being subnet of M holds not [b_{1},x] in lim_inf-Convergence L
; :: thesis: verum

end;A16: M in NetUniv L and

A17: not x >= inf M ;

take M ; :: thesis: ( M in NetUniv L & ( for b

thus M in NetUniv L by A16; :: thesis: for b

for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L

proof

hence
for b
let M1 be subnet of M; :: thesis: not [M1,x] in lim_inf-Convergence L

A18: M1 is subnet of M1 by YELLOW_6:14;

A19: ( lim_inf M1 >= lim_inf M & lim_inf M >= inf M ) by Th1, WAYBEL21:37;

assume A20: [M1,x] in lim_inf-Convergence L ; :: thesis: contradiction

then M1 in NetUniv L by A5, ZFMISC_1:87;

then x = lim_inf M1 by A20, A18, Def3;

hence contradiction by A17, A19, YELLOW_0:def 2; :: thesis: verum

end;A18: M1 is subnet of M1 by YELLOW_6:14;

A19: ( lim_inf M1 >= lim_inf M & lim_inf M >= inf M ) by Th1, WAYBEL21:37;

assume A20: [M1,x] in lim_inf-Convergence L ; :: thesis: contradiction

then M1 in NetUniv L by A5, ZFMISC_1:87;

then x = lim_inf M1 by A20, A18, Def3;

hence contradiction by A17, A19, YELLOW_0:def 2; :: thesis: verum