:: Limit of Sequence of Subsets
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received March 15, 2005
:: Copyright (c) 2005-2011 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
( B is non-descending or B is non-ascending );

end;

:: deftheorem Def1 defines monotone SETLIM_1:def 1 :
for X being set
for B being SetSequence of X holds
( B is monotone iff ( B is non-descending or B is non-ascending ) );

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 b₁ being Function st
( dom b₁ = NAT & ( for n being Element of NAT holds b₁ . n = meet { (B . k) where k is Element of NAT : n <= k } ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & ( for n being Element of NAT holds b₁ . n = meet { (B . k) where k is Element of NAT : n <= k } ) & dom b₂ = NAT & ( for n being Element of NAT holds b₂ . n = meet { (B . k) where k is Element of NAT : n <= k } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines inferior_setsequence SETLIM_1:def 2 :
for B, b₂ being Function holds
( b₂ = inferior_setsequence B iff ( dom b₂ = NAT & ( for n being Element of NAT holds b₂ . 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 b₁ being Function st
( dom b₁ = NAT & ( for n being Element of NAT holds b₁ . n = union { (B . k) where k is Element of NAT : n <= k } ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & ( for n being Element of NAT holds b₁ . n = union { (B . k) where k is Element of NAT : n <= k } ) & dom b₂ = NAT & ( for n being Element of NAT holds b₂ . n = union { (B . k) where k is Element of NAT : n <= k } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines superior_setsequence SETLIM_1:def 3 :
for B, b₂ being Function holds
( b₂ = superior_setsequence B iff ( dom b₂ = NAT & ( for n being Element of NAT holds b₂ . 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 non-descending

proof end;

theorem Th24: :: SETLIM_1:24

for X being set
for B being SetSequence of X holds superior_setsequence B is non-ascending

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 -> V46() SetSequence of X;
coherence
for b₁ being SetSequence of X st b₁ = inferior_setsequence A holds
b₁ is non-descending by Th23;

end;

registration

let X be set ;
let A be SetSequence of X;
cluster superior_setsequence A -> V45() SetSequence of X;
coherence
for b₁ being SetSequence of X st b₁ = superior_setsequence A holds
b₁ 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 non-descending 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 non-descending 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 non-descending 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 non-descending 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 non-descending 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 non-descending 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 non-descending 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 non-ascending 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 non-ascending 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 non-ascending 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 non-ascending 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 non-ascending 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 non-ascending 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 non-ascending 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 b₁ being Element of bool X holds
( b₁ = lim_inf B iff b₁ = 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 b₁ being Element of bool X holds
( b₁ = lim_sup B iff b₁ = 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 non-descending 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 non-descending 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 non-ascending 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 non-ascending 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 non-descending 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 non-ascending 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

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

:: deftheorem SETLIM_1:def 6 :
canceled;

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;

definition

let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
func @Complement S -> SetSequence of Si equals :: SETLIM_1:def 7
Complement S;
coherence
Complement S is SetSequence of Si

proof end;

end;

:: deftheorem defines @Complement SETLIM_1:def 7 :
for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds @Complement S = Complement S;

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 non-descending 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 non-descending 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 non-descending 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 non-ascending 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 non-ascending 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 non-ascending 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;