:: Lim-inf Convergence
::  by Bart{\l}omiej Skorulski
::
:: Received January 6, 2000
:: Copyright (c) 2000-2021 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;


begin

theorem :: WAYBEL28:1
  for L being complete LATTICE, N being net of L holds inf N <= lim_inf N;

theorem :: WAYBEL28:2 ::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);

theorem :: WAYBEL28:3
  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);

definition
  let N be non empty RelStr;
  let f be Function of N,N;
  attr f is greater_or_equal_to_id means
:: WAYBEL28:def 1

  for j being Element of N holds j <= f.j;
end;

theorem :: WAYBEL28:4
  for N being reflexive non empty RelStr holds id N is greater_or_equal_to_id;

theorem :: WAYBEL28:5
  for N being directed non empty RelStr, x,y being Element of N ex
  z being Element of N st x <= z & y <= z;

registration
  let N be directed non empty RelStr;
  cluster greater_or_equal_to_id for Function of N,N;
end;

registration
  let N be reflexive non empty RelStr;
  cluster greater_or_equal_to_id for Function of N,N;
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
:: WAYBEL28:def 2

  the RelStr of it =
  the RelStr of N & the mapping of it = (the mapping of N) * f;
end;

theorem :: WAYBEL28:6
  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;

theorem :: WAYBEL28:7
  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#);

theorem :: WAYBEL28:8
  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;

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

theorem :: WAYBEL28:9
  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;

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

theorem :: WAYBEL28:10
  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;

theorem :: WAYBEL28:11
  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;

theorem :: WAYBEL28:12
  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;

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

theorem :: WAYBEL28:13 ::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);

theorem :: WAYBEL28:14
  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;

definition
  let L be non empty RelStr;
  func lim_inf-Convergence L -> Convergence-Class of L means
:: WAYBEL28:def 3

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

theorem :: WAYBEL28:15
  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;

theorem :: WAYBEL28:16
  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;

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

theorem :: WAYBEL28:17
  for L being complete LATTICE holds lim_inf-Convergence L is (CONSTANTS);

theorem :: WAYBEL28:18
  for L being non empty RelStr holds lim_inf-Convergence L is (SUBNETS);

theorem :: WAYBEL28:19
  for L being continuous complete LATTICE holds lim_inf-Convergence L is
  (DIVERGENCE);

theorem :: WAYBEL28:20
  for L being non empty RelStr, N,x being set holds [N,x] in
  lim_inf-Convergence L implies N in NetUniv L;

theorem :: WAYBEL28:21
  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;

theorem :: WAYBEL28:22
  for L being non empty reflexive RelStr holds lim_inf-Convergence
  L c= Scott-Convergence L;

theorem :: WAYBEL28:23
  for X,Y being set holds X c= Y implies X in the_universe_of Y;

theorem :: WAYBEL28:24
  for L being non empty transitive reflexive RelStr, D being
  directed non empty Subset of L holds Net-Str D in NetUniv L;

theorem :: WAYBEL28:25
  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;

theorem :: WAYBEL28:26
  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;

theorem :: WAYBEL28:27
  for L being complete LATTICE, U1 being Subset of L holds U1 in
  xi(L) implies U1 is property(S);

theorem :: WAYBEL28:28
  for L being non empty reflexive RelStr, A being Subset of L
  holds A in sigma L implies A in xi L;

theorem :: WAYBEL28:29
  for L being complete LATTICE, A being Subset of L st A is upper
  holds A in xi L implies A in sigma L;

theorem :: WAYBEL28:30 ::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;