:: WAYBEL28 semantic presentation begin theorem Th1: :: WAYBEL28:1 for L being complete LATTICE for N being net of L holds inf N <= lim_inf N proof let L be complete LATTICE; ::_thesis: for N being net of L holds inf N <= lim_inf N let N be net of L; ::_thesis: inf N <= lim_inf N set X = { ("/\" ( { (N . i) where i is Element of N : i >= j1 } ,L)) where j1 is Element of N : verum } ; { ("/\" ( { (N . i) where i is Element of N : i >= j1 } ,L)) where j1 is Element of N : verum } c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("/\" ( { (N . i) where i is Element of N : i >= j1 } ,L)) where j1 is Element of N : verum } or x in the carrier of L ) assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j1 } ,L)) where j1 is Element of N : verum } ; ::_thesis: x in the carrier of L then ex j1 being Element of N st x = "/\" ( { (N . i) where i is Element of N : i >= j1 } ,L) ; hence x in the carrier of L ; ::_thesis: verum end; then reconsider X = { ("/\" ( { (N . i) where i is Element of N : i >= j1 } ,L)) where j1 is Element of N : verum } as Subset of L ; set j = the Element of N; A1: { (N . i) where i is Element of N : i >= the Element of N } c= rng the mapping of N proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (N . i) where i is Element of N : i >= the Element of N } or x in rng the mapping of N ) A2: dom the mapping of N = the carrier of N by FUNCT_2:def_1; assume x in { (N . i) where i is Element of N : i >= the Element of N } ; ::_thesis: x in rng the mapping of N then consider i being Element of N such that A3: x = N . i and i >= the Element of N ; x = the mapping of N . i by A3, WAYBEL_0:def_8; hence x in rng the mapping of N by A2, FUNCT_1:def_3; ::_thesis: verum end; reconsider X = X as Subset of L ; set x = "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L); ( ex_inf_of { (N . i) where i is Element of N : i >= the Element of N } ,L & ex_inf_of rng the mapping of N,L ) by YELLOW_0:17; then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) >= "/\" ((rng the mapping of N),L) by A1, YELLOW_0:35; then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) >= Inf by YELLOW_2:def_6; then A4: inf N <= "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) by WAYBEL_9:def_2; ex_sup_of X,L by YELLOW_0:17; then ( "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) in X & X is_<=_than "\/" (X,L) ) by YELLOW_0:def_9; then "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,L) <= "\/" (X,L) by LATTICE3:def_9; hence inf N <= lim_inf N by A4, YELLOW_0:def_2; ::_thesis: verum end; theorem :: WAYBEL28:2 for L being complete LATTICE for N being net of L for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) ) proof let L be complete LATTICE; ::_thesis: for N being net of L for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) ) let N be net of L; ::_thesis: for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) ) let x be Element of L; ::_thesis: ( ( for M being subnet of N holds x = lim_inf M ) implies ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) ) ) assume A1: for M being subnet of N holds x = lim_inf M ; ::_thesis: ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) ) N is subnet of N by YELLOW_6:14; hence x = lim_inf N by A1; ::_thesis: for M being subnet of N holds x >= inf M let M be subnet of N; ::_thesis: x >= inf M x = lim_inf M by A1; hence x >= inf M by Th1; ::_thesis: verum end; theorem Th3: :: WAYBEL28:3 for L being complete LATTICE for N being net of L for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds x = lim_inf M ) holds ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds x >= inf M ) ) proof let L be complete LATTICE; ::_thesis: for N being net of L for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds x = lim_inf M ) holds ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds x >= inf M ) ) let N be net of L; ::_thesis: for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds x = lim_inf M ) holds ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds x >= inf M ) ) let x be Element of L; ::_thesis: ( N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds x = lim_inf M ) implies ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds x >= inf M ) ) ) assume A1: N in NetUniv L ; ::_thesis: ( ex M being subnet of N st ( M in NetUniv L & not x = lim_inf M ) or ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds x >= inf M ) ) ) assume A2: for M being subnet of N st M in NetUniv L holds x = lim_inf M ; ::_thesis: ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds x >= inf M ) ) N is subnet of N by YELLOW_6:14; hence x = lim_inf N by A1, A2; ::_thesis: for M being subnet of N st M in NetUniv L holds x >= inf M let M be subnet of N; ::_thesis: ( M in NetUniv L implies x >= inf M ) assume M in NetUniv L ; ::_thesis: x >= inf M then x = lim_inf M by A2; hence x >= inf M by Th1; ::_thesis: verum end; definition let N be non empty RelStr ; let f be Function of N,N; attrf is greater_or_equal_to_id means :Def1: :: WAYBEL28:def 1 for j being Element of N holds j <= f . j; end; :: deftheorem Def1 defines greater_or_equal_to_id WAYBEL28:def_1_:_ for N being non empty RelStr for f being Function of N,N holds ( f is greater_or_equal_to_id iff for j being Element of N holds j <= f . j ); theorem Th4: :: WAYBEL28:4 for N being non empty reflexive RelStr holds id N is greater_or_equal_to_id proof let N be non empty reflexive RelStr ; ::_thesis: id N is greater_or_equal_to_id let j be Element of N; :: according to WAYBEL28:def_1 ::_thesis: j <= (id N) . j reconsider n = j as Element of N ; n <= (id N) . n by FUNCT_1:18; hence j <= (id N) . j ; ::_thesis: verum end; theorem Th5: :: WAYBEL28:5 for N being non empty directed RelStr for x, y being Element of N ex z being Element of N st ( x <= z & y <= z ) proof let N be non empty directed RelStr ; ::_thesis: for x, y being Element of N ex z being Element of N st ( x <= z & y <= z ) let x, y be Element of N; ::_thesis: ex z being Element of N st ( x <= z & y <= z ) [#] N is directed by WAYBEL_0:def_6; then ex z being Element of N st ( z in [#] N & x <= z & y <= z ) by WAYBEL_0:def_1; hence ex z being Element of N st ( x <= z & y <= z ) ; ::_thesis: verum end; registration let N be non empty directed RelStr ; cluster non empty Relation-like the carrier of N -defined the carrier of N -valued Function-like V34( the carrier of N) V35( the carrier of N, the carrier of N) greater_or_equal_to_id for Element of bool [: the carrier of N, the carrier of N:]; existence ex b1 being Function of N,N st b1 is greater_or_equal_to_id proof defpred S1[ set , set ] means for n, m being Element of N st N = n & c2 = m holds n <= m; A1: for e being set st e in the carrier of N holds ex u being set st ( u in the carrier of N & S1[e,u] ) proof let e be set ; ::_thesis: ( e in the carrier of N implies ex u being set st ( u in the carrier of N & S1[e,u] ) ) assume e in the carrier of N ; ::_thesis: ex u being set st ( u in the carrier of N & S1[e,u] ) then reconsider e9 = e as Element of N ; consider u9 being Element of N such that A2: e9 <= u9 and e9 <= u9 by Th5; take u9 ; ::_thesis: ( u9 in the carrier of N & S1[e,u9] ) thus u9 in the carrier of N ; ::_thesis: S1[e,u9] let n, m be Element of N; ::_thesis: ( e = n & u9 = m implies n <= m ) assume ( e = n & u9 = m ) ; ::_thesis: n <= m hence n <= m by A2; ::_thesis: verum end; consider p being Function such that A3: ( dom p = the carrier of N & rng p c= the carrier of N ) and A4: for e being set st e in the carrier of N holds S1[e,p . e] from FUNCT_1:sch_5(A1); reconsider p = p as Function of N,N by A3, FUNCT_2:2; take p ; ::_thesis: p is greater_or_equal_to_id let j be Element of N; :: according to WAYBEL28:def_1 ::_thesis: j <= p . j thus j <= p . j by A4; ::_thesis: verum end; end; registration let N be non empty reflexive RelStr ; cluster non empty Relation-like the carrier of N -defined the carrier of N -valued Function-like V34( the carrier of N) V35( the carrier of N, the carrier of N) greater_or_equal_to_id for Element of bool [: the carrier of N, the carrier of N:]; existence ex b1 being Function of N,N st b1 is greater_or_equal_to_id proof take id N ; ::_thesis: id N is greater_or_equal_to_id thus id N is greater_or_equal_to_id by Th4; ::_thesis: verum end; end; definition let L be non empty 1-sorted ; let N be non empty NetStr over L; let f be Function of N,N; funcN * f -> non empty strict NetStr over L means :Def2: :: WAYBEL28:def 2 ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = the mapping of N * f ); existence ex b1 being non empty strict NetStr over L st ( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = the mapping of N * f ) proof take NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) ; ::_thesis: ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) = the mapping of N * f ) thus ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) = the mapping of N * f ) ; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict NetStr over L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = the mapping of N * f & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b2 = the mapping of N * f holds b1 = b2 ; end; :: deftheorem Def2 defines * WAYBEL28:def_2_:_ for L being non empty 1-sorted for N being non empty NetStr over L for f being Function of N,N for b4 being non empty strict NetStr over L holds ( b4 = N * f iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b4 = the mapping of N * f ) ); theorem Th6: :: WAYBEL28:6 for L being non empty 1-sorted for N being non empty NetStr over L for f being Function of N,N holds the carrier of (N * f) = the carrier of N proof let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L for f being Function of N,N holds the carrier of (N * f) = the carrier of N let N be non empty NetStr over L; ::_thesis: for f being Function of N,N holds the carrier of (N * f) = the carrier of N let f be Function of N,N; ::_thesis: the carrier of (N * f) = the carrier of N RelStr(# the carrier of (N * f), the InternalRel of (N * f) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def2; hence the carrier of (N * f) = the carrier of N ; ::_thesis: verum end; theorem Th7: :: WAYBEL28:7 for L being non empty 1-sorted for N being non empty NetStr over L for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) proof let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) let N be non empty NetStr over L; ::_thesis: for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) let f be Function of N,N; ::_thesis: N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) RelStr(# the carrier of (N * f), the InternalRel of (N * f) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def2; hence N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) by Def2; ::_thesis: verum end; theorem Th8: :: WAYBEL28:8 for L being non empty 1-sorted for N being non empty transitive directed RelStr for f being Function of the carrier of N, the carrier of L holds NetStr(# the carrier of N, the InternalRel of N,f #) is net of L proof let L be non empty 1-sorted ; ::_thesis: for N being non empty transitive directed RelStr for f being Function of the carrier of N, the carrier of L holds NetStr(# the carrier of N, the InternalRel of N,f #) is net of L let N be non empty transitive directed RelStr ; ::_thesis: for f being Function of the carrier of N, the carrier of L holds NetStr(# the carrier of N, the InternalRel of N,f #) is net of L let f be Function of the carrier of N, the carrier of L; ::_thesis: NetStr(# the carrier of N, the InternalRel of N,f #) is net of L set N2 = NetStr(# the carrier of N, the InternalRel of N,f #); A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,f #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,f #) #) ; [#] N is directed by WAYBEL_0:def_6; then [#] NetStr(# the carrier of N, the InternalRel of N,f #) is directed by A1, WAYBEL_0:3; hence NetStr(# the carrier of N, the InternalRel of N,f #) is net of L by A1, WAYBEL_0:def_6, WAYBEL_8:13; ::_thesis: verum end; registration let L be non empty 1-sorted ; let N be non empty transitive directed RelStr ; let f be Function of the carrier of N, the carrier of L; cluster NetStr(# the carrier of N, the InternalRel of N,f #) -> non empty transitive directed ; correctness coherence ( NetStr(# the carrier of N, the InternalRel of N,f #) is transitive & NetStr(# the carrier of N, the InternalRel of N,f #) is directed & not NetStr(# the carrier of N, the InternalRel of N,f #) is empty ); by Th8; end; theorem Th9: :: WAYBEL28:9 for L being non empty 1-sorted for N being net of L for p being Function of N,N holds N * p is net of L proof let L be non empty 1-sorted ; ::_thesis: for N being net of L for p being Function of N,N holds N * p is net of L let N be net of L; ::_thesis: for p being Function of N,N holds N * p is net of L let p be Function of N,N; ::_thesis: N * p is net of L N * p = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * p) #) by Th7; hence N * p is net of L ; ::_thesis: verum end; registration let L be non empty 1-sorted ; let N be net of L; let p be Function of N,N; clusterN * p -> non empty transitive strict directed ; correctness coherence ( N * p is transitive & N * p is directed ); by Th9; end; theorem Th10: :: WAYBEL28:10 for L being non empty 1-sorted for N being net of L for p being Function of N,N st N in NetUniv L holds N * p in NetUniv L proof let L be non empty 1-sorted ; ::_thesis: for N being net of L for p being Function of N,N st N in NetUniv L holds N * p in NetUniv L let N be net of L; ::_thesis: for p being Function of N,N st N in NetUniv L holds N * p in NetUniv L let p be Function of N,N; ::_thesis: ( N in NetUniv L implies N * p in NetUniv L ) assume N in NetUniv L ; ::_thesis: N * p in NetUniv L then A1: ex N1 being strict net of L st ( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by YELLOW_6:def_11; the carrier of (N * p) = the carrier of N by Th6; hence N * p in NetUniv L by A1, YELLOW_6:def_11; ::_thesis: verum end; theorem :: WAYBEL28:11 for L being non empty 1-sorted for N, M being net of L st NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) holds M is subnet of N proof let L be non empty 1-sorted ; ::_thesis: for N, M being net of L st NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) holds M is subnet of N let N, M be net of L; ::_thesis: ( NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) implies M is subnet of N ) assume A1: NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) ; ::_thesis: M is subnet of N A2: N is subnet of N by YELLOW_6:14; ex f being Function of M,N st ( the mapping of M = the mapping of N * f & ( for m being Element of N ex n being Element of M st for p being Element of M st n <= p holds m <= f . p ) ) proof consider f being Function of N,N such that A3: the mapping of N = the mapping of N * f and A4: for m being Element of N ex n being Element of N st for p being Element of N st n <= p holds m <= f . p by A2, YELLOW_6:def_9; reconsider f2 = f as Function of M,N by A1; take f2 ; ::_thesis: ( the mapping of M = the mapping of N * f2 & ( for m being Element of N ex n being Element of M st for p being Element of M st n <= p holds m <= f2 . p ) ) thus the mapping of M = the mapping of N * f2 by A1, A3; ::_thesis: for m being Element of N ex n being Element of M st for p being Element of M st n <= p holds m <= f2 . p let m be Element of N; ::_thesis: ex n being Element of M st for p being Element of M st n <= p holds m <= f2 . p consider n being Element of N such that A5: for p being Element of N st n <= p holds m <= f . p by A4; reconsider n2 = n as Element of M by A1; take n2 ; ::_thesis: for p being Element of M st n2 <= p holds m <= f2 . p let p be Element of M; ::_thesis: ( n2 <= p implies m <= f2 . p ) reconsider p1 = p as Element of N by A1; assume n2 <= p ; ::_thesis: m <= f2 . p then [n2,p] in the InternalRel of M by ORDERS_2:def_5; then n <= p1 by A1, ORDERS_2:def_5; hence m <= f2 . p by A5; ::_thesis: verum end; hence M is subnet of N by YELLOW_6:def_9; ::_thesis: verum end; theorem Th12: :: WAYBEL28:12 for L being non empty 1-sorted for N being net of L for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N proof let L be non empty 1-sorted ; ::_thesis: for N being net of L for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N let N be net of L; ::_thesis: for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N let p be greater_or_equal_to_id Function of N,N; ::_thesis: N * p is subnet of N ex f being Function of (N * p),N st ( the mapping of (N * p) = the mapping of N * f & ( for m being Element of N ex n being Element of (N * p) st for k being Element of (N * p) st n <= k holds m <= f . k ) ) proof the carrier of (N * p) = the carrier of N by Th6; then reconsider f = p as Function of (N * p),N ; take f ; ::_thesis: ( the mapping of (N * p) = the mapping of N * f & ( for m being Element of N ex n being Element of (N * p) st for k being Element of (N * p) st n <= k holds m <= f . k ) ) thus the mapping of (N * p) = the mapping of N * f by Def2; ::_thesis: for m being Element of N ex n being Element of (N * p) st for k being Element of (N * p) st n <= k holds m <= f . k let m be Element of N; ::_thesis: ex n being Element of (N * p) st for k being Element of (N * p) st n <= k holds m <= f . k reconsider n = m as Element of (N * p) by Th6; take n ; ::_thesis: for k being Element of (N * p) st n <= k holds m <= f . k let k be Element of (N * p); ::_thesis: ( n <= k implies m <= f . k ) assume A1: n <= k ; ::_thesis: m <= f . k reconsider k1 = k as Element of N by Th6; A2: k1 <= p . k1 by Def1; RelStr(# the carrier of (N * p), the InternalRel of (N * p) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def2; then m <= k1 by A1, YELLOW_0:1; hence m <= f . k by A2, YELLOW_0:def_2; ::_thesis: verum end; hence N * p is subnet of N by YELLOW_6:def_9; ::_thesis: verum end; definition let L be non empty 1-sorted ; let N be net of L; let p be greater_or_equal_to_id Function of N,N; :: original: * redefine funcN * p -> strict subnet of N; correctness coherence N * p is strict subnet of N; by Th12; end; theorem :: WAYBEL28:13 for L being complete LATTICE for N being net of L for x being Element of L st N in NetUniv L & x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds x >= inf M ) holds ( x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) ) by Th10; theorem Th14: :: WAYBEL28:14 for L being complete LATTICE for N being net of L for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds for M being subnet of N holds x = lim_inf M proof let L be complete LATTICE; ::_thesis: for N being net of L for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds for M being subnet of N holds x = lim_inf M let N be net of L; ::_thesis: for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds for M being subnet of N holds x = lim_inf M let x be Element of L; ::_thesis: ( x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) implies for M being subnet of N holds x = lim_inf M ) assume that A1: x = lim_inf N and A2: for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ; ::_thesis: for M being subnet of N holds x = lim_inf M let M be subnet of N; ::_thesis: x = lim_inf M consider f being Function of M,N such that A3: the mapping of M = the mapping of N * f and A4: for j being Element of N ex k being Element of M st for m being Element of M st k <= m holds j <= f . m by YELLOW_6:def_9; A5: x <= lim_inf M by A1, WAYBEL21:37; A6: for k0 being Element of M holds "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= x proof let k0 be Element of M; ::_thesis: "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= x defpred S1[ set , set ] means for j being Element of N for v, v9 being Element of M st \$1 = j & \$2 = v & v9 >= v holds ( v >= k0 & f . v9 >= j & f . v >= j ); A7: for j being Element of N ex v being Element of M st ( v >= k0 & ( for v9 being Element of M st v9 >= v holds ( f . v9 >= j & f . v >= j ) ) ) proof let j be Element of N; ::_thesis: ex v being Element of M st ( v >= k0 & ( for v9 being Element of M st v9 >= v holds ( f . v9 >= j & f . v >= j ) ) ) consider w being Element of M such that A8: for w9 being Element of M st w <= w9 holds j <= f . w9 by A4; consider v being Element of M such that A9: v >= k0 and A10: v >= w by Th5; take v ; ::_thesis: ( v >= k0 & ( for v9 being Element of M st v9 >= v holds ( f . v9 >= j & f . v >= j ) ) ) thus v >= k0 by A9; ::_thesis: for v9 being Element of M st v9 >= v holds ( f . v9 >= j & f . v >= j ) let v9 be Element of M; ::_thesis: ( v9 >= v implies ( f . v9 >= j & f . v >= j ) ) assume v9 >= v ; ::_thesis: ( f . v9 >= j & f . v >= j ) then v9 >= w by A10, YELLOW_0:def_2; hence f . v9 >= j by A8; ::_thesis: f . v >= j thus f . v >= j by A8, A10; ::_thesis: verum end; A11: for e being set st e in the carrier of N holds ex u being set st ( u in the carrier of M & S1[e,u] ) proof let e be set ; ::_thesis: ( e in the carrier of N implies ex u being set st ( u in the carrier of M & S1[e,u] ) ) assume e in the carrier of N ; ::_thesis: ex u being set st ( u in the carrier of M & S1[e,u] ) then reconsider e9 = e as Element of N ; consider u being Element of M such that A12: u >= k0 and A13: for v9 being Element of M st v9 >= u holds ( f . v9 >= e9 & f . u >= e9 ) by A7; take u ; ::_thesis: ( u in the carrier of M & S1[e,u] ) thus u in the carrier of M ; ::_thesis: S1[e,u] let j be Element of N; ::_thesis: for v, v9 being Element of M st e = j & u = v & v9 >= v holds ( v >= k0 & f . v9 >= j & f . v >= j ) let v, v9 be Element of M; ::_thesis: ( e = j & u = v & v9 >= v implies ( v >= k0 & f . v9 >= j & f . v >= j ) ) assume that A14: e = j and A15: u = v and A16: v9 >= v ; ::_thesis: ( v >= k0 & f . v9 >= j & f . v >= j ) thus v >= k0 by A12, A15; ::_thesis: ( f . v9 >= j & f . v >= j ) thus f . v9 >= j by A13, A14, A15, A16; ::_thesis: f . v >= j thus f . v >= j by A13, A14, A15, A16; ::_thesis: verum end; consider g being Function such that A17: dom g = the carrier of N and A18: rng g c= the carrier of M and A19: for e being set st e in the carrier of N holds S1[e,g . e] from FUNCT_1:sch_5(A11); reconsider g = g as Function of the carrier of N, the carrier of M by A17, A18, FUNCT_2:2; A20: for j being Element of N holds g . j >= k0 proof let j be Element of N; ::_thesis: g . j >= k0 reconsider v = g . j as Element of M ; ex v9 being Element of M st ( v9 >= v & v9 >= v ) by Th5; hence g . j >= k0 by A19; ::_thesis: verum end; reconsider g = g as Function of N,M ; reconsider p = f * g as Function of N,N ; for j being Element of N holds j <= p . j proof let j be Element of N; ::_thesis: j <= p . j reconsider v = g . j as Element of M ; [#] M is directed by WAYBEL_0:def_6; then ex v9 being Element of M st ( v9 in [#] M & v <= v9 & v <= v9 ) by WAYBEL_0:def_1; then j <= f . (g . j) by A19; hence j <= p . j by A17, FUNCT_1:13; ::_thesis: verum end; then reconsider p = p as greater_or_equal_to_id Function of N,N by Def1; A21: { ((N * p) . j) where j is Element of (N * p) : verum } c= { (M . k) where k is Element of M : k >= k0 } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { ((N * p) . j) where j is Element of (N * p) : verum } or y in { (M . k) where k is Element of M : k >= k0 } ) assume y in { ((N * p) . j) where j is Element of (N * p) : verum } ; ::_thesis: y in { (M . k) where k is Element of M : k >= k0 } then consider j being Element of (N * p) such that A22: y = (N * p) . j ; reconsider j9 = j as Element of N by Th6; A23: the carrier of (N * p) = the carrier of N by Th6; y = the mapping of (N * p) . j by A22, WAYBEL_0:def_8 .= ( the mapping of N * (f * g)) . j by Def2 .= ( the mapping of M * g) . j by A3, RELAT_1:36 .= the mapping of M . (g . j) by A17, A23, FUNCT_1:13 ; then A24: y = M . (g . j9) by WAYBEL_0:def_8; g . j9 >= k0 by A20; hence y in { (M . k) where k is Element of M : k >= k0 } by A24; ::_thesis: verum end; A25: ( ex_inf_of { ((N * p) . j) where j is Element of (N * p) : verum } ,L & ex_inf_of { (M . k) where k is Element of M : k >= k0 } ,L ) by YELLOW_0:17; A26: dom the mapping of (N * p) = the carrier of (N * p) by FUNCT_2:def_1; A27: rng the mapping of (N * p) = { ((N * p) . j) where j is Element of (N * p) : verum } proof thus rng the mapping of (N * p) c= { ((N * p) . j) where j is Element of (N * p) : verum } :: according to XBOOLE_0:def_10 ::_thesis: { ((N * p) . j) where j is Element of (N * p) : verum } c= rng the mapping of (N * p) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng the mapping of (N * p) or y in { ((N * p) . j) where j is Element of (N * p) : verum } ) assume y in rng the mapping of (N * p) ; ::_thesis: y in { ((N * p) . j) where j is Element of (N * p) : verum } then consider j1 being set such that A28: j1 in dom the mapping of (N * p) and A29: the mapping of (N * p) . j1 = y by FUNCT_1:def_3; reconsider j1 = j1 as Element of (N * p) by A28; y = (N * p) . j1 by A29, WAYBEL_0:def_8; hence y in { ((N * p) . j) where j is Element of (N * p) : verum } ; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { ((N * p) . j) where j is Element of (N * p) : verum } or y in rng the mapping of (N * p) ) assume y in { ((N * p) . j) where j is Element of (N * p) : verum } ; ::_thesis: y in rng the mapping of (N * p) then consider j being Element of (N * p) such that A30: y = (N * p) . j ; y = the mapping of (N * p) . j by A30, WAYBEL_0:def_8; hence y in rng the mapping of (N * p) by A26, FUNCT_1:def_3; ::_thesis: verum end; A31: inf (N * p) <= x by A2; inf (N * p) = Inf by WAYBEL_9:def_2 .= "/\" ( { ((N * p) . j) where j is Element of (N * p) : verum } ,L) by A27, YELLOW_2:def_6 ; then "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= inf (N * p) by A25, A21, YELLOW_0:35; hence "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) <= x by A31, YELLOW_0:def_2; ::_thesis: verum end; for b being Element of L st b in { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } holds b <= x proof let b be Element of L; ::_thesis: ( b in { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } implies b <= x ) assume b in { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } ; ::_thesis: b <= x then ex k0 being Element of M st b = "/\" ( { (M . k) where k is Element of M : k >= k0 } ,L) ; hence b <= x by A6; ::_thesis: verum end; then A32: x is_>=_than { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } by LATTICE3:def_9; ex_sup_of { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } ,L by YELLOW_0:17; then "\/" ( { ("/\" ( { (M . k) where k is Element of M : k >= k0 } ,L)) where k0 is Element of M : verum } ,L) <= x by A32, YELLOW_0:def_9; hence x = lim_inf M by A5, ORDERS_2:2; ::_thesis: verum end; definition let L be non empty RelStr ; func lim_inf-Convergence L -> Convergence-Class of L means :Def3: :: WAYBEL28:def 3 for N being net of L st N in NetUniv L holds for x being Element of L holds ( [N,x] in it iff for M being subnet of N holds x = lim_inf M ); existence ex b1 being Convergence-Class of L st for N being net of L st N in NetUniv L holds for x being Element of L holds ( [N,x] in b1 iff for M being subnet of N holds x = lim_inf M ) proof defpred S1[ set , set ] means ex N being strict net of L st ( \$1 = N & ( for M being subnet of N holds \$2 = lim_inf M ) ); consider C being Relation of (NetUniv L), the carrier of L such that A1: for N9 being Element of NetUniv L for x being Element of L holds ( [N9,x] in C iff S1[N9,x] ) from RELSET_1:sch_2(); reconsider C = C as Convergence-Class of L by YELLOW_6:def_18; take C ; ::_thesis: for N being net of L st N in NetUniv L holds for x being Element of L holds ( [N,x] in C iff for M being subnet of N holds x = lim_inf M ) let N be net of L; ::_thesis: ( N in NetUniv L implies for x being Element of L holds ( [N,x] in C iff for M being subnet of N holds x = lim_inf M ) ) assume N in NetUniv L ; ::_thesis: for x being Element of L holds ( [N,x] in C iff for M being subnet of N holds x = lim_inf M ) then reconsider N1 = N as Element of NetUniv L ; let x be Element of L; ::_thesis: ( [N,x] in C iff for M being subnet of N holds x = lim_inf M ) thus ( [N,x] in C implies for M being subnet of N holds x = lim_inf M ) ::_thesis: ( ( for M being subnet of N holds x = lim_inf M ) implies [N,x] in C ) proof assume A2: [N,x] in C ; ::_thesis: for M being subnet of N holds x = lim_inf M let M be subnet of N; ::_thesis: x = lim_inf M ex N2 being strict net of L st ( N1 = N2 & ( for M being subnet of N2 holds x = lim_inf M ) ) by A1, A2; hence x = lim_inf M ; ::_thesis: verum end; A3: ex N2 being strict net of L st ( N2 = N1 & the carrier of N2 in the_universe_of the carrier of L ) by YELLOW_6:def_11; assume for M being subnet of N holds x = lim_inf M ; ::_thesis: [N,x] in C hence [N,x] in C by A1, A3; ::_thesis: verum end; uniqueness for b1, b2 being Convergence-Class of L st ( for N being net of L st N in NetUniv L holds for x being Element of L holds ( [N,x] in b1 iff for M being subnet of N holds x = lim_inf M ) ) & ( for N being net of L st N in NetUniv L holds for x being Element of L holds ( [N,x] in b2 iff for M being subnet of N holds x = lim_inf M ) ) holds b1 = b2 proof let C1, C2 be Convergence-Class of L; ::_thesis: ( ( for N being net of L st N in NetUniv L holds for x being Element of L holds ( [N,x] in C1 iff for M being subnet of N holds x = lim_inf M ) ) & ( for N being net of L st N in NetUniv L holds for x being Element of L holds ( [N,x] in C2 iff for M being subnet of N holds x = lim_inf M ) ) implies C1 = C2 ) assume that A4: for N being net of L st N in NetUniv L holds for x being Element of L holds ( [N,x] in C1 iff for M being subnet of N holds x = lim_inf M ) and A5: for N being net of L st N in NetUniv L holds for x being Element of L holds ( [N,x] in C2 iff for M being subnet of N holds x = lim_inf M ) ; ::_thesis: C1 = C2 let Ns, xs be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [Ns,xs] in C1 or [Ns,xs] in C2 ) & ( not [Ns,xs] in C2 or [Ns,xs] in C1 ) ) A6: C1 c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18; thus ( [Ns,xs] in C1 implies [Ns,xs] in C2 ) ::_thesis: ( not [Ns,xs] in C2 or [Ns,xs] in C1 ) proof assume A7: [Ns,xs] in C1 ; ::_thesis: [Ns,xs] in C2 then reconsider x = xs as Element of L by A6, ZFMISC_1:87; Ns in NetUniv L by A6, A7, ZFMISC_1:87; then consider N being strict net of L such that A8: N = Ns and the carrier of N in the_universe_of the carrier of L by YELLOW_6:def_11; A9: N in NetUniv L by A6, A7, A8, ZFMISC_1:87; then for M being subnet of N holds x = lim_inf M by A4, A7, A8; hence [Ns,xs] in C2 by A5, A8, A9; ::_thesis: verum end; assume A10: [Ns,xs] in C2 ; ::_thesis: [Ns,xs] in C1 A11: C2 c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18; then reconsider x = xs as Element of L by A10, ZFMISC_1:87; Ns in NetUniv L by A11, A10, ZFMISC_1:87; then consider N being strict net of L such that A12: N = Ns and the carrier of N in the_universe_of the carrier of L by YELLOW_6:def_11; A13: N in NetUniv L by A11, A10, A12, ZFMISC_1:87; then for M being subnet of N holds x = lim_inf M by A5, A10, A12; hence [Ns,xs] in C1 by A4, A12, A13; ::_thesis: verum end; end; :: deftheorem Def3 defines lim_inf-Convergence WAYBEL28:def_3_:_ for L being non empty RelStr for b2 being Convergence-Class of L holds ( b2 = lim_inf-Convergence L iff for N being net of L st N in NetUniv L holds for x being Element of L holds ( [N,x] in b2 iff for M being subnet of N holds x = lim_inf M ) ); theorem :: WAYBEL28:15 for L being complete LATTICE for N being net of L for x being Element of L st N in NetUniv L holds ( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds x = lim_inf M ) proof let L be complete LATTICE; ::_thesis: for N being net of L for x being Element of L st N in NetUniv L holds ( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds x = lim_inf M ) let N be net of L; ::_thesis: for x being Element of L st N in NetUniv L holds ( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds x = lim_inf M ) let x be Element of L; ::_thesis: ( N in NetUniv L implies ( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds x = lim_inf M ) ) assume A1: N in NetUniv L ; ::_thesis: ( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds x = lim_inf M ) hence ( [N,x] in lim_inf-Convergence L implies for M being subnet of N st M in NetUniv L holds x = lim_inf M ) by Def3; ::_thesis: ( ( for M being subnet of N st M in NetUniv L holds x = lim_inf M ) implies [N,x] in lim_inf-Convergence L ) assume A2: for M being subnet of N st M in NetUniv L holds x = lim_inf M ; ::_thesis: [N,x] in lim_inf-Convergence L then for M being subnet of N st M in NetUniv L holds x >= inf M by A1, Th3; then A3: for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) by A1, Th10; x = lim_inf N by A1, A2, Th3; then for M being subnet of N holds x = lim_inf M by A3, Th14; hence [N,x] in lim_inf-Convergence L by A1, Def3; ::_thesis: verum end; theorem Th16: :: WAYBEL28:16 for L being non empty RelStr for N being constant net of L for M being subnet of N holds ( M is constant & the_value_of N = the_value_of M ) proof let L be non empty RelStr ; ::_thesis: for N being constant net of L for M being subnet of N holds ( M is constant & the_value_of N = the_value_of M ) let N be constant net of L; ::_thesis: for M being subnet of N holds ( M is constant & the_value_of N = the_value_of M ) let M be subnet of N; ::_thesis: ( M is constant & the_value_of N = the_value_of M ) consider f being Function of M,N such that A1: the mapping of M = the mapping of N * f and for m being Element of N ex n being Element of M st for p being Element of M st n <= p holds m <= f . p by YELLOW_6:def_9; set y = the Element of dom the mapping of M; A2: dom the mapping of N = the carrier of N by FUNCT_2:def_1; then A3: the_value_of the mapping of N = the mapping of N . (f . the Element of dom the mapping of M) by FUNCT_1:def_12 .= the mapping of M . the Element of dom the mapping of M by A1, FUNCT_1:12 ; A4: dom f = the carrier of M by FUNCT_2:def_1; for n1, n2 being set st n1 in dom the mapping of M & n2 in dom the mapping of M holds the mapping of M . n1 = the mapping of M . n2 proof let n1, n2 be set ; ::_thesis: ( n1 in dom the mapping of M & n2 in dom the mapping of M implies the mapping of M . n1 = the mapping of M . n2 ) assume that A5: n1 in dom the mapping of M and A6: n2 in dom the mapping of M ; ::_thesis: the mapping of M . n1 = the mapping of M . n2 A7: ( f . n1 in rng f & f . n2 in rng f ) by A4, A5, A6, FUNCT_1:def_3; thus the mapping of M . n1 = the mapping of N . (f . n1) by A1, A4, A5, FUNCT_1:13 .= the mapping of N . (f . n2) by A2, A7, FUNCT_1:def_10 .= the mapping of M . n2 by A1, A4, A6, FUNCT_1:13 ; ::_thesis: verum end; then A8: the mapping of M is constant by FUNCT_1:def_10; hence A9: M is constant by YELLOW_6:def_4; ::_thesis: the_value_of N = the_value_of M thus the_value_of N = the_value_of the mapping of N by YELLOW_6:def_8 .= the_value_of the mapping of M by A8, A3, FUNCT_1:def_12 .= the_value_of M by A9, YELLOW_6:def_8 ; ::_thesis: verum end; definition let L be non empty RelStr ; func xi L -> Subset-Family of L equals :: WAYBEL28:def 4 the topology of (ConvergenceSpace (lim_inf-Convergence L)); correctness coherence the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Subset-Family of L; by YELLOW_6:def_24; end; :: deftheorem defines xi WAYBEL28:def_4_:_ for L being non empty RelStr holds xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L)); theorem :: WAYBEL28:17 for L being complete LATTICE holds lim_inf-Convergence L is (CONSTANTS) proof let L be complete LATTICE; ::_thesis: lim_inf-Convergence L is (CONSTANTS) let N be constant net of L; :: according to YELLOW_6:def_20 ::_thesis: ( not N in NetUniv L or [N,(the_value_of N)] in lim_inf-Convergence L ) A1: for M being subnet of N holds the_value_of N = lim_inf M proof let M be subnet of N; ::_thesis: the_value_of N = lim_inf M A2: M is constant by Th16; thus the_value_of N = the_value_of M by Th16 .= lim_inf M by A2, WAYBEL11:23 ; ::_thesis: verum end; assume N in NetUniv L ; ::_thesis: [N,(the_value_of N)] in lim_inf-Convergence L hence [N,(the_value_of N)] in lim_inf-Convergence L by A1, Def3; ::_thesis: verum end; theorem :: WAYBEL28:18 for L being non empty RelStr holds lim_inf-Convergence L is (SUBNETS) proof let L be non empty RelStr ; ::_thesis: lim_inf-Convergence L is (SUBNETS) let N be net of L; :: according to YELLOW_6:def_21 ::_thesis: for b1 being subnet of N holds ( not b1 in NetUniv L or for b2 being Element of the carrier of L holds ( not [N,b2] in lim_inf-Convergence L or [b1,b2] in lim_inf-Convergence L ) ) let M be subnet of N; ::_thesis: ( not M in NetUniv L or for b1 being Element of the carrier of L holds ( not [N,b1] in lim_inf-Convergence L or [M,b1] in lim_inf-Convergence L ) ) assume A1: M in NetUniv L ; ::_thesis: for b1 being Element of the carrier of L holds ( not [N,b1] in lim_inf-Convergence L or [M,b1] in lim_inf-Convergence L ) let x be Element of L; ::_thesis: ( not [N,x] in lim_inf-Convergence L or [M,x] in lim_inf-Convergence L ) assume A2: [N,x] in lim_inf-Convergence L ; ::_thesis: [M,x] in lim_inf-Convergence L lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18; then A3: N in NetUniv L by A2, ZFMISC_1:87; for M1 being subnet of M holds x = lim_inf M1 proof let M1 be subnet of M; ::_thesis: x = lim_inf M1 reconsider M19 = M1 as subnet of N by YELLOW_6:15; x = lim_inf M19 by A2, A3, Def3; hence x = lim_inf M1 ; ::_thesis: verum end; hence [M,x] in lim_inf-Convergence L by A1, Def3; ::_thesis: verum end; theorem :: WAYBEL28:19 for L being continuous complete LATTICE holds lim_inf-Convergence L is (DIVERGENCE) proof 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 b1 being Element of the carrier of L holds ( not N in NetUniv L or [N,b1] in lim_inf-Convergence L or ex b2 being subnet of N st ( b2 in NetUniv L & ( for b3 being subnet of b2 holds not [b3,b1] 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 b1 being subnet of N st ( b1 in NetUniv L & ( for b2 being subnet of b1 holds not [b2,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 b1 being subnet of N st ( b1 in NetUniv L & ( for b2 being subnet of b1 holds not [b2,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; percases ( ( 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; supposeA6: ( not x = lim_inf N & x <= lim_inf N ) ; ::_thesis: ex b1 being subnet of N st ( b1 in NetUniv L & ( for b2 being subnet of b1 holds not [b2,x] in lim_inf-Convergence L ) ) reconsider N9 = N as subnet of N by YELLOW_6:14; take N9 ; ::_thesis: ( N9 in NetUniv L & ( for b1 being subnet of N9 holds not [b1,x] in lim_inf-Convergence L ) ) thus N9 in NetUniv L by A1; ::_thesis: for b1 being subnet of N9 holds not [b1,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; suppose ( not x = lim_inf N & not x <= lim_inf N ) ; ::_thesis: ex b1 being subnet of N st ( b1 in NetUniv L & ( for b2 being subnet of b1 holds not [b2,x] in lim_inf-Convergence L ) ) then not x is_S-limit_of N by WAYBEL11:def_7; 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 b1 being subnet of M holds not [b1,x] in lim_inf-Convergence L ) ) thus M in NetUniv L by A10; ::_thesis: for b1 being subnet of M holds not [b1,x] in lim_inf-Convergence L for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L proof 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, WAYBEL11:def_7; ::_thesis: verum end; hence for b1 being subnet of M holds not [b1,x] in lim_inf-Convergence L ; ::_thesis: verum end; suppose ex M being subnet of N st ( M in NetUniv L & not x >= inf M ) ; ::_thesis: ex b1 being subnet of N st ( b1 in NetUniv L & ( for b2 being subnet of b1 holds not [b2,x] in lim_inf-Convergence L ) ) 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 b1 being subnet of M holds not [b1,x] in lim_inf-Convergence L ) ) thus M in NetUniv L by A16; ::_thesis: for b1 being subnet of M holds not [b1,x] in lim_inf-Convergence L for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L proof 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; hence for b1 being subnet of M holds not [b1,x] in lim_inf-Convergence L ; ::_thesis: verum end; end; end; theorem :: WAYBEL28:20 for L being non empty RelStr for N, x being set st [N,x] in lim_inf-Convergence L holds N in NetUniv L proof let L be non empty RelStr ; ::_thesis: for N, x being set st [N,x] in lim_inf-Convergence L holds N in NetUniv L let N, x be set ; ::_thesis: ( [N,x] in lim_inf-Convergence L implies N in NetUniv L ) A1: lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18; assume [N,x] in lim_inf-Convergence L ; ::_thesis: N in NetUniv L hence N in NetUniv L by A1, ZFMISC_1:87; ::_thesis: verum end; theorem Th21: :: WAYBEL28:21 for L being non empty 1-sorted for C1, C2 being Convergence-Class of L st C1 c= C2 holds the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1) proof let L be non empty 1-sorted ; ::_thesis: for C1, C2 being Convergence-Class of L st C1 c= C2 holds the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1) let C1, C2 be Convergence-Class of L; ::_thesis: ( C1 c= C2 implies the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1) ) assume A1: C1 c= C2 ; ::_thesis: the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1) let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in the topology of (ConvergenceSpace C2) or A in the topology of (ConvergenceSpace C1) ) assume A in the topology of (ConvergenceSpace C2) ; ::_thesis: A in the topology of (ConvergenceSpace C1) then A in { V where V is Subset of L : for p being Element of L st p in V holds for N being net of L st [N,p] in C2 holds N is_eventually_in V } by YELLOW_6:def_24; then consider V1 being Subset of L such that A2: A = V1 and A3: for p being Element of L st p in V1 holds for N being net of L st [N,p] in C2 holds N is_eventually_in V1 ; ex V being Subset of L st ( A = V & ( for p being Element of L st p in V holds for N being net of L st [N,p] in C1 holds N is_eventually_in V ) ) proof take V1 ; ::_thesis: ( A = V1 & ( for p being Element of L st p in V1 holds for N being net of L st [N,p] in C1 holds N is_eventually_in V1 ) ) thus A = V1 by A2; ::_thesis: for p being Element of L st p in V1 holds for N being net of L st [N,p] in C1 holds N is_eventually_in V1 let p be Element of L; ::_thesis: ( p in V1 implies for N being net of L st [N,p] in C1 holds N is_eventually_in V1 ) assume A4: p in V1 ; ::_thesis: for N being net of L st [N,p] in C1 holds N is_eventually_in V1 let N be net of L; ::_thesis: ( [N,p] in C1 implies N is_eventually_in V1 ) assume [N,p] in C1 ; ::_thesis: N is_eventually_in V1 hence N is_eventually_in V1 by A1, A3, A4; ::_thesis: verum end; then A in { V where V is Subset of L : for p being Element of L st p in V holds for N being net of L st [N,p] in C1 holds N is_eventually_in V } ; hence A in the topology of (ConvergenceSpace C1) by YELLOW_6:def_24; ::_thesis: verum end; theorem Th22: :: WAYBEL28:22 for L being non empty reflexive RelStr holds lim_inf-Convergence L c= Scott-Convergence L proof let L be non empty reflexive RelStr ; ::_thesis: lim_inf-Convergence L c= Scott-Convergence L let Ns, xs be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [Ns,xs] in lim_inf-Convergence L or [Ns,xs] in Scott-Convergence L ) assume A1: [Ns,xs] in lim_inf-Convergence L ; ::_thesis: [Ns,xs] in Scott-Convergence L A2: lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18; then reconsider x = xs as Element of L by A1, ZFMISC_1:87; Ns in NetUniv L by A2, A1, ZFMISC_1:87; then consider N being strict net of L such that A3: N = Ns and the carrier of N in the_universe_of the carrier of L by YELLOW_6:def_11; A4: N in NetUniv L by A2, A1, A3, ZFMISC_1:87; N is subnet of N by YELLOW_6:14; then x = lim_inf N by A1, A3, A4, Def3; then x is_S-limit_of N by WAYBEL11:def_7; hence [Ns,xs] in Scott-Convergence L by A3, A4, WAYBEL11:def_8; ::_thesis: verum end; theorem Th23: :: WAYBEL28:23 for X, Y being set st X c= Y holds X in the_universe_of Y proof let X, Y be set ; ::_thesis: ( X c= Y implies X in the_universe_of Y ) A1: Y c= the_transitive-closure_of Y by CLASSES1:52; Tarski-Class (the_transitive-closure_of Y) is_Tarski-Class_of the_transitive-closure_of Y by CLASSES1:def_4; then A2: the_transitive-closure_of Y in Tarski-Class (the_transitive-closure_of Y) by CLASSES1:def_3; assume X c= Y ; ::_thesis: X in the_universe_of Y then X c= the_transitive-closure_of Y by A1, XBOOLE_1:1; hence X in the_universe_of Y by A2, CLASSES1:def_1; ::_thesis: verum end; theorem Th24: :: WAYBEL28:24 for L being non empty reflexive transitive RelStr for D being non empty directed Subset of L holds Net-Str D in NetUniv L proof let L be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of L holds Net-Str D in NetUniv L let D be non empty directed Subset of L; ::_thesis: Net-Str D in NetUniv L ( D in the_universe_of the carrier of L & the carrier of (Net-Str D) = D ) by Th23, WAYBEL21:32; hence Net-Str D in NetUniv L by YELLOW_6:def_11; ::_thesis: verum end; theorem Th25: :: WAYBEL28:25 for L being complete LATTICE for D being non empty directed Subset of L for M being subnet of Net-Str D holds lim_inf M = sup D proof let L be complete LATTICE; ::_thesis: for D being non empty directed Subset of L for M being subnet of Net-Str D holds lim_inf M = sup D let D be non empty directed Subset of L; ::_thesis: for M being subnet of Net-Str D holds lim_inf M = sup D for M being subnet of Net-Str D holds sup D >= inf M proof let M be subnet of Net-Str D; ::_thesis: sup D >= inf M set i = the Element of M; set f = the mapping of M; consider g being Function of M,(Net-Str D) such that A1: the mapping of M = the mapping of (Net-Str D) * g and for m being Element of (Net-Str D) ex n being Element of M st for p being Element of M st n <= p holds m <= g . p by YELLOW_6:def_9; A2: dom the mapping of M = the carrier of M by FUNCT_2:def_1; then the mapping of M . the Element of M in rng the mapping of M by FUNCT_1:def_3; then A3: "/\" ((rng the mapping of M),L) <= the mapping of M . the Element of M by YELLOW_0:17, YELLOW_4:2; g . the Element of M in the carrier of (Net-Str D) ; then A4: g . the Element of M in D by WAYBEL21:32; then g . the Element of M = (id D) . (g . the Element of M) by FUNCT_1:18 .= the mapping of (Net-Str D) . (g . the Element of M) by WAYBEL21:32 .= the mapping of M . the Element of M by A1, A2, FUNCT_1:12 ; then the mapping of M . the Element of M <= sup D by A4, YELLOW_2:22; then sup D >= "/\" ((rng the mapping of M),L) by A3, YELLOW_0:def_2; then sup D >= Inf by YELLOW_2:def_6; hence sup D >= inf M by WAYBEL_9:def_2; ::_thesis: verum end; then ( lim_inf (Net-Str D) = sup D & ( for p being greater_or_equal_to_id Function of (Net-Str D),(Net-Str D) holds sup D >= inf ((Net-Str D) * p) ) ) by WAYBEL17:10; hence for M being subnet of Net-Str D holds lim_inf M = sup D by Th14; ::_thesis: verum end; theorem Th26: :: WAYBEL28:26 for L being non empty complete LATTICE for D being non empty directed Subset of L holds [(Net-Str D),(sup D)] in lim_inf-Convergence L proof let L be non empty complete LATTICE; ::_thesis: for D being non empty directed Subset of L holds [(Net-Str D),(sup D)] in lim_inf-Convergence L let D be non empty directed Subset of L; ::_thesis: [(Net-Str D),(sup D)] in lim_inf-Convergence L ( Net-Str D in NetUniv L & ( for M being subnet of Net-Str D holds lim_inf M = sup D ) ) by Th24, Th25; hence [(Net-Str D),(sup D)] in lim_inf-Convergence L by Def3; ::_thesis: verum end; theorem Th27: :: WAYBEL28:27 for L being complete LATTICE for U1 being Subset of L st U1 in xi L holds U1 is property(S) proof let L be complete LATTICE; ::_thesis: for U1 being Subset of L st U1 in xi L holds U1 is property(S) let U1 be Subset of L; ::_thesis: ( U1 in xi L implies U1 is property(S) ) assume U1 in xi L ; ::_thesis: U1 is property(S) then U1 in { V where V is Subset of L : for p being Element of L st p in V holds for N being net of L st [N,p] in lim_inf-Convergence L holds N is_eventually_in V } by YELLOW_6:def_24; then A1: ex V being Subset of L st ( U1 = V & ( for p being Element of L st p in V holds for N being net of L st [N,p] in lim_inf-Convergence L holds N is_eventually_in V ) ) ; let D be non empty directed Subset of L; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,L) in U1 or ex b1 being Element of the carrier of L st ( b1 in D & ( for b2 being Element of the carrier of L holds ( not b2 in D or not b1 <= b2 or b2 in U1 ) ) ) ) assume A2: sup D in U1 ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in D & ( for b2 being Element of the carrier of L holds ( not b2 in D or not b1 <= b2 or b2 in U1 ) ) ) [(Net-Str D),(sup D)] in lim_inf-Convergence L by Th26; then Net-Str D is_eventually_in U1 by A1, A2; then consider y being Element of (Net-Str D) such that A3: for x being Element of (Net-Str D) st y <= x holds (Net-Str D) . x in U1 by WAYBEL_0:def_11; A4: y in the carrier of (Net-Str D) ; then y in D by WAYBEL21:32; then reconsider y1 = y as Element of L ; reconsider y1 = y1 as Element of L ; take y1 ; ::_thesis: ( y1 in D & ( for b1 being Element of the carrier of L holds ( not b1 in D or not y1 <= b1 or b1 in U1 ) ) ) thus y1 in D by A4, WAYBEL21:32; ::_thesis: for b1 being Element of the carrier of L holds ( not b1 in D or not y1 <= b1 or b1 in U1 ) let x1 be Element of L; ::_thesis: ( not x1 in D or not y1 <= x1 or x1 in U1 ) assume that A5: x1 in D and A6: x1 >= y1 ; ::_thesis: x1 in U1 A7: Net-Str D is full SubRelStr of L by WAYBEL21:32; reconsider x = x1 as Element of (Net-Str D) by A5, WAYBEL21:32; reconsider x = x as Element of (Net-Str D) ; (Net-Str D) . x = the mapping of (Net-Str D) . x by WAYBEL_0:def_8 .= (id D) . x by WAYBEL21:32 .= x by A5, FUNCT_1:18 ; hence x1 in U1 by A3, A6, A7, YELLOW_0:60; ::_thesis: verum end; theorem Th28: :: WAYBEL28:28 for L being non empty reflexive RelStr for A being Subset of L st A in sigma L holds A in xi L proof let L be non empty reflexive RelStr ; ::_thesis: for A being Subset of L st A in sigma L holds A in xi L let A be Subset of L; ::_thesis: ( A in sigma L implies A in xi L ) assume A1: A in sigma L ; ::_thesis: A in xi L the topology of (ConvergenceSpace (Scott-Convergence L)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L)) by Th21, Th22; hence A in xi L by A1; ::_thesis: verum end; theorem Th29: :: WAYBEL28:29 for L being complete LATTICE for A being Subset of L st A is upper & A in xi L holds A in sigma L proof let L be complete LATTICE; ::_thesis: for A being Subset of L st A is upper & A in xi L holds A in sigma L let A be Subset of L; ::_thesis: ( A is upper & A in xi L implies A in sigma L ) set T = the Scott TopAugmentation of L; A1: RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4; then reconsider A9 = A as Subset of the Scott TopAugmentation of L ; reconsider A9 = A9 as Subset of the Scott TopAugmentation of L ; assume A is upper ; ::_thesis: ( not A in xi L or A in sigma L ) then A2: A9 is upper by A1, WAYBEL_0:25; assume A in xi L ; ::_thesis: A in sigma L then A9 is property(S) by A1, Th27, YELLOW12:19; then A9 is open by A2, WAYBEL11:15; then A9 in the topology of the Scott TopAugmentation of L by PRE_TOPC:def_2; hence A in sigma L by YELLOW_9:51; ::_thesis: verum end; theorem :: WAYBEL28:30 for L being complete LATTICE for A being Subset of L st A is lower holds ( A ` in xi L iff A is closed_under_directed_sups ) proof let L be complete LATTICE; ::_thesis: for A being Subset of L st A is lower holds ( A ` in xi L iff A is closed_under_directed_sups ) let A be Subset of L; ::_thesis: ( A is lower implies ( A ` in xi L iff A is closed_under_directed_sups ) ) set T = the Scott TopAugmentation of L; assume A1: A is lower ; ::_thesis: ( A ` in xi L iff A is closed_under_directed_sups ) then reconsider A1 = A as lower Subset of L ; A2: RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) by YELLOW_9:def_4; then reconsider A9 = A as Subset of the Scott TopAugmentation of L ; reconsider A9 = A9 as Subset of the Scott TopAugmentation of L ; A3: A1 ` is upper ; thus ( A ` in xi L implies A is closed_under_directed_sups ) ::_thesis: ( A is closed_under_directed_sups implies A ` in xi L ) proof assume A ` in xi L ; ::_thesis: A is closed_under_directed_sups then A9 ` in sigma L by A3, A2, Th29; then A9 ` in the topology of the Scott TopAugmentation of L by YELLOW_9:51; then A9 ` is open by PRE_TOPC:def_2; then A9 is closed by TOPS_1:3; then A9 is directly_closed by WAYBEL11:7; hence A is closed_under_directed_sups by A2, YELLOW12:20; ::_thesis: verum end; assume A is closed_under_directed_sups ; ::_thesis: A ` in xi L then A4: A9 is directly_closed by A2, YELLOW12:20; A9 is lower by A1, A2, WAYBEL_0:25; then A9 is closed by A4, WAYBEL11:7; then A9 ` is open by TOPS_1:3; then A9 ` in the topology of the Scott TopAugmentation of L by PRE_TOPC:def_2; then A ` in sigma L by A2, YELLOW_9:51; hence A ` in xi L by Th28; ::_thesis: verum end;