:: Limit of Sequence of Subsets
::  by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received March 15, 2005
:: Copyright (c) 2005-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 SUBSET_1, NUMBERS, PROB_1, XXREAL_0, ARYTM_3, FUNCT_1, XBOOLE_0,
      TARSKI, NAT_1, RELAT_1, CARD_1, SETFAM_1, EQREL_1, CARD_3, ZFMISC_1,
      SEQM_3, ORDINAL2, SEQ_2, SETLIM_1;
 notations ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1,
      TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, SETFAM_1, PROB_1,
      FUNCT_2, KURATO_0;
 constructors SETFAM_1, NAT_1, KURATO_0, XREAL_0, RELSET_1, FINSUB_1, PROB_2;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, FUNCT_2, RELAT_1, PROB_1,
      RELSET_1, NAT_1;
 requirements NUMERALS, BOOLE, SUBSET;


begin

reserve n,m,k,k1,k2,i,j for Nat;
reserve x,y,z for object,X,Y,Z for set;
reserve A for Subset of X;
reserve B,A1,A2,A3 for SetSequence of X;
reserve Si for SigmaField of X;
reserve S,S1,S2,S3 for SetSequence of Si;

theorem :: SETLIM_1:1
  for f be sequence of Y
   holds f.(n + m) in {f.k: n <= k};

theorem :: SETLIM_1:2
  for f being sequence of Y holds {f.k1: n <= k1} = {f.k2 : n+1
  <=k2} \/ {f.n};

theorem :: SETLIM_1:3
  for f be sequence of Y holds (for k1 holds x in f.(n+k1)) iff
  for Z st Z in {f.k2 : n <= k2} holds x in Z;

theorem :: SETLIM_1:4
  for Y being non empty set for f being sequence of Y holds x
  in rng f iff ex n st x = f.n;

theorem :: SETLIM_1:5
  for Y be non empty set for f being sequence of Y holds rng f
  = {f.k : 0 <= k};

theorem :: SETLIM_1:6
  for Y being non empty set for f being sequence of Y holds rng
  (f ^\ k) = {f.n: k <= n};

theorem :: SETLIM_1:7
  x in meet rng B iff for n being Nat holds x in B.n;

theorem :: SETLIM_1:8
  Intersection B = meet rng B;

theorem :: SETLIM_1:9
  Intersection B c= Union B;

theorem :: SETLIM_1:10
  (for n holds B.n = A) implies Union B = A;

theorem :: SETLIM_1:11
  (for n holds B.n = A) implies Intersection B = A;

theorem :: SETLIM_1:12
  B is constant implies Union B = Intersection B;

theorem :: SETLIM_1:13
  B is constant & the_value_of B = A implies for n holds union {B.
k: n <= k} = A;

theorem :: SETLIM_1:14
  B is constant & the_value_of B = A implies for n holds meet {B.k
  : n <= k} = A;

theorem :: SETLIM_1:15
  for X, B for f being Function st dom f = NAT & for n holds f.n =
  meet {B.k: n <= k} holds f is SetSequence of X;

theorem :: SETLIM_1:16
  for X being set, B being SetSequence of X for f being Function
  st dom f = NAT & for n holds f.n = union {B.k: n <= k} holds
  f is sequence of bool X;

definition
  let X,B;
  attr B is monotone means
:: SETLIM_1:def 1

  B is non-descending or B is non-ascending;
end;

definition
  let B be Function;
  func inferior_setsequence B -> Function means
:: SETLIM_1:def 2

  dom it = NAT & for n holds it.n = meet {B.k : n <= k};
end;

definition
  let X be set, B be SetSequence of X;
  redefine func inferior_setsequence B -> SetSequence of X;
end;

definition
  let B be Function;
  func superior_setsequence B -> Function means
:: SETLIM_1:def 3

  dom it = NAT & for n holds it.n = union {B.k : n <= k};
end;

definition
  let X be set, B be SetSequence of X;
  redefine func superior_setsequence B -> SetSequence of X;
end;

theorem :: SETLIM_1:17
  (inferior_setsequence B).0 = Intersection B;

theorem :: SETLIM_1:18
  (superior_setsequence B).0 = Union B;

theorem :: SETLIM_1:19
 for n being Nat holds
  x in (inferior_setsequence B).n iff
     for k being Nat holds x in B.(n+k);

theorem :: SETLIM_1:20
 for n being Nat holds
  x in (superior_setsequence B).n iff
   ex k being Nat st x in B.(n + k);

theorem :: SETLIM_1:21
 for n being Nat holds
  (inferior_setsequence B).n = (inferior_setsequence B).(n+1) /\ B .n;

theorem :: SETLIM_1:22
 for n being Nat holds
  (superior_setsequence B).n = (superior_setsequence B).(n+1) \/ B .n;

theorem :: SETLIM_1:23
  inferior_setsequence B is non-descending;

theorem :: SETLIM_1:24
  superior_setsequence B is non-ascending;

theorem :: SETLIM_1:25
  inferior_setsequence B is monotone & superior_setsequence B is monotone;

registration
  let X be set, A be SetSequence of X;
  cluster inferior_setsequence A -> non-descending for SetSequence of X;
end;

registration
  let X be set, A be SetSequence of X;
  cluster superior_setsequence A -> non-ascending for SetSequence of X;
end;

theorem :: SETLIM_1:26
  Intersection B c= (inferior_setsequence B).n;

theorem :: SETLIM_1:27
  (superior_setsequence B).n c= Union B;

theorem :: SETLIM_1:28
  for B,n holds {B.k: n <= k} is Subset-Family of X;

theorem :: SETLIM_1:29
  Union B = (Intersection Complement B)`;

theorem :: SETLIM_1:30
 for n being Element of NAT holds
  (inferior_setsequence B).n = ((superior_setsequence Complement B ).n)`;

theorem :: SETLIM_1:31
 for n being Element of NAT holds
  (superior_setsequence B).n = ((inferior_setsequence Complement B).n)`;

theorem :: SETLIM_1:32
  Complement (inferior_setsequence B) = (superior_setsequence Complement B);

theorem :: SETLIM_1:33
  Complement superior_setsequence B = inferior_setsequence Complement B;

theorem :: SETLIM_1:34
  (for n being Nat holds A3.n = A1.n \/ A2.n) implies
   for n being Nat holds (
  inferior_setsequence A1).n \/ (inferior_setsequence(A2)).n c= (
  inferior_setsequence(A3)).n;

theorem :: SETLIM_1:35
  (for n being Nat holds A3.n = A1.n /\ A2.n) implies
 for n being Nat holds (
  inferior_setsequence A3).n = (inferior_setsequence A1).n /\ (
  inferior_setsequence A2).n;

theorem :: SETLIM_1:36
  (for n holds A3.n = A1.n \/ A2.n) implies for n holds (
  superior_setsequence(A3)).n = (superior_setsequence(A1)).n \/ (
  superior_setsequence(A2)).n;

theorem :: SETLIM_1:37
  (for n holds A3.n = A1.n /\ A2.n) implies for n holds (
  superior_setsequence A3).n c= (superior_setsequence A1).n /\ (
  superior_setsequence A2).n;

theorem :: SETLIM_1:38
  B is constant & the_value_of B = A implies for n holds (
  inferior_setsequence B).n = A;

theorem :: SETLIM_1:39
  B is constant & the_value_of B = A implies for n holds (
  superior_setsequence B).n = A;

theorem :: SETLIM_1:40
 for n being Nat holds
  B is non-descending implies B.n c= (superior_setsequence(B)).(n+ 1);

theorem :: SETLIM_1:41
 for n being Nat holds
  B is non-descending implies (superior_setsequence B).n = (
  superior_setsequence B).(n+1);

theorem :: SETLIM_1:42
 for n being Nat holds
  B is non-descending implies (superior_setsequence B).n = Union B;

theorem :: SETLIM_1:43
  B is non-descending implies Intersection superior_setsequence B = Union B;

theorem :: SETLIM_1:44
  B is non-descending implies B.n c= (inferior_setsequence B).(n+1 );

theorem :: SETLIM_1:45
  B is non-descending implies (inferior_setsequence B).n = B.n;

theorem :: SETLIM_1:46
  B is non-descending implies inferior_setsequence B = B;

theorem :: SETLIM_1:47
  B is non-ascending implies (superior_setsequence B).(n+1) c= B.n;

theorem :: SETLIM_1:48
  B is non-ascending implies (superior_setsequence(B)).n = B.n;

theorem :: SETLIM_1:49
  B is non-ascending implies superior_setsequence(B) = B;

theorem :: SETLIM_1:50
 for n being Nat holds
  B is non-ascending implies (inferior_setsequence(B)).(n+1) c= B. n;

theorem :: SETLIM_1:51
 for n being Nat holds
  B is non-ascending implies (inferior_setsequence(B)).n = (
  inferior_setsequence(B)).(n+1);

theorem :: SETLIM_1:52
 for n being Nat holds
  B is non-ascending implies (inferior_setsequence(B)).n = Intersection B;

theorem :: SETLIM_1:53
  B is non-ascending implies Union inferior_setsequence(B) = Intersection B;

definition
  let X be set, B be SetSequence of X;
  redefine func lim_inf B equals
:: SETLIM_1:def 4
  Union inferior_setsequence B;
end;

definition
  let X be set, B be SetSequence of X;
  redefine func lim_sup B equals
:: SETLIM_1:def 5
  Intersection superior_setsequence B;
end;

notation
  let X be set, B be SetSequence of X;
  synonym lim B for lim_sup B;
end;

theorem :: SETLIM_1:54
  Intersection B c= lim_inf B;

theorem :: SETLIM_1:55
  lim_inf B = lim inferior_setsequence(B);

theorem :: SETLIM_1:56
  lim_sup B = lim superior_setsequence(B);

theorem :: SETLIM_1:57
  lim_sup B = (lim_inf Complement B)`;

theorem :: SETLIM_1:58
  B is constant & the_value_of B = A implies B is convergent & lim
  B = A & lim_inf B = A & lim_sup B = A;

theorem :: SETLIM_1:59
  B is non-descending implies lim_sup B = Union B;

theorem :: SETLIM_1:60
  B is non-descending implies lim_inf B = Union B;

theorem :: SETLIM_1:61
  B is non-ascending implies lim_sup B = Intersection B;

theorem :: SETLIM_1:62
  B is non-ascending implies lim_inf B = Intersection B;

theorem :: SETLIM_1:63
  B is non-descending implies B is convergent & lim B = Union B;

theorem :: SETLIM_1:64
  B is non-ascending implies B is convergent & lim B = Intersection B;

theorem :: SETLIM_1:65
  B is monotone implies B is convergent;

definition

  let X be set, Si be SigmaField of X, S be SetSequence of Si;
  redefine func inferior_setsequence S -> SetSequence of Si;
end;

definition
  let X be set, Si be SigmaField of X, S be SetSequence of Si;
  redefine func superior_setsequence S -> SetSequence of Si;
end;

theorem :: SETLIM_1:66
  x in lim_sup S iff for n being Nat
    ex k being Nat st x in S.(n+k);

theorem :: SETLIM_1:67
  x in lim_inf S iff ex n being Nat st for k being Nat holds x in S.(n+k);

theorem :: SETLIM_1:68
  Intersection S c= lim_inf S;

theorem :: SETLIM_1:69
  lim_sup S c= Union S;

theorem :: SETLIM_1:70
  lim_inf S c= lim_sup S;

theorem :: SETLIM_1:71
  lim_inf S = (lim_sup Complement S)`;

theorem :: SETLIM_1:72
  lim_sup S = (lim_inf Complement S)`;

theorem :: SETLIM_1:73
  (for n being Nat holds S3.n = S1.n \/ S2.n)
  implies lim_inf S1 \/ lim_inf S2 c=
  lim_inf S3;

theorem :: SETLIM_1:74
  (for n being Nat holds S3.n = S1.n /\ S2.n)
implies lim_inf S3 = lim_inf S1 /\
  lim_inf S2;

theorem :: SETLIM_1:75
  (for n being Nat holds S3.n = S1.n \/ S2.n)
implies lim_sup S3 = lim_sup S1 \/
  lim_sup S2;

theorem :: SETLIM_1:76
  (for n being Nat holds S3.n = S1.n /\ S2.n)
  implies lim_sup S3 c= lim_sup S1 /\ lim_sup S2;

theorem :: SETLIM_1:77
  S is constant & the_value_of S = A implies S is convergent & lim S = A
  & lim_inf S = A & lim_sup S = A;

theorem :: SETLIM_1:78
  S is non-descending implies lim_sup S = Union S;

theorem :: SETLIM_1:79
  S is non-descending implies lim_inf S = Union S;

theorem :: SETLIM_1:80
  S is non-descending implies S is convergent & lim S = Union S;

theorem :: SETLIM_1:81
  S is non-ascending implies lim_sup S = Intersection S;

theorem :: SETLIM_1:82
  S is non-ascending implies lim_inf S = Intersection S;

theorem :: SETLIM_1:83
  S is non-ascending implies S is convergent & lim S = Intersection S;

theorem :: SETLIM_1:84
  S is monotone implies S is convergent;