:: Some Equations Related to the Limit of Sequence of Subsets
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received May 24, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

theorem Th1: :: SETLIM_2:1
for n being Element of NAT
for X being set
for A1 being SetSequence of X holds (inferior_setsequence A1) . n = Intersection (A1 ^\ n)
proofend;

theorem Th2: :: SETLIM_2:2
for n being Element of NAT
for X being set
for A1 being SetSequence of X holds (superior_setsequence A1) . n = Union (A1 ^\ n)
proofend;

definition
let X be set ;
let A1, A2 be SetSequence of X;
funcA1 (/\) A2 ->  SetSequence of X means :Def1: :: SETLIM_2:def 1
 for n being Element of NAT holds it . n = (A1 . n) /\ (A2 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n)
proofend;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) /\ (A2 . n) ) holds
b1 = b2
proofend;
commutativity
 for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) /\ (A1 . n) ;
funcA1 (\/) A2 ->  SetSequence of X means :Def2: :: SETLIM_2:def 2
 for n being Element of NAT holds it . n = (A1 . n) \/ (A2 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n)
proofend;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \/ (A2 . n) ) holds
b1 = b2
proofend;
commutativity
 for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) \/ (A1 . n) ;
funcA1 (\) A2 ->  SetSequence of X means :Def3: :: SETLIM_2:def 3
 for n being Element of NAT holds it . n = (A1 . n) \ (A2 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \ (A2 . n)
proofend;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \ (A2 . n) ) holds
b1 = b2
proofend;
funcA1 (\+\) A2 ->  SetSequence of X means :Def4: :: SETLIM_2:def 4
 for n being Element of NAT holds it . n = (A1 . n) \+\ (A2 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n)
proofend;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \+\ (A2 . n) ) holds
b1 = b2
proofend;
commutativity
 for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) \+\ (A1 . n) ;
end;

:: deftheorem Def1 defines (/\) SETLIM_2:def_1_:_
 for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (/\) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) /\ (A2 . n) );

:: deftheorem Def2 defines (\/) SETLIM_2:def_2_:_
 for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (\/) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) \/ (A2 . n) );

:: deftheorem Def3 defines (\) SETLIM_2:def_3_:_
 for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (\) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) \ (A2 . n) );

:: deftheorem Def4 defines (\+\) SETLIM_2:def_4_:_
 for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (\+\) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) \+\ (A2 . n) );

theorem Th3: :: SETLIM_2:3
for X being set
for A1, A2 being SetSequence of X holds A1 (\+\) A2 = (A1 (\) A2) (\/) (A2 (\) A1)
proofend;

theorem Th4: :: SETLIM_2:4
for k being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (A1 (/\) A2) ^\ k = (A1 ^\ k) (/\) (A2 ^\ k)
proofend;

theorem Th5: :: SETLIM_2:5
for k being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (A1 (\/) A2) ^\ k = (A1 ^\ k) (\/) (A2 ^\ k)
proofend;

theorem Th6: :: SETLIM_2:6
for k being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (A1 (\) A2) ^\ k = (A1 ^\ k) (\) (A2 ^\ k)
proofend;

theorem Th7: :: SETLIM_2:7
for k being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (A1 (\+\) A2) ^\ k = (A1 ^\ k) (\+\) (A2 ^\ k)
proofend;

theorem Th8: :: SETLIM_2:8
for X being set
for A1, A2 being SetSequence of X holds Union (A1 (/\) A2) c= (Union A1) /\ (Union A2)
proofend;

theorem Th9: :: SETLIM_2:9
for X being set
for A1, A2 being SetSequence of X holds Union (A1 (\/) A2) = (Union A1) \/ (Union A2)
proofend;

theorem Th10: :: SETLIM_2:10
for X being set
for A1, A2 being SetSequence of X holds (Union A1) \ (Union A2) c= Union (A1 (\) A2)
proofend;

theorem Th11: :: SETLIM_2:11
for X being set
for A1, A2 being SetSequence of X holds (Union A1) \+\ (Union A2) c= Union (A1 (\+\) A2)
proofend;

theorem Th12: :: SETLIM_2:12
for X being set
for A1, A2 being SetSequence of X holds Intersection (A1 (/\) A2) = (Intersection A1) /\ (Intersection A2)
proofend;

theorem Th13: :: SETLIM_2:13
for X being set
for A1, A2 being SetSequence of X holds (Intersection A1) \/ (Intersection A2) c= Intersection (A1 (\/) A2)
proofend;

theorem Th14: :: SETLIM_2:14
for X being set
for A1, A2 being SetSequence of X holds Intersection (A1 (\) A2) c= (Intersection A1) \ (Intersection A2)
proofend;

definition
let X be set ;
let A1 be SetSequence of X;
let A be Subset of X;
funcA (/\) A1 ->  SetSequence of X means :Def5: :: SETLIM_2:def 5
 for n being Element of NAT holds it . n = A /\ (A1 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A /\ (A1 . n)
proofend;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = A /\ (A1 . n) ) & ( for n being Element of NAT holds b2 . n = A /\ (A1 . n) ) holds
b1 = b2
proofend;
funcA (\/) A1 ->  SetSequence of X means :Def6: :: SETLIM_2:def 6
 for n being Element of NAT holds it . n = A \/ (A1 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A \/ (A1 . n)
proofend;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = A \/ (A1 . n) ) & ( for n being Element of NAT holds b2 . n = A \/ (A1 . n) ) holds
b1 = b2
proofend;
funcA (\) A1 ->  SetSequence of X means :Def7: :: SETLIM_2:def 7
 for n being Element of NAT holds it . n = A \ (A1 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A \ (A1 . n)
proofend;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = A \ (A1 . n) ) & ( for n being Element of NAT holds b2 . n = A \ (A1 . n) ) holds
b1 = b2
proofend;
funcA1 (\) A ->  SetSequence of X means :Def8: :: SETLIM_2:def 8
 for n being Element of NAT holds it . n = (A1 . n) \ A;
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \ A
proofend;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \ A ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \ A ) holds
b1 = b2
proofend;
funcA (\+\) A1 ->  SetSequence of X means :Def9: :: SETLIM_2:def 9
 for n being Element of NAT holds it . n = A \+\ (A1 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A \+\ (A1 . n)
proofend;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = A \+\ (A1 . n) ) & ( for n being Element of NAT holds b2 . n = A \+\ (A1 . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines (/\) SETLIM_2:def_5_:_
 for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (/\) A1 iff for n being Element of NAT holds b4 . n = A /\ (A1 . n) );

:: deftheorem Def6 defines (\/) SETLIM_2:def_6_:_
 for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (\/) A1 iff for n being Element of NAT holds b4 . n = A \/ (A1 . n) );

:: deftheorem Def7 defines (\) SETLIM_2:def_7_:_
 for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (\) A1 iff for n being Element of NAT holds b4 . n = A \ (A1 . n) );

:: deftheorem Def8 defines (\) SETLIM_2:def_8_:_
 for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A1 (\) A iff for n being Element of NAT holds b4 . n = (A1 . n) \ A );

:: deftheorem Def9 defines (\+\) SETLIM_2:def_9_:_
 for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (\+\) A1 iff for n being Element of NAT holds b4 . n = A \+\ (A1 . n) );

theorem :: SETLIM_2:15
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A)
proofend;

theorem Th16: :: SETLIM_2:16
for k being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (/\) A1) ^\ k = A (/\) (A1 ^\ k)
proofend;

theorem Th17: :: SETLIM_2:17
for k being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\/) A1) ^\ k = A (\/) (A1 ^\ k)
proofend;

theorem Th18: :: SETLIM_2:18
for k being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\) A1) ^\ k = A (\) (A1 ^\ k)
proofend;

theorem Th19: :: SETLIM_2:19
for k being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A1 (\) A) ^\ k = (A1 ^\ k) (\) A
proofend;

theorem Th20: :: SETLIM_2:20
for k being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)
proofend;

theorem Th21: :: SETLIM_2:21
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A (/\) A1 is non-ascending
proofend;

theorem Th22: :: SETLIM_2:22
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A (/\) A1 is non-descending
proofend;

theorem :: SETLIM_2:23
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A (/\) A1 is monotone
proofend;

theorem Th24: :: SETLIM_2:24
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A (\/) A1 is non-ascending
proofend;

theorem Th25: :: SETLIM_2:25
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A (\/) A1 is non-descending
proofend;

theorem :: SETLIM_2:26
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A (\/) A1 is monotone
proofend;

theorem Th27: :: SETLIM_2:27
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A (\) A1 is non-descending
proofend;

theorem Th28: :: SETLIM_2:28
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A (\) A1 is non-ascending
proofend;

theorem :: SETLIM_2:29
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A (\) A1 is monotone
proofend;

theorem Th30: :: SETLIM_2:30
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A1 (\) A is non-ascending
proofend;

theorem Th31: :: SETLIM_2:31
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A1 (\) A is non-descending
proofend;

theorem :: SETLIM_2:32
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A1 (\) A is monotone
proofend;

theorem Th33: :: SETLIM_2:33
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (/\) A1) = A /\ (Intersection A1)
proofend;

theorem Th34: :: SETLIM_2:34
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\/) A1) = A \/ (Intersection A1)
proofend;

theorem Th35: :: SETLIM_2:35
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\) A1) c= A \ (Intersection A1)
proofend;

theorem Th36: :: SETLIM_2:36
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Intersection (A1 (\) A) = (Intersection A1) \ A
proofend;

theorem Th37: :: SETLIM_2:37
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\+\) A1) c= A \+\ (Intersection A1)
proofend;

theorem Th38: :: SETLIM_2:38
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Union (A (/\) A1) = A /\ (Union A1)
proofend;

theorem Th39: :: SETLIM_2:39
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Union (A (\/) A1) = A \/ (Union A1)
proofend;

theorem Th40: :: SETLIM_2:40
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \ (Union A1) c= Union (A (\) A1)
proofend;

theorem Th41: :: SETLIM_2:41
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Union (A1 (\) A) = (Union A1) \ A
proofend;

theorem Th42: :: SETLIM_2:42
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \+\ (Union A1) c= Union (A (\+\) A1)
proofend;

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

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

theorem :: SETLIM_2:45
for n being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ ((inferior_setsequence A2) . n)
proofend;

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

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

theorem :: SETLIM_2:48
for n being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\) A2)) . n
proofend;

theorem :: SETLIM_2:49
for n being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n
proofend;

theorem Th50: :: SETLIM_2:50
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (/\) A1)) . n = A /\ ((inferior_setsequence A1) . n)
proofend;

theorem Th51: :: SETLIM_2:51
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\/) A1)) . n = A \/ ((inferior_setsequence A1) . n)
proofend;

theorem :: SETLIM_2:52
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\) A1)) . n c= A \ ((inferior_setsequence A1) . n)
proofend;

theorem Th53: :: SETLIM_2:53
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A
proofend;

theorem :: SETLIM_2:54
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\+\) A1)) . n c= A \+\ ((inferior_setsequence A1) . n)
proofend;

theorem Th55: :: SETLIM_2:55
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n)
proofend;

theorem Th56: :: SETLIM_2:56
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A (\/) A1)) . n = A \/ ((superior_setsequence A1) . n)
proofend;

theorem :: SETLIM_2:57
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n
proofend;

theorem Th58: :: SETLIM_2:58
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A
proofend;

theorem :: SETLIM_2:59
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n
proofend;

theorem Th60: :: SETLIM_2:60
for X being set
for A1, A2 being SetSequence of X holds lim_inf (A1 (/\) A2) = (lim_inf A1) /\ (lim_inf A2)
proofend;

theorem Th61: :: SETLIM_2:61
for X being set
for A1, A2 being SetSequence of X holds (lim_inf A1) \/ (lim_inf A2) c= lim_inf (A1 (\/) A2)
proofend;

theorem Th62: :: SETLIM_2:62
for X being set
for A1, A2 being SetSequence of X holds lim_inf (A1 (\) A2) c= (lim_inf A1) \ (lim_inf A2)
proofend;

theorem Th63: :: SETLIM_2:63
for X being set
for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)
proofend;

theorem Th64: :: SETLIM_2:64
for X being set
for A2, A1 being SetSequence of X st A2 is convergent holds
lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2)
proofend;

theorem Th65: :: SETLIM_2:65
for X being set
for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)
proofend;

theorem Th66: :: SETLIM_2:66
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
lim_inf (A1 (\+\) A2) = (lim_inf A1) \+\ (lim_inf A2)
proofend;

theorem Th67: :: SETLIM_2:67
for X being set
for A1, A2 being SetSequence of X holds lim_sup (A1 (/\) A2) c= (lim_sup A1) /\ (lim_sup A2)
proofend;

theorem Th68: :: SETLIM_2:68
for X being set
for A1, A2 being SetSequence of X holds lim_sup (A1 (\/) A2) = (lim_sup A1) \/ (lim_sup A2)
proofend;

theorem Th69: :: SETLIM_2:69
for X being set
for A1, A2 being SetSequence of X holds (lim_sup A1) \ (lim_sup A2) c= lim_sup (A1 (\) A2)
proofend;

theorem :: SETLIM_2:70
for X being set
for A1, A2 being SetSequence of X holds (lim_sup A1) \+\ (lim_sup A2) c= lim_sup (A1 (\+\) A2)
proofend;

theorem Th71: :: SETLIM_2:71
for X being set
for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)
proofend;

theorem Th72: :: SETLIM_2:72
for X being set
for A2, A1 being SetSequence of X st A2 is convergent holds
lim_sup (A1 (\) A2) = (lim_sup A1) \ (lim_sup A2)
proofend;

theorem Th73: :: SETLIM_2:73
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
lim_sup (A1 (\+\) A2) = (lim_sup A1) \+\ (lim_sup A2)
proofend;

theorem Th74: :: SETLIM_2:74
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (/\) A1) = A /\ (lim_inf A1)
proofend;

theorem Th75: :: SETLIM_2:75
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\/) A1) = A \/ (lim_inf A1)
proofend;

theorem Th76: :: SETLIM_2:76
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\) A1) c= A \ (lim_inf A1)
proofend;

theorem Th77: :: SETLIM_2:77
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A1 (\) A) = (lim_inf A1) \ A
proofend;

theorem Th78: :: SETLIM_2:78
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\+\) A1) c= A \+\ (lim_inf A1)
proofend;

theorem Th79: :: SETLIM_2:79
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_inf (A (\) A1) = A \ (lim_inf A1)
proofend;

theorem Th80: :: SETLIM_2:80
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_inf (A (\+\) A1) = A \+\ (lim_inf A1)
proofend;

theorem Th81: :: SETLIM_2:81
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_sup (A (/\) A1) = A /\ (lim_sup A1)
proofend;

theorem Th82: :: SETLIM_2:82
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_sup (A (\/) A1) = A \/ (lim_sup A1)
proofend;

theorem Th83: :: SETLIM_2:83
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \ (lim_sup A1) c= lim_sup (A (\) A1)
proofend;

theorem Th84: :: SETLIM_2:84
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_sup (A1 (\) A) = (lim_sup A1) \ A
proofend;

theorem Th85: :: SETLIM_2:85
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1)
proofend;

theorem Th86: :: SETLIM_2:86
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_sup (A (\) A1) = A \ (lim_sup A1)
proofend;

theorem Th87: :: SETLIM_2:87
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_sup (A (\+\) A1) = A \+\ (lim_sup A1)
proofend;

theorem :: SETLIM_2:88
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (/\) A2 is convergent & lim (A1 (/\) A2) = (lim A1) /\ (lim A2) )
proofend;

theorem :: SETLIM_2:89
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (\/) A2 is convergent & lim (A1 (\/) A2) = (lim A1) \/ (lim A2) )
proofend;

theorem :: SETLIM_2:90
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (\) A2 is convergent & lim (A1 (\) A2) = (lim A1) \ (lim A2) )
proofend;

theorem :: SETLIM_2:91
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (\+\) A2 is convergent & lim (A1 (\+\) A2) = (lim A1) \+\ (lim A2) )
proofend;

theorem :: SETLIM_2:92
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (/\) A1 is convergent & lim (A (/\) A1) = A /\ (lim A1) )
proofend;

theorem :: SETLIM_2:93
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (\/) A1 is convergent & lim (A (\/) A1) = A \/ (lim A1) )
proofend;

theorem :: SETLIM_2:94
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (\) A1 is convergent & lim (A (\) A1) = A \ (lim A1) )
proofend;

theorem :: SETLIM_2:95
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A1 (\) A is convergent & lim (A1 (\) A) = (lim A1) \ A )
proofend;

theorem :: SETLIM_2:96
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) )
proofend;