:: Limit of Sequence of Subsets
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received March 15, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

Lm1:  for i, j being Element of NAT holds
( not i <= j or i = j or i + 1 <= j )
proofend;

theorem Th1: :: SETLIM_1:1
for n, m being Element of NAT
for Y being set
for f being Function of NAT,Y holds f . (n + m) in  {  (f . k) where k is Element of NAT : n <= k  }
proofend;

theorem Th2: :: SETLIM_1:2
for n being Element of NAT
for Y being set
for f being Function of NAT,Y holds  {  (f . k1) where k1 is Element of NAT : n <= k1  }  =  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)}
proofend;

theorem Th3: :: SETLIM_1:3
for n being Element of NAT
for Y, x being set
for f being Function of NAT,Y holds
( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in  {  (f . k2) where k2 is Element of NAT : n <= k2  }  holds
x in Z )
proofend;

theorem Th4: :: SETLIM_1:4
for x being set
for Y being non empty set
for f being Function of NAT,Y holds
( x in rng f iff ex n being Element of NAT st x = f . n )
proofend;

theorem Th5: :: SETLIM_1:5
for Y being non empty set
for f being Function of NAT,Y holds rng f =  {  (f . k) where k is Element of NAT : 0 <= k  }
proofend;

theorem Th6: :: SETLIM_1:6
for k being Element of NAT
for Y being non empty set
for f being Function of NAT,Y holds rng (f ^\ k) =  {  (f . n) where n is Element of NAT : k <= n  }
proofend;

theorem Th7: :: SETLIM_1:7
for X, x being set
for B being SetSequence of X holds
( x in meet (rng B) iff for n being Element of NAT holds x in B . n )
proofend;

theorem Th8: :: SETLIM_1:8
for X being set
for B being SetSequence of X holds Intersection B = meet (rng B)
proofend;

theorem :: SETLIM_1:9
for X being set
for B being SetSequence of X holds Intersection B c= Union B
proofend;

theorem Th10: :: SETLIM_1:10
for X being set
for A being Subset of X
for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds
Union B = A
proofend;

theorem Th11: :: SETLIM_1:11
for X being set
for A being Subset of X
for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds
Intersection B = A
proofend;

theorem :: SETLIM_1:12
for X being set
for B being SetSequence of X st B is constant holds
Union B = Intersection B
proofend;

Lm2:  for X being set
for A being Subset of X
for B being SetSequence of X st B is constant &amp; the_value_of B = A holds
for n being Element of NAT holds
( B . n = A &amp; Union B = A &amp; Intersection B = A )
proofend;

theorem Th13: :: SETLIM_1:13
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant &amp; the_value_of B = A holds
for n being Element of NAT holds union  {  (B . k) where k is Element of NAT : n <= k  }  = A
proofend;

theorem Th14: :: SETLIM_1:14
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant &amp; the_value_of B = A holds
for n being Element of NAT holds meet  {  (B . k) where k is Element of NAT : n <= k  }  = A
proofend;

theorem Th15: :: SETLIM_1:15
for X being set
for B being SetSequence of X
for f being Function st dom f = NAT &amp; ( for n being Element of NAT holds f . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
f is SetSequence of X
proofend;

theorem Th16: :: SETLIM_1:16
for X being set
for B being SetSequence of X
for f being Function st dom f = NAT &amp; ( for n being Element of NAT holds f . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
f is Function of NAT,(bool X)
proofend;

definition
let X be set ;
let B be SetSequence of X;
attrB is monotone  means :Def1: :: SETLIM_1:def 1
( not B is V50() or not B is V49() );
end;

:: deftheorem Def1 defines monotone SETLIM_1:def_1_:_
 for X being set
for B being SetSequence of X holds
( B is monotone iff ( not B is V50() or not B is V49() ) );

definition
let B be Function;
func inferior_setsequence B ->  Function means :Def2: :: SETLIM_1:def 2
( dom it = NAT &amp; ( for n being Element of NAT holds it . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) );
existence
 ex b1 being Function st
( dom b1 = NAT &amp; ( for n being Element of NAT holds b1 . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = NAT &amp; ( for n being Element of NAT holds b1 . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) &amp; dom b2 = NAT &amp; ( for n being Element of NAT holds b2 . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines inferior_setsequence SETLIM_1:def_2_:_
 for B, b2 being Function holds
( b2 = inferior_setsequence B iff ( dom b2 = NAT &amp; ( for n being Element of NAT holds b2 . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) ) );

definition
let X be set ;
let B be SetSequence of X;
:: original:inferior_setsequence
redefine func inferior_setsequence B ->  SetSequence of X;
coherence
 inferior_setsequence B is SetSequence of X
proofend;
end;

definition
let B be Function;
func superior_setsequence B ->  Function means :Def3: :: SETLIM_1:def 3
( dom it = NAT &amp; ( for n being Element of NAT holds it . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) );
existence
 ex b1 being Function st
( dom b1 = NAT &amp; ( for n being Element of NAT holds b1 . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = NAT &amp; ( for n being Element of NAT holds b1 . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) &amp; dom b2 = NAT &amp; ( for n being Element of NAT holds b2 . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines superior_setsequence SETLIM_1:def_3_:_
 for B, b2 being Function holds
( b2 = superior_setsequence B iff ( dom b2 = NAT &amp; ( for n being Element of NAT holds b2 . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) ) );

definition
let X be set ;
let B be SetSequence of X;
:: original:superior_setsequence
redefine func superior_setsequence B ->  SetSequence of X;
coherence
 superior_setsequence B is SetSequence of X
proofend;
end;

theorem Th17: :: SETLIM_1:17
for X being set
for B being SetSequence of X holds (inferior_setsequence B) . 0 = Intersection B
proofend;

theorem Th18: :: SETLIM_1:18
for X being set
for B being SetSequence of X holds (superior_setsequence B) . 0 = Union B
proofend;

theorem Th19: :: SETLIM_1:19
for n being Element of NAT
for X, x being set
for B being SetSequence of X holds
( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) )
proofend;

theorem Th20: :: SETLIM_1:20
for n being Element of NAT
for X, x being set
for B being SetSequence of X holds
( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) )
proofend;

theorem Th21: :: SETLIM_1:21
for n being Element of NAT
for X being set
for B being SetSequence of X holds (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
proofend;

theorem Th22: :: SETLIM_1:22
for n being Element of NAT
for X being set
for B being SetSequence of X holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)
proofend;

theorem Th23: :: SETLIM_1:23
for X being set
for B being SetSequence of X holds inferior_setsequence B is V50()
proofend;

theorem Th24: :: SETLIM_1:24
for X being set
for B being SetSequence of X holds superior_setsequence B is V49()
proofend;

theorem :: SETLIM_1:25
for X being set
for B being SetSequence of X holds
( inferior_setsequence B is monotone &amp; superior_setsequence B is monotone )
proofend;

registration
let X be set ;
let A be SetSequence of X;
cluster inferior_setsequence A -> V50() for SetSequence of X;
coherence
 for b1 being SetSequence of X st b1 = inferior_setsequence A holds
b1 is non-descending by Th23;
end;

registration
let X be set ;
let A be SetSequence of X;
cluster superior_setsequence A -> V49() for SetSequence of X;
coherence
 for b1 being SetSequence of X st b1 = superior_setsequence A holds
b1 is non-ascending by Th24;
end;

theorem :: SETLIM_1:26
for n being Element of NAT
for X being set
for B being SetSequence of X holds Intersection B c= (inferior_setsequence B) . n
proofend;

theorem :: SETLIM_1:27
for n being Element of NAT
for X being set
for B being SetSequence of X holds (superior_setsequence B) . n c= Union B
proofend;

theorem Th28: :: SETLIM_1:28
for X being set
for B being SetSequence of X
for n being Element of NAT holds  {  (B . k) where k is Element of NAT : n <= k  }  is Subset-Family of X
proofend;

theorem :: SETLIM_1:29
for X being set
for B being SetSequence of X holds Union B = (Intersection (Complement B)) `
proofend;

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

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

theorem Th32: :: SETLIM_1:32
for X being set
for B being SetSequence of X holds Complement (inferior_setsequence B) = superior_setsequence (Complement B)
proofend;

theorem :: SETLIM_1:33
for X being set
for B being SetSequence of X holds Complement (superior_setsequence B) = inferior_setsequence (Complement B)
proofend;

theorem :: SETLIM_1:34
for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Element of NAT holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
proofend;

theorem :: SETLIM_1:35
for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Element of NAT holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)
proofend;

theorem :: SETLIM_1:36
for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Element of NAT holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
proofend;

theorem :: SETLIM_1:37
for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Element of NAT holds (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
proofend;

theorem Th38: :: SETLIM_1:38
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant &amp; the_value_of B = A holds
for n being Element of NAT holds (inferior_setsequence B) . n = A
proofend;

theorem Th39: :: SETLIM_1:39
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant &amp; the_value_of B = A holds
for n being Element of NAT holds (superior_setsequence B) . n = A
proofend;

theorem Th40: :: SETLIM_1:40
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V50() holds
B . n c= (superior_setsequence B) . (n + 1)
proofend;

theorem Th41: :: SETLIM_1:41
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V50() holds
(superior_setsequence B) . n = (superior_setsequence B) . (n + 1)
proofend;

theorem Th42: :: SETLIM_1:42
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V50() holds
(superior_setsequence B) . n = Union B
proofend;

theorem Th43: :: SETLIM_1:43
for X being set
for B being SetSequence of X st B is V50() holds
Intersection (superior_setsequence B) = Union B
proofend;

theorem Th44: :: SETLIM_1:44
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V50() holds
B . n c= (inferior_setsequence B) . (n + 1)
proofend;

theorem Th45: :: SETLIM_1:45
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V50() holds
(inferior_setsequence B) . n = B . n
proofend;

theorem Th46: :: SETLIM_1:46
for X being set
for B being SetSequence of X st B is V50() holds
inferior_setsequence B = B
proofend;

theorem Th47: :: SETLIM_1:47
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V49() holds
(superior_setsequence B) . (n + 1) c= B . n
proofend;

theorem Th48: :: SETLIM_1:48
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V49() holds
(superior_setsequence B) . n = B . n
proofend;

theorem Th49: :: SETLIM_1:49
for X being set
for B being SetSequence of X st B is V49() holds
superior_setsequence B = B
proofend;

theorem Th50: :: SETLIM_1:50
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . (n + 1) c= B . n
proofend;

theorem Th51: :: SETLIM_1:51
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1)
proofend;

theorem Th52: :: SETLIM_1:52
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . n = Intersection B
proofend;

theorem Th53: :: SETLIM_1:53
for X being set
for B being SetSequence of X st B is V49() holds
Union (inferior_setsequence B) = Intersection B
proofend;

definition
let X be set ;
let B be SetSequence of X;
redefine func lim_inf B equals :: SETLIM_1:def 4
 Union (inferior_setsequence B);
compatibility
 for b1 being Element of bool X holds
( b1 = lim_inf B iff b1 = Union (inferior_setsequence B) )
proofend;
end;

:: deftheorem  defines lim_inf SETLIM_1:def_4_:_
 for X being set
for B being SetSequence of X holds lim_inf B = Union (inferior_setsequence B);

definition
let X be set ;
let B be SetSequence of X;
redefine func lim_sup B equals :: SETLIM_1:def 5
 Intersection (superior_setsequence B);
compatibility
 for b1 being Element of bool X holds
( b1 = lim_sup B iff b1 = Intersection (superior_setsequence B) )
proofend;
end;

:: deftheorem  defines lim_sup SETLIM_1:def_5_:_
 for X being set
for B being SetSequence of X holds lim_sup B = Intersection (superior_setsequence B);

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

theorem :: SETLIM_1:54
for X being set
for B being SetSequence of X holds Intersection B c= lim_inf B
proofend;

theorem :: SETLIM_1:55
for X being set
for B being SetSequence of X holds lim_inf B = lim (inferior_setsequence B) by Th43;

theorem :: SETLIM_1:56
for X being set
for B being SetSequence of X holds lim_sup B = lim (superior_setsequence B) by Th49;

theorem :: SETLIM_1:57
for X being set
for B being SetSequence of X holds lim_sup B = (lim_inf (Complement B)) `
proofend;

theorem Th58: :: SETLIM_1:58
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant &amp; the_value_of B = A holds
( B is convergent &amp; lim B = A &amp; lim_inf B = A &amp; lim_sup B = A )
proofend;

theorem :: SETLIM_1:59
for X being set
for B being SetSequence of X st B is V50() holds
lim_sup B = Union B by Th43;

theorem :: SETLIM_1:60
for X being set
for B being SetSequence of X st B is V50() holds
lim_inf B = Union B by Th46;

theorem :: SETLIM_1:61
for X being set
for B being SetSequence of X st B is V49() holds
lim_sup B = Intersection B by Th49;

theorem :: SETLIM_1:62
for X being set
for B being SetSequence of X st B is V49() holds
lim_inf B = Intersection B by Th53;

theorem Th63: :: SETLIM_1:63
for X being set
for B being SetSequence of X st B is V50() holds
( B is convergent &amp; lim B = Union B )
proofend;

theorem Th64: :: SETLIM_1:64
for X being set
for B being SetSequence of X st B is V49() holds
( B is convergent &amp; lim B = Intersection B )
proofend;

theorem :: SETLIM_1:65
for X being set
for B being SetSequence of X st B is monotone holds
B is convergent
proofend;

definition
let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
:: original:inferior_setsequence
redefine func inferior_setsequence S ->  SetSequence of Si;
coherence
 inferior_setsequence S is SetSequence of Si
proofend;
end;

definition
let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
:: original:superior_setsequence
redefine func superior_setsequence S ->  SetSequence of Si;
coherence
 superior_setsequence S is SetSequence of Si
proofend;
end;

theorem Th66: :: SETLIM_1:66
for X, x being set
for Si being SigmaField of X
for S being SetSequence of Si holds
( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) )
proofend;

theorem Th67: :: SETLIM_1:67
for X, x being set
for Si being SigmaField of X
for S being SetSequence of Si holds
( x in lim_inf S iff ex n being Element of NAT st
for k being Element of NAT holds x in S . (n + k) )
proofend;

theorem :: SETLIM_1:68
for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds Intersection S c= lim_inf S
proofend;

theorem :: SETLIM_1:69
for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds lim_sup S c= Union S
proofend;

theorem :: SETLIM_1:70
for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds lim_inf S c= lim_sup S
proofend;

theorem Th71: :: SETLIM_1:71
for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) `
proofend;

theorem :: SETLIM_1:72
for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds lim_sup S = (lim_inf (Complement S)) `
proofend;

theorem :: SETLIM_1:73
for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
(lim_inf S1) \/ (lim_inf S2) c= lim_inf S3
proofend;

theorem :: SETLIM_1:74
for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_inf S3 = (lim_inf S1) /\ (lim_inf S2)
proofend;

theorem :: SETLIM_1:75
for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
lim_sup S3 = (lim_sup S1) \/ (lim_sup S2)
proofend;

theorem :: SETLIM_1:76
for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2)
proofend;

theorem :: SETLIM_1:77
for X being set
for A being Subset of X
for Si being SigmaField of X
for S being SetSequence of Si st S is constant &amp; the_value_of S = A holds
( S is convergent &amp; lim S = A &amp; lim_inf S = A &amp; lim_sup S = A )
proofend;

theorem Th78: :: SETLIM_1:78
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V50() holds
lim_sup S = Union S by Th43;

theorem Th79: :: SETLIM_1:79
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V50() holds
lim_inf S = Union S by Th46;

theorem Th80: :: SETLIM_1:80
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V50() holds
( S is convergent &amp; lim S = Union S )
proofend;

theorem Th81: :: SETLIM_1:81
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V49() holds
lim_sup S = Intersection S by Th49;

theorem Th82: :: SETLIM_1:82
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V49() holds
lim_inf S = Intersection S by Th53;

theorem Th83: :: SETLIM_1:83
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V49() holds
( S is convergent &amp; lim S = Intersection S )
proofend;

theorem :: SETLIM_1:84
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is monotone holds
S is convergent
proofend;