:: 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 }

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)}

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 )

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 )

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 }

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 }

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 )

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

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

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;

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

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

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

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)

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;

:: 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() ) );

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;

ex b_{1} being Function st

( dom b_{1} = NAT & ( for n being Element of NAT holds b_{1} . n = meet { (B . k) where k is Element of NAT : n <= k } ) )

for b_{1}, b_{2} being Function st dom b_{1} = NAT & ( for n being Element of NAT holds b_{1} . n = meet { (B . k) where k is Element of NAT : n <= k } ) & dom b_{2} = NAT & ( for n being Element of NAT holds b_{2} . n = meet { (B . k) where k is Element of NAT : n <= k } ) holds

b_{1} = b_{2}

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

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines inferior_setsequence SETLIM_1:def 2 :

for B, b_{2} being Function holds

( b_{2} = inferior_setsequence B iff ( dom b_{2} = NAT & ( for n being Element of NAT holds b_{2} . n = meet { (B . k) where k is Element of NAT : n <= k } ) ) );

for B, b

( b

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

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

definition

let B be Function;

ex b_{1} being Function st

( dom b_{1} = NAT & ( for n being Element of NAT holds b_{1} . n = union { (B . k) where k is Element of NAT : n <= k } ) )

for b_{1}, b_{2} being Function st dom b_{1} = NAT & ( for n being Element of NAT holds b_{1} . n = union { (B . k) where k is Element of NAT : n <= k } ) & dom b_{2} = NAT & ( for n being Element of NAT holds b_{2} . n = union { (B . k) where k is Element of NAT : n <= k } ) holds

b_{1} = b_{2}

end;
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 ( dom it = NAT & ( for n being Element of NAT holds it . n = union { (B . k) where k is Element of NAT : n <= k } ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines superior_setsequence SETLIM_1:def 3 :

for B, b_{2} being Function holds

( b_{2} = superior_setsequence B iff ( dom b_{2} = NAT & ( for n being Element of NAT holds b_{2} . n = union { (B . k) where k is Element of NAT : n <= k } ) ) );

for B, b

( b

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

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

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) )

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) )

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)

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)

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 :: SETLIM_1:25

for X being set

for B being SetSequence of X holds

( inferior_setsequence B is monotone & superior_setsequence B is monotone )

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;

coherence

for b_{1} being SetSequence of X st b_{1} = inferior_setsequence A holds

b_{1} is non-descending
by Th23;

end;
let A be SetSequence of X;

coherence

for b

b

registration

let X be set ;

let A be SetSequence of X;

coherence

for b_{1} being SetSequence of X st b_{1} = superior_setsequence A holds

b_{1} is non-ascending
by Th24;

end;
let A be SetSequence of X;

coherence

for b

b

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

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

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

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 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) `

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) `

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)

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)

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

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)

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)

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)

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

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

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)

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)

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

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

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)

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

for X being set

for B being SetSequence of X st B is V50() holds

(inferior_setsequence B) . n = B . n

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

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

for X being set

for B being SetSequence of X st B is V49() holds

(superior_setsequence B) . n = B . n

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

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)

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

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

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;

compatibility

for b_{1} being Element of bool X holds

( b_{1} = lim_inf B iff b_{1} = Union (inferior_setsequence B) )

end;
let B be SetSequence of X;

compatibility

for b

( b

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

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;

compatibility

for b_{1} being Element of bool X holds

( b_{1} = lim_sup B iff b_{1} = Intersection (superior_setsequence B) )

end;
let B be SetSequence of X;

compatibility

for b

( b

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

for X being set

for B being SetSequence of X holds lim_sup B = Intersection (superior_setsequence B);

theorem :: SETLIM_1:55

for X being set

for B being SetSequence of X holds lim_inf B = lim (inferior_setsequence B) by Th43;

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;

for B being SetSequence of X holds lim_sup B = lim (superior_setsequence B) by Th49;

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 )

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

theorem :: SETLIM_1:60

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;

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;

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 )

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 )

for B being SetSequence of X st B is V49() holds

( B is convergent & lim B = Intersection B )

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

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

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

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

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) )

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) )

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

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

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

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)) `

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)) `

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

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)

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)

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)

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 )

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;

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;

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 )

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;

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;

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 )

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

for Si being SigmaField of X

for S being SetSequence of Si st S is monotone holds

S is convergent

proof end;