SETLIM_2: Some Equations Related to the Limit of Sequence of Subsets

:: 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-2021 Association of Mizar Users

theorem Th1: :: SETLIM_2:1

for n being Nat
for X being set
for A1 being SetSequence of X holds (inferior_setsequence A1) . n = Intersection (A1 ^\ n)

proof end;

theorem Th2: :: SETLIM_2:2

for n being Nat
for X being set
for A1 being SetSequence of X holds (superior_setsequence A1) . n = Union (A1 ^\ n)

proof end;

definition

let X be set ;
let A1, A2 be SetSequence of X;

func A1 (/\) A2 -> SetSequence of X means :Def1: :: SETLIM_2:def 1
for n being Nat holds it . n = (A1 . n) /\ (A2 . n);

existence

proof end;

uniqueness

proof end;

commutativity ;

func A1 (\/) A2 -> SetSequence of X means :Def2: :: SETLIM_2:def 2
for n being Nat holds it . n = (A1 . n) \/ (A2 . n);

existence

proof end;

uniqueness

proof end;

commutativity ;

func A1 (\) A2 -> SetSequence of X means :Def3: :: SETLIM_2:def 3
for n being Nat holds it . n = (A1 . n) \ (A2 . n);

existence

proof end;

uniqueness

proof end;

func A1 (\+\) A2 -> SetSequence of X means :Def4: :: SETLIM_2:def 4
for n being Nat holds it . n = (A1 . n) \+\ (A2 . n);

existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def1 defines (/\) SETLIM_2:def 1 :

:: deftheorem Def2 defines (\/) SETLIM_2:def 2 :

:: deftheorem Def3 defines (\) SETLIM_2:def 3 :

:: deftheorem Def4 defines (\+\) SETLIM_2:def 4 :

theorem Th3: :: SETLIM_2:3

for X being set
for A1, A2 being SetSequence of X holds A1 (\+\) A2 = (A1 (\) A2) (\/) (A2 (\) A1)

proof end;

theorem Th4: :: SETLIM_2:4

for k being Nat
for X being set
for A1, A2 being SetSequence of X holds (A1 (/\) A2) ^\ k = (A1 ^\ k) (/\) (A2 ^\ k)

proof end;

theorem Th5: :: SETLIM_2:5

for k being Nat
for X being set
for A1, A2 being SetSequence of X holds (A1 (\/) A2) ^\ k = (A1 ^\ k) (\/) (A2 ^\ k)

proof end;

theorem Th6: :: SETLIM_2:6

for k being Nat
for X being set
for A1, A2 being SetSequence of X holds (A1 (\) A2) ^\ k = (A1 ^\ k) (\) (A2 ^\ k)

proof end;

theorem Th7: :: SETLIM_2:7

for k being Nat
for X being set
for A1, A2 being SetSequence of X holds (A1 (\+\) A2) ^\ k = (A1 ^\ k) (\+\) (A2 ^\ k)

proof end;

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)

proof end;

theorem Th9: :: SETLIM_2:9

for X being set
for A1, A2 being SetSequence of X holds Union (A1 (\/) A2) = (Union A1) \/ (Union A2)

proof end;

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)

proof end;

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)

proof end;

theorem Th12: :: SETLIM_2:12

for X being set
for A1, A2 being SetSequence of X holds Intersection (A1 (/\) A2) = (Intersection A1) /\ (Intersection A2)

proof end;

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)

proof end;

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)

proof end;

definition

let X be set ;
let A1 be SetSequence of X;
let A be Subset of X;

func A (/\) A1 -> SetSequence of X means :Def5: :: SETLIM_2:def 5
for n being Nat holds it . n = A /\ (A1 . n);

existence

proof end;

uniqueness

proof end;

func A (\/) A1 -> SetSequence of X means :Def6: :: SETLIM_2:def 6
for n being Nat holds it . n = A \/ (A1 . n);

existence

proof end;

uniqueness

proof end;

func A (\) A1 -> SetSequence of X means :Def7: :: SETLIM_2:def 7
for n being Nat holds it . n = A \ (A1 . n);

existence

proof end;

uniqueness

proof end;

func A1 (\) A -> SetSequence of X means :Def8: :: SETLIM_2:def 8
for n being Nat holds it . n = (A1 . n) \ A;

existence

proof end;

uniqueness

proof end;

func A (\+\) A1 -> SetSequence of X means :Def9: :: SETLIM_2:def 9
for n being Nat holds it . n = A \+\ (A1 . n);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines (/\) SETLIM_2:def 5 :

:: deftheorem Def6 defines (\/) SETLIM_2:def 6 :

:: deftheorem Def7 defines (\) SETLIM_2:def 7 :

:: deftheorem Def8 defines (\) SETLIM_2:def 8 :

:: deftheorem Def9 defines (\+\) SETLIM_2:def 9 :

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)

proof end;

theorem Th16: :: SETLIM_2:16

for k being Nat
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (/\) A1) ^\ k = A (/\) (A1 ^\ k)

proof end;

theorem Th17: :: SETLIM_2:17

for k being Nat
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\/) A1) ^\ k = A (\/) (A1 ^\ k)

proof end;

theorem Th18: :: SETLIM_2:18

for k being Nat
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\) A1) ^\ k = A (\) (A1 ^\ k)

proof end;

theorem Th19: :: SETLIM_2:19

for k being Nat
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A1 (\) A) ^\ k = (A1 ^\ k) (\) A

proof end;

theorem Th20: :: SETLIM_2:20

for k being Nat
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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)

proof end;

theorem :: SETLIM_2:43

for n being 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)

proof end;

theorem :: SETLIM_2:44

for n being 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

proof end;

theorem :: SETLIM_2:45

for n being 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)

proof end;

theorem :: SETLIM_2:46

for n being 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)

proof end;

theorem :: SETLIM_2:47

for n being 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)

proof end;

theorem :: SETLIM_2:48

for n being 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

proof end;

theorem :: SETLIM_2:49

for n being 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

proof end;

theorem Th50: :: SETLIM_2:50

for n being 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)

proof end;

theorem Th51: :: SETLIM_2:51

for n being 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)

proof end;

theorem :: SETLIM_2:52

for n being 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)

proof end;

theorem Th53: :: SETLIM_2:53

for n being 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

proof end;

theorem :: SETLIM_2:54

for n being 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)

proof end;

theorem Th55: :: SETLIM_2:55

for n being 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)

proof end;

theorem Th56: :: SETLIM_2:56

for n being 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)

proof end;

theorem :: SETLIM_2:57

for n being 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

proof end;

theorem Th58: :: SETLIM_2:58

for n being 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

proof end;

theorem :: SETLIM_2:59

for n being 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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

theorem Th64: :: SETLIM_2:64

for X being set
for A1, A2 being SetSequence of X st A2 is convergent holds
lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

theorem Th72: :: SETLIM_2:72

for X being set
for A1, A2 being SetSequence of X st A2 is convergent holds
lim_sup (A1 (\) A2) = (lim_sup A1) \ (lim_sup A2)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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

proof end;