:: 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 )
proof end;

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

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)}
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th15: :: SETLIM_1:15
for X being set
for B being SetSequence of X
for f being Function st dom f = NAT & ( 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
proof end;

theorem Th16: :: SETLIM_1:16
for X being set
for B being SetSequence of X
for f being Function st dom f = NAT & ( 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)
proof end;

definition
let X be set ;
let B be SetSequence of X;
attr B 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 & ( 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 & ( for n being Element of NAT holds b1 . n = meet { (B . k) where k is Element of NAT : n <= k } ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = NAT & ( for n being Element of NAT holds b1 . n = meet { (B . k) where k is Element of NAT : n <= k } ) & dom b2 = NAT & ( for n being Element of NAT holds b2 . n = meet { (B . k) where k is Element of NAT : n <= k } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines inferior_setsequence SETLIM_1:def 2 :
for B, b2 being Function holds
( b2 = inferior_setsequence B iff ( dom b2 = NAT & ( 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
proof end;
end;

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

:: deftheorem Def3 defines superior_setsequence SETLIM_1:def 3 :
for B, b2 being Function holds
( b2 = superior_setsequence B iff ( dom b2 = NAT & ( 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
proof end;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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) `
proof end;

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) `
proof end;

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

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

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

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

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

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

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 & the_value_of B = A holds
for n being Element of NAT holds (inferior_setsequence B) . n = A
proof end;

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 & the_value_of B = A holds
for n being Element of NAT holds (superior_setsequence B) . n = A
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)) `
proof end;

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 & the_value_of B = A holds
( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )
proof end;

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 & lim B = Union B )
proof end;

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

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

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

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

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

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

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

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)) `
proof end;

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)) `
proof end;

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

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

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

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

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 & the_value_of S = A holds
( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
proof end;

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 & lim S = Union S )
proof end;

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 & lim S = Intersection S )
proof end;

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