WAYBEL28

:: Lim-inf Convergence
::  by Bart{\l}omiej Skorulski
::
:: Received January 6, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies REWRITE1, WAYBEL_0, ORDINAL2, XXREAL_0, LATTICES, FUNCT_1,
      SUBSET_1, TARSKI, STRUCT_0, RELAT_1, YELLOW_0, YELLOW_2, LATTICE3,
      EQREL_1, YELLOW_6, XBOOLE_0, ORDERS_2, RELAT_2, ZFMISC_1, SETFAM_1,
      PRE_TOPC, WAYBEL11, CLASSES1, CAT_1, PROB_1, YELLOW_9, RCOMP_1, WAYBEL28;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, STRUCT_0, CLASSES1, PRE_TOPC, ORDERS_2, LATTICE3,
      YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_3, YELLOW_6, YELLOW_9, WAYBEL_9,
      WAYBEL11, WAYBEL17;
 constructors CLASSES1, YELLOW_2, WAYBEL_3, WAYBEL17, YELLOW_9, RELSET_1;
 registrations RELAT_1, FUNCT_1, FUNCT_2, CLASSES2, STRUCT_0, LATTICE3,
      YELLOW_0, WAYBEL_0, WAYBEL_3, YELLOW_6, WAYBEL_9, WAYBEL11, WAYBEL17,
      YELLOW_9, RELSET_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, XBOOLE_0, RELAT_1, YELLOW_6, WAYBEL11;
 equalities XBOOLE_0, YELLOW_6, WAYBEL11, STRUCT_0;
 expansions TARSKI, YELLOW_6, WAYBEL11;
 theorems ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, TOPS_1, ORDERS_2,
      CLASSES1, WAYBEL_0, YELLOW_0, LATTICE3, YELLOW_2, YELLOW_4, YELLOW_6,
      WAYBEL_8, YELLOW_9, WAYBEL_9, WAYBEL11, YELLOW12, WAYBEL17, WAYBEL21;
 schemes RELSET_1, FUNCT_1;

begin

theorem Th1:
  for L being complete LATTICE, N being net of L holds inf N <= lim_inf N
proof
  let L be complete LATTICE, N be net of L;
  set X = the set of all
"/\"({N.i where i is Element of N :i >= j1},L) where j1 is Element
  of N;
  X c= the carrier of L
  proof
    let x be object;
    assume x in X;
    then ex j1 being Element of N st x = "/\"({N.i where i is Element of N :i
    >= j1},L);
    hence thesis;
  end;
  then reconsider X as Subset of L;
  set j = the Element of N;
A1: {N.i where i is Element of N:i >= j} c= rng the mapping of N
  proof
    let x be object;
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 >= j};
    then consider i being Element of N such that
A3: x = N.i and
    i >= j;
    x = (the mapping of N).i by A3,WAYBEL_0:def 8;
    hence thesis by A2,FUNCT_1:def 3;
  end;
  reconsider X as Subset of L;
  set x = "/\"({N.i where i is Element of N:i >= j},L);
  ex_inf_of {N.i where i is Element of N:i >= j},L & ex_inf_of rng the
  mapping of N,L by YELLOW_0:17;
  then
  "/\"({N.i where i is Element of N:i >= j},L) >= "/\"(rng the mapping of
  N,L) by A1,YELLOW_0:35;
  then x >= Inf(the mapping of N) by YELLOW_2:def 6;
  then
A4: inf N <= x by WAYBEL_9:def 2;
  ex_sup_of X,L by YELLOW_0:17;
  then x in X & X is_<=_than "\/"(X,L) by YELLOW_0:def 9;
  then x <= "\/"(X,L) by LATTICE3:def 9;
  hence thesis by A4,YELLOW_0:def 2;
end;

theorem ::3.1 Proposition (1)=>(2)
  for L being complete LATTICE, N being net of L, x being Element of L
holds (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)
proof
  let L be complete LATTICE, N be net of L, x be Element of L;
  assume
A1: for M being subnet of N holds x = lim_inf M;
  N is subnet of N by YELLOW_6:14;
  hence x=lim_inf N by A1;
  let M be subnet of N;
  x = lim_inf M by A1;
  hence thesis by Th1;
end;

theorem Th3:
  for L being complete LATTICE, N being net of L, x being Element
of L st N in NetUniv L holds (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)
proof
  let L be complete LATTICE, N be net of L, x be Element of L;
  assume
A1: N in NetUniv L;
  assume
A2: for M being subnet of N st M in NetUniv L holds x = lim_inf M;
  N is subnet of N by YELLOW_6:14;
  hence x=lim_inf N by A1,A2;
  let M be subnet of N;
  assume M in NetUniv L;
  then x = lim_inf M by A2;
  hence thesis by Th1;
end;

definition
  let N be non empty RelStr;
  let f be Function of N,N;
  attr f is greater_or_equal_to_id means
  :Def1:
  for j being Element of N holds j <= f.j;
end;

theorem Th4:
  for N being reflexive non empty RelStr holds id N is greater_or_equal_to_id
proof
  let N be reflexive non empty RelStr;
  let j be Element of N;
  reconsider n=j as Element of N;
  n <= (id N).n;
  hence thesis;
end;

theorem Th5:
  for N being directed non empty RelStr, x,y being Element of N ex
  z being Element of N st x <= z & y <= z
proof
  let N be directed non empty RelStr, x,y be Element of N;
  [#]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 thesis;
end;

registration
  let N be directed non empty RelStr;
  cluster greater_or_equal_to_id for Function of N,N;
  existence
proof
  defpred P[object,object] means
  for n,m being Element of N st $1=n & $2=m holds n
  <= m;
A1: for e being object st e in the carrier of N
   ex u being object st u in the carrier of N & P[e,u]
  proof
    let e be object;
    assume e in the carrier of N;
    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;
    thus u9 in the carrier of N;
    let n,m be Element of N;
    assume e=n & u9=m;
    hence thesis by A2;
  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 object st e in the carrier of N holds P[e,p.e] from
  FUNCT_1:sch 6(A1);
  reconsider p as Function of N,N by A3,FUNCT_2:2;
  take p;
  let j be Element of N;
  thus thesis by A4;
end;
end;

registration
  let N be reflexive non empty RelStr;
  cluster greater_or_equal_to_id for Function of N,N;
  existence
  proof
    take id N;
    thus thesis by Th4;
  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;
  func N * f -> strict non empty NetStr over L means
  :Def2:
  the RelStr of it =
  the RelStr of N & the mapping of it = (the mapping of N) * f;
  existence
  proof
    take NetStr (# the carrier of N,the InternalRel of N,(the mapping of N)*f
    #);
    thus thesis;
  end;
  uniqueness;
end;

theorem Th6:
  for L being non empty 1-sorted, N being non empty NetStr over L,
  f being Function of N, N holds the carrier of N * f = the carrier of N
proof
  let L be non empty 1-sorted, N be non empty NetStr over L, f be Function of
  N, N;
  the RelStr of N * f = the RelStr of N by Def2;
  hence thesis;
end;

theorem Th7:
  for L being non empty 1-sorted, N being non empty NetStr over L,
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, N be non empty NetStr over L, f be Function of
  N,N;
  the RelStr of N*f=the RelStr of N by Def2;
  hence thesis by Def2;
end;

theorem Th8:
  for L being non empty 1-sorted, N being transitive directed non
  empty RelStr, 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, N be transitive directed non empty RelStr, f be
  Function of the carrier of N,the carrier of L;
  set N2 = NetStr(#the carrier of N,the InternalRel of N,f#);
A1: the RelStr of N = the RelStr of N2;
  [#]N is directed by WAYBEL_0:def 6;
  then [#]N2 is directed by A1,WAYBEL_0:3;
  hence thesis by A1,WAYBEL_0:def 6,WAYBEL_8:13;
end;

registration
  let L be non empty 1-sorted, N be transitive directed non empty RelStr, f be
  Function of the carrier of N,the carrier of L;
  cluster NetStr (#the carrier of N,the InternalRel of N,f#) -> transitive
    directed non empty;
  correctness by Th8;
end;

theorem Th9:
  for L being non empty 1-sorted, N being net of L, p being
  Function of N,N holds N * p is net of L
proof
  let L be non empty 1-sorted, N be net of L, p be Function of N,N;
  N * p = NetStr(#the carrier of N,the InternalRel of N,(the mapping of N
    ) * p #) by Th7;
  hence thesis;
end;

registration
  let L be non empty 1-sorted, N be net of L;
  let p be Function of N,N;
  cluster N * p -> transitive directed;
  correctness by Th9;
end;

theorem Th10:
  for L being non empty 1-sorted, N being net of L, 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, N be net of L, p be Function of N,N;
  assume N 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 thesis by A1,YELLOW_6:def 11;
end;

theorem
  for L being non empty 1-sorted, N,M being net of L st the NetStr of N
  = the NetStr of M holds M is subnet of N
proof
  let L be non empty 1-sorted, N,M be net of L;
  assume
A1: the NetStr of N = the NetStr of M;
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;
    thus the mapping of M = (the mapping of N)*f2 by A1,A3;
    let m be Element of N;
    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;
    let p be Element of M;
    reconsider p1=p as Element of N by A1;
    assume n2 <= p;
    then [n2,p] in the InternalRel of M by ORDERS_2:def 5;
    then n <= p1 by A1,ORDERS_2:def 5;
    hence thesis by A5;
  end;
  hence thesis by YELLOW_6:def 9;
end;

theorem Th12:
  for L being non empty 1-sorted, N being net of L, 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;
  let N be net of L;
  let p be greater_or_equal_to_id Function of N,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;
    thus the mapping of (N * p) = (the mapping of N)*f by Def2;
    let m be Element of N;
    reconsider n=m as Element of (N * p) by Th6;
    take n;
    let k be Element of (N * p);
    assume
A1: n <= k;
    reconsider k1 = k as Element of N by Th6;
A2: k1 <= p.k1 by Def1;
    the RelStr of N*p = the RelStr of N by Def2;
    then m <= k1 by A1,YELLOW_0:1;
    hence thesis by A2,YELLOW_0:def 2;
  end;
  hence thesis by YELLOW_6:def 9;
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;
  redefine func N * p -> strict subnet of N;  :: redefines * (WAYBEL28, definition)
  correctness by Th12;
end;

theorem ::3.1 Proposition (2)=>(3)
  for L being complete LATTICE, N being net of L, x being Element of L
st N in NetUniv L holds (x=lim_inf N & for M being subnet of N st M in NetUniv
  L holds x >= inf M) implies 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:
  for L being complete LATTICE, N being net of L, x being Element
  of L holds (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
proof
  let L be complete LATTICE, N be net of L, x be Element of L;
  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);
  let M be subnet of N;
  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;
    defpred P[object,object] means
    for j being Element of N, 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;
      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;
      thus v >= k0 by A9;
      let v9 be Element of M;
      assume v9>= v;
      then v9 >= w by A10,YELLOW_0:def 2;
      hence f.(v9)>=j by A8;
      thus thesis by A8,A10;
    end;
A11: for e being object st e in the carrier of N
    ex u being object st u in the
    carrier of M & P[e,u]
    proof
      let e be object;
      assume e in the carrier of N;
      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;
      thus u in the carrier of M;
      let j be Element of N, v,v9 be Element of M;
      assume that
A14:  e=j and
A15:  u=v and
A16:  v9>= v;
      thus v >= k0 by A12,A15;
      thus f.(v9)>=j by A13,A14,A15,A16;
      thus thesis by A13,A14,A15,A16;
    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 object st e in the carrier of N holds P[e,g.e] from
    FUNCT_1:sch 6(A11);
    reconsider 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;
      reconsider v=g.j as Element of M;
      ex v9 being Element of M st v9>= v & v9>= v by Th5;
      hence thesis by A19;
    end;
    reconsider 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;
      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 thesis by A17,FUNCT_1:13;
    end;
    then reconsider p as greater_or_equal_to_id Function of N,N by Def1;
A21: the set of all (N*p).j where j is Element of (N*p) c= {M.k where
    k is Element of M:k >= k0}
    proof
      let y be object;
      assume y in the set of all (N*p).j where j is Element of (N*p);
      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 thesis by A24;
    end;
A25: ex_inf_of (the set of all (N*p).j where j is Element of (N*p)),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) = the set of all
(N*p).j where j is Element of (N*p)
    proof
      thus rng the mapping of (N*p) c= the set of all
(N*p).j where j is Element of (N*p)
      proof
        let y be object;
        assume y in rng the mapping of (N*p);
        then consider j1 being object 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 as Element of (N*p) by A28;
        y = (N*p).j1 by A29,WAYBEL_0:def 8;
        hence thesis;
      end;
      let y be object;
      assume y in the set of all (N*p).j where j is Element 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 thesis by A26,FUNCT_1:def 3;
    end;
A31: inf (N * p) <= x by A2;
    inf (N*p) = Inf the mapping of (N*p) by WAYBEL_9:def 2
      .= "/\"((the set of all (N*p).j where j is Element of (N*p)),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 thesis by A31,YELLOW_0:def 2;
  end;
  for b being Element of L st b in the set of all
 "/\"({M.k where k is Element of M:k
  >= k0},L) where k0 is Element of M holds b <= x
  proof
    let b be Element of L;
    assume b in the set of all
 "/\"({M.k where k is Element of M:k >= k0},L) where k0 is
    Element of M;
    then
    ex k0 being Element of M st b = "/\"({M.k where k is Element of M:k >=
    k0},L);
    hence thesis by A6;
  end;
  then
A32: x is_>=_than the set of all
 "/\" ({M.k where k is Element of M:k >= k0},L) where k0
  is Element of M by LATTICE3:def 9;
  ex_sup_of (the set of all "/\"({M.k where k is Element of M:k >= k0},L)
  where k0 is Element of M),L by YELLOW_0:17;
  then "\/"((the set of all "/\"({M.k where k is Element of M:k >= k0},L)
  where k0 is Element of M),L)<=x by A32,YELLOW_0:def 9;
  hence thesis by A5,ORDERS_2:2;
end;

definition
  let L be non empty RelStr;
  func lim_inf-Convergence L -> Convergence-Class of L means
  :Def3:
  for N being net of L st N in NetUniv L for x being Element of L holds
  [N,x] in it iff for M being subnet of N holds x = lim_inf M;
  existence
  proof
    defpred P[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, x being Element of L holds [N9,
    x] in C iff P[N9, x] from RELSET_1:sch 2;
    reconsider C as Convergence-Class of L by YELLOW_6:def 18;
    take C;
    let N be net of L;
    assume N in NetUniv L;
    then reconsider N1=N as Element of NetUniv L;
    let x be Element of L;
    thus [N,x] in C implies for M being subnet of N holds x = lim_inf M
    proof
      assume
A2:   [N,x] in C;
      let M be subnet of N;
      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 thesis;
    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;
    hence thesis by A1,A3;
  end;
  uniqueness
  proof
    let C1,C2 be Convergence-Class of L such that
A4: for N being net of L st N in NetUniv L 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 for x being Element of L
    holds [N,x] in C2 iff for M being subnet of N holds x = lim_inf M;
    let Ns,xs be object;
A6: C1 c= [:NetUniv L,the carrier of L:] by YELLOW_6:def 18;
    thus [Ns,xs] in C1 implies [Ns,xs] in C2
    proof
      assume
A7:   [Ns,xs] in C1;
      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 thesis by A5,A8,A9;
    end;
    assume
A10: [Ns,xs] in C2;
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 thesis by A4,A12,A13;
  end;
end;

theorem
  for L being complete LATTICE, N being net of L, 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;
  let N be net of L;
  let x be Element of L;
  assume
A1: N in NetUniv L;
  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;
  assume
A2: for M being subnet of N st M in NetUniv L holds x = lim_inf M;
  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 thesis by A1,Def3;
end;

theorem Th16:
  for L being non empty RelStr, N being constant net of L, M being
  subnet of N holds M is constant & the_value_of N = the_value_of M
proof
  let L be non empty RelStr, N be constant net of L, M be subnet of N;
  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.y) by FUNCT_1:def 12
    .= (the mapping of M).y by A1,FUNCT_1:12;
A4: dom f = the carrier of M by FUNCT_2:def 1;
  for n1,n2 being object 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 object;
    assume that
A5: n1 in dom (the mapping of M) and
A6: n2 in dom (the mapping of M);
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;
  end;
  then
A8: the mapping of M is constant by FUNCT_1:def 10;
  hence
A9: M is constant;
  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;
end;

definition
  let L be non empty RelStr;
  func xi L -> Subset-Family of L equals
  the topology of ConvergenceSpace
  lim_inf-Convergence L;
  correctness by YELLOW_6:def 24;
end;

theorem
  for L being complete LATTICE holds lim_inf-Convergence L is (CONSTANTS)
proof
  let L be complete LATTICE;
  let N be constant net of L;
A1: for M being subnet of N holds the_value_of N = lim_inf M
  proof
    let M be subnet of N;
A2: M is constant by Th16;
    thus the_value_of N = the_value_of M by Th16
      .= lim_inf M by A2,WAYBEL11:23;
  end;
  assume N in NetUniv L;
  hence thesis by A1,Def3;
end;

theorem
  for L being non empty RelStr holds lim_inf-Convergence L is (SUBNETS)
proof
  let L be non empty RelStr;
  let N be net of L, M be subnet of N;
  assume
A1: M in NetUniv L;
  let x be Element of L;
  assume
A2: [N,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;
    reconsider M19=M1 as subnet of N by YELLOW_6:15;
    x = lim_inf M19 by A2,A3,Def3;
    hence thesis;
  end;
  hence thesis by A1,Def3;
end;

theorem
  for L being continuous complete LATTICE holds lim_inf-Convergence L is
  (DIVERGENCE)
proof
  let L be continuous complete LATTICE;
  let N be net of L, x be Element of L;
  assume that
A1: N in NetUniv L and
A2: not [N,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 & for p being greater_or_equal_to_id Function of N,N
  holds 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 by A1,A4,Th10;
  suppose
A6: not x=lim_inf N & x<=lim_inf N;
    reconsider N9=N as subnet of N by YELLOW_6:14;
    take N9;
    thus N9 in NetUniv L by A1;
    given M2 being subnet of N9 such that
A7: [M2,x] in lim_inf-Convergence L;
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;
  end;
  suppose
    not x=lim_inf N & not x<=lim_inf N;
    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: not ex M1 being subnet of M st [M1,x] in Scott-Convergence L by A1,
YELLOW_6:def 22;
    take M;
    thus M in NetUniv L by A10;
    for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L
    proof
      let M1 be subnet of M;
A12:  not [M1,x] in Scott-Convergence L by A11;
      assume
A13:  [M1,x] in lim_inf-Convergence L;
      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;
    end;
    hence thesis;
  end;
  suppose
    not (for M being subnet of N st M in NetUniv L holds x >= inf M);
    then consider M being subnet of N such that
A16: M in NetUniv L and
A17: not x >= inf M;
    take M;
    thus M in NetUniv L by A16;
    for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L
    proof
      let M1 be subnet of M;
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;
      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;
    end;
    hence thesis;
  end;
end;

theorem
  for L being non empty RelStr, N,x being set holds [N,x] in
  lim_inf-Convergence L implies N in NetUniv L
proof
  let L be non empty RelStr, N,x be set;
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;
  hence thesis by A1,ZFMISC_1:87;
end;

theorem Th21:
  for L being non empty 1-sorted, C1,C2 being Convergence-Class of
L holds C1 c= C2 implies the topology of ConvergenceSpace C2 c= the topology of
  ConvergenceSpace C1
proof
  let L be non empty 1-sorted, C1,C2 be Convergence-Class of L;
  assume
A1: C1 c= C2;
  let A be object;
  assume A in the topology of ConvergenceSpace C2;
  then
  A in { V where V is Subset of L: for p being Element of L st p in V 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 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 for N
  being net of L st [N,p] in C1 holds N is_eventually_in V
  proof
    take V1;
    thus A=V1 by A2;
    let p be Element of L;
    assume
A4: p in V1;
    let N be net of L;
    assume [N,p] in C1;
    hence thesis by A1,A3,A4;
  end;
  then
  A in { V where V is Subset of L: for p being Element of L st p in V for
  N being net of L st [N,p] in C1 holds N is_eventually_in V};
  hence thesis by YELLOW_6:def 24;
end;

theorem Th22:
  for L being non empty reflexive RelStr holds lim_inf-Convergence
  L c= Scott-Convergence L
proof
  let L be non empty reflexive RelStr;
  let Ns,xs be object;
  assume
A1: [Ns,xs] in lim_inf-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;
  hence thesis by A3,A4,WAYBEL11:def 8;
end;

theorem Th23:
  for X,Y being set holds X c= Y implies X in the_universe_of Y
proof
  let X,Y be set;
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;
  then X c= the_transitive-closure_of Y by A1;
  hence thesis by A2,CLASSES1:def 1;
end;

theorem Th24:
  for L being non empty transitive reflexive RelStr, D being
  directed non empty Subset of L holds Net-Str D in NetUniv L
proof
  let L be non empty transitive reflexive RelStr;
  let D be directed non empty Subset of L;
  D in the_universe_of the carrier of L & the carrier of Net-Str D = D by Th23,
WAYBEL21:32;
  hence thesis by YELLOW_6:def 11;
end;

theorem Th25:
  for L being complete LATTICE, D being directed non empty Subset
  of L holds for M being subnet of Net-Str D holds lim_inf M = sup D
proof
  let L be complete LATTICE;
  let D be directed non empty Subset of L;
  for M being subnet of Net-Str D holds sup D >= inf M
  proof
    let M be subnet of Net-Str D;
    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 f = the carrier of M by FUNCT_2:def 1;
    then f.i in rng f by FUNCT_1:def 3;
    then
A3: "/\"(rng f,L) <= f.i by YELLOW_0:17,YELLOW_4:2;
    g.i in the carrier of Net-Str D;
    then
A4: g.i in D by WAYBEL21:32;
    then g.i = (id D).(g.i) by FUNCT_1:18
      .= (the mapping of Net-Str D).(g.i) by WAYBEL21:32
      .= f.i by A1,A2,FUNCT_1:12;
    then f.i <= sup D by A4,YELLOW_2:22;
    then sup D >= "/\"(rng f,L) by A3,YELLOW_0:def 2;
    then sup D >= Inf the mapping of M by YELLOW_2:def 6;
    hence thesis by WAYBEL_9:def 2;
  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 thesis by Th14;
end;

theorem Th26:
  for L being non empty complete LATTICE, D being directed non
  empty Subset of L holds [Net-Str D,sup D] in lim_inf-Convergence L
proof
  let L be non empty complete LATTICE;
  let D be directed non empty Subset of 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 thesis by Def3;
end;

theorem Th27:
  for L being complete LATTICE, U1 being Subset of L holds U1 in
  xi(L) implies U1 is property(S)
proof
  let L be complete LATTICE;
  let U1 be Subset of L;
  assume U1 in xi(L);
  then
  U1 in { V where V is Subset of L: for p being Element of L st p in V 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 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;
  assume
A2: sup D 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 as Element of L;
  take y1;
  thus y1 in D by A4,WAYBEL21:32;
  let x1 be Element of L;
  assume that
A5: x1 in D and
A6: x1 >= y1;
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 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 thesis by A3,A6,A7,YELLOW_0:60;
end;

theorem Th28:
  for L being non empty reflexive RelStr, A being Subset of L
  holds A in sigma L implies A in xi L
proof
  let L be non empty reflexive RelStr, A be Subset of L;
  assume
A1: A in sigma L;
  the topology of ConvergenceSpace Scott-Convergence L c= the topology of
  ConvergenceSpace lim_inf-Convergence L by Th21,Th22;
  hence thesis by A1;
end;

theorem Th29:
  for L being complete LATTICE, A being Subset of L st A is upper
  holds A in xi L implies A in sigma L
proof
  let L be complete LATTICE, A be Subset of L;
  set T = the Scott TopAugmentation of L;
A1: the RelStr of T = the RelStr of L by YELLOW_9:def 4;
  then reconsider A9=A as Subset of T;
  reconsider A9 as Subset of T;
  assume A is upper;
  then
A2: A9 is upper by A1,WAYBEL_0:25;
  assume A in xi 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 T by PRE_TOPC:def 2;
  hence thesis by YELLOW_9:51;
end;

theorem ::3.3 Proposition (ii)
  for L being complete LATTICE , 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, A be Subset of L;
  set T = the Scott TopAugmentation of L;
  assume
A1: A is lower;
  then reconsider A1=A as lower Subset of L;
A2: the RelStr of L = the RelStr of T by YELLOW_9:def 4;
  then reconsider A9=A as Subset of T;
  reconsider A9 as Subset of T;
A3: A1` is upper;
  thus A` in xi L implies A is closed_under_directed_sups
  proof
    assume A` in xi L;
    then A9` in sigma L by A3,A2,Th29;
    then A9` in the topology of T 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 thesis by A2,YELLOW12:20;
  end;
  assume A is closed_under_directed_sups;
  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 T by PRE_TOPC:def 2;
  then A` in sigma L by A2,YELLOW_9:51;
  hence thesis by Th28;
end;