:: SETLIM_1 semantic presentation

Lm1: for i, j being Nat holds
( not i <= j or i = j or i + 1 <= j )

proof end;

theorem Th1: :: SETLIM_1:1

for X, y being set st X <> {} & ( for x being set st x in X holds
x = y ) holds
union X = y

proof end;

theorem Th2: :: SETLIM_1:2

for X, y being set st X <> {} & ( for x being set st x in X holds
x = y ) holds
meet X = y

proof end;

theorem Th3: :: SETLIM_1:3

for Y being set
for f being Function of NAT ,Y
for n being Nat holds { (f . k) where k is Nat : n <= k } <> {}

proof end;

theorem Th4: :: SETLIM_1:4

for n, m being Nat
for Y being set
for f being Function of NAT ,Y holds f . (n + m) in { (f . k) where k is Nat : n <= k }

proof end;

theorem Th5: :: SETLIM_1:5

for n being Nat
for Y being set
for f being Function of NAT ,Y holds { (f . k1) where k1 is Nat : n <= k1 } = { (f . k2) where k2 is Nat : n + 1 <= k2 } \/ {(f . n)}

proof end;

theorem Th6: :: SETLIM_1:6

for n being Nat
for Y, x being set
for f being Function of NAT ,Y holds
( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds
x in Z )

proof end;

theorem Th7: :: SETLIM_1:7

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 Nat st x = f . n )

proof end;

theorem Th8: :: SETLIM_1:8

for X, Y being non empty set
for f being Function of X,Y holds
( rng f <> {} & f <> {} )

proof end;

theorem Th9: :: SETLIM_1:9

for Y being non empty set
for f being Function of NAT ,Y holds rng f = { (f . k) where k is Nat : 0 <= k }

proof end;

theorem Th10: :: SETLIM_1:10

for k being Nat
for Y being non empty set
for f being Function of NAT ,Y holds rng (f ^\ k) = { (f . n) where n is Nat : k <= n }

proof end;

theorem :: SETLIM_1:11

canceled;

theorem Th12: :: SETLIM_1:12

for X, x being set
for A1 being SetSequence of X holds
( x in meet (rng A1) iff for n being Nat holds x in A1 . n )

proof end;

theorem Th13: :: SETLIM_1:13

for X being set
for A1 being SetSequence of X holds Intersection A1 = meet (rng A1)

proof end;

theorem :: SETLIM_1:14

for X being set
for A1 being SetSequence of X holds Intersection A1 c= Union A1

proof end;

theorem Th15: :: SETLIM_1:15

for X being set
for A being Subset of X
for A1 being SetSequence of X st ( for n being Nat holds A1 . n = A ) holds
Union A1 = A

proof end;

theorem Th16: :: SETLIM_1:16

for X being set
for A being Subset of X
for A1 being SetSequence of X st ( for n being Nat holds A1 . n = A ) holds
Intersection A1 = A

proof end;

theorem :: SETLIM_1:17

for X being set
for A1 being SetSequence of X st A1 is constant holds
Union A1 = Intersection A1

proof end;

Lm2: for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is constant & the_value_of A1 = A holds
for n being Nat holds
( A1 . n = A & Union A1 = A & Intersection A1 = A )

proof end;

theorem Th18: :: SETLIM_1:18

for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is constant & the_value_of A1 = A holds
for n being Nat holds union { (A1 . k) where k is Nat : n <= k } = A

proof end;

theorem Th19: :: SETLIM_1:19

for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is constant & the_value_of A1 = A holds
for n being Nat holds meet { (A1 . k) where k is Nat : n <= k } = A

proof end;

theorem Th20: :: SETLIM_1:20

for X being set
for A1 being SetSequence of X ex f being Function of NAT , bool X st
for n being Nat
for Y being set st Y = { (A1 . k) where k is Nat : n <= k } holds
f . n = meet Y

proof end;

theorem Th21: :: SETLIM_1:21

for X being set
for A1 being SetSequence of X ex f being Function of NAT , bool X st
for n being Nat
for Y being set st Y = { (A1 . k) where k is Nat : n <= k } holds
f . n = union Y

proof end;

definition

let X be set ;
let A1 be SetSequence of X;
attr A1 is monotone means :Def1: :: SETLIM_1:def 1
( A1 is non-decreasing or A1 is non-increasing );

end;

:: deftheorem Def1 defines monotone SETLIM_1:def 1 :

definition

let X be set ;
let A1 be SetSequence of X;
func inferior_setsequence A1 -> SetSequence of X means :Def2: :: SETLIM_1:def 2
for n being Nat
for Y being set st Y = { (A1 . k) where k is Nat : n <= k } holds
it . n = meet Y;
existence by Th20;
uniqueness

proof end;

end;

:: deftheorem Def2 defines inferior_setsequence SETLIM_1:def 2 :

definition

let X be set ;
let A1 be SetSequence of X;
func superior_setsequence A1 -> SetSequence of X means :Def3: :: SETLIM_1:def 3
for n being Nat
for Y being set st Y = { (A1 . k) where k is Nat : n <= k } holds
it . n = union Y;
existence by Th21;
uniqueness

proof end;

end;

:: deftheorem Def3 defines superior_setsequence SETLIM_1:def 3 :

theorem Th22: :: SETLIM_1:22

for X being set
for A1 being SetSequence of X holds (inferior_setsequence A1) . 0 = Intersection A1

proof end;

theorem Th23: :: SETLIM_1:23

for X being set
for A1 being SetSequence of X holds (superior_setsequence A1) . 0 = Union A1

proof end;

theorem Th24: :: SETLIM_1:24

for n being Nat
for X, x being set
for A1 being SetSequence of X holds
( x in (inferior_setsequence A1) . n iff for k being Nat holds x in A1 . (n + k) )

proof end;

theorem Th25: :: SETLIM_1:25

for n being Nat
for X, x being set
for A1 being SetSequence of X holds
( x in (superior_setsequence A1) . n iff ex k being Nat st x in A1 . (n + k) )

proof end;

theorem Th26: :: SETLIM_1:26

for n being Nat
for X being set
for A1 being SetSequence of X holds (inferior_setsequence A1) . n = ((inferior_setsequence A1) . (n + 1)) /\ (A1 . n)

proof end;

theorem Th27: :: SETLIM_1:27

for n being Nat
for X being set
for A1 being SetSequence of X holds (superior_setsequence A1) . n = ((superior_setsequence A1) . (n + 1)) \/ (A1 . n)

proof end;

theorem Th28: :: SETLIM_1:28

for X being set
for A1 being SetSequence of X holds inferior_setsequence A1 is non-decreasing

proof end;

theorem Th29: :: SETLIM_1:29

for X being set
for A1 being SetSequence of X holds superior_setsequence A1 is non-increasing

proof end;

theorem :: SETLIM_1:30

for X being set
for A1 being SetSequence of X holds
( inferior_setsequence A1 is monotone & superior_setsequence A1 is monotone )

proof end;

registration

let X be set ;
let A be SetSequence of X;
cluster inferior_setsequence A -> non-decreasing ;
coherence by Th28;

end;

registration

let X be set ;
let A be SetSequence of X;
cluster superior_setsequence A -> non-increasing ;
coherence by Th29;

end;

theorem :: SETLIM_1:31

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

proof end;

theorem :: SETLIM_1:32

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

proof end;

theorem Th33: :: SETLIM_1:33

for X being set
for A1 being SetSequence of X
for n being Nat holds { (A1 . k) where k is Nat : n <= k } is Subset-Family of X

proof end;

theorem :: SETLIM_1:34

canceled;

theorem :: SETLIM_1:35

for X being set
for A1 being SetSequence of X holds Union A1 = (Intersection (Complement A1)) `

proof end;

theorem Th36: :: SETLIM_1:36

for n being Nat
for X being set
for A1 being SetSequence of X holds (inferior_setsequence A1) . n = ((superior_setsequence (Complement A1)) . n) `

proof end;

theorem :: SETLIM_1:37

for n being Nat
for X being set
for A1 being SetSequence of X holds (superior_setsequence A1) . n = ((inferior_setsequence (Complement A1)) . n) `

proof end;

theorem Th38: :: SETLIM_1:38

for X being set
for A1 being SetSequence of X holds Complement (inferior_setsequence A1) = superior_setsequence (Complement A1)

proof end;

theorem :: SETLIM_1:39

for X being set
for A1 being SetSequence of X holds Complement (superior_setsequence A1) = inferior_setsequence (Complement A1)

proof end;

theorem :: SETLIM_1:40

for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Nat holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n

proof end;

theorem :: SETLIM_1:41

for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Nat holds A3 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Nat holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)

proof end;

theorem :: SETLIM_1:42

for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Nat holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)

proof end;

theorem :: SETLIM_1:43

for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Nat holds A3 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Nat holds (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)

proof end;

theorem Th44: :: SETLIM_1:44

for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is constant & the_value_of A1 = A holds
for n being Nat holds (inferior_setsequence A1) . n = A

proof end;

theorem Th45: :: SETLIM_1:45

for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is constant & the_value_of A1 = A holds
for n being Nat holds (superior_setsequence A1) . n = A

proof end;

theorem Th46: :: SETLIM_1:46

for n being Nat
for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
A1 . n c= (superior_setsequence A1) . (n + 1)

proof end;

theorem Th47: :: SETLIM_1:47

for n being Nat
for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
(superior_setsequence A1) . n = (superior_setsequence A1) . (n + 1)

proof end;

theorem Th48: :: SETLIM_1:48

for n being Nat
for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
(superior_setsequence A1) . n = Union A1

proof end;

theorem Th49: :: SETLIM_1:49

for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
Intersection (superior_setsequence A1) = Union A1

proof end;

theorem Th50: :: SETLIM_1:50

for n being Nat
for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
A1 . n c= (inferior_setsequence A1) . (n + 1)

proof end;

theorem Th51: :: SETLIM_1:51

for n being Nat
for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
(inferior_setsequence A1) . n = A1 . n

proof end;

theorem Th52: :: SETLIM_1:52

for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
inferior_setsequence A1 = A1

proof end;

theorem Th53: :: SETLIM_1:53

for n being Nat
for X being set
for A1 being SetSequence of X st A1 is non-increasing holds
(superior_setsequence A1) . (n + 1) c= A1 . n

proof end;

theorem Th54: :: SETLIM_1:54

for n being Nat
for X being set
for A1 being SetSequence of X st A1 is non-increasing holds
(superior_setsequence A1) . n = A1 . n

proof end;

theorem Th55: :: SETLIM_1:55

for X being set
for A1 being SetSequence of X st A1 is non-increasing holds
superior_setsequence A1 = A1

proof end;

theorem Th56: :: SETLIM_1:56

for n being Nat
for X being set
for A1 being SetSequence of X st A1 is non-increasing holds
(inferior_setsequence A1) . (n + 1) c= A1 . n

proof end;

theorem Th57: :: SETLIM_1:57

for n being Nat
for X being set
for A1 being SetSequence of X st A1 is non-increasing holds
(inferior_setsequence A1) . n = (inferior_setsequence A1) . (n + 1)

proof end;

theorem Th58: :: SETLIM_1:58

for n being Nat
for X being set
for A1 being SetSequence of X st A1 is non-increasing holds
(inferior_setsequence A1) . n = Intersection A1

proof end;

theorem Th59: :: SETLIM_1:59

for X being set
for A1 being SetSequence of X st A1 is non-increasing holds
Union (inferior_setsequence A1) = Intersection A1

proof end;

definition

let X be set ;
let A1 be SetSequence of X;
redefine func lim_inf A1 equals :: SETLIM_1:def 4
Union (inferior_setsequence A1);
compatibility

proof end;

end;

:: deftheorem defines lim_inf SETLIM_1:def 4 :

definition

let X be set ;
let A1 be SetSequence of X;
redefine func lim_sup A1 equals :: SETLIM_1:def 5
Intersection (superior_setsequence A1);
compatibility

proof end;

end;

:: deftheorem defines lim_sup SETLIM_1:def 5 :

definition

let X be set ;
let A1 be SetSequence of X;
assume A1: A1 is convergent ;
func lim A1 -> Subset of X means :Def6: :: SETLIM_1:def 6
( it = lim_sup A1 & it = lim_inf A1 );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines lim SETLIM_1:def 6 :

theorem :: SETLIM_1:60

for X being set
for A1 being SetSequence of X holds Intersection A1 c= lim_inf A1

proof end;

theorem :: SETLIM_1:61

for X being set
for A1 being SetSequence of X holds lim_inf A1 = lim (inferior_setsequence A1)

proof end;

theorem :: SETLIM_1:62

for X being set
for A1 being SetSequence of X holds lim_sup A1 = lim (superior_setsequence A1)

proof end;

theorem :: SETLIM_1:63

for X being set
for A1 being SetSequence of X holds lim_sup A1 = (lim_inf (Complement A1)) `

proof end;

theorem Th64: :: SETLIM_1:64

for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is constant & the_value_of A1 = A holds
( A1 is convergent & lim A1 = A & lim_inf A1 = A & lim_sup A1 = A )

proof end;

theorem Th65: :: SETLIM_1:65

for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
lim_sup A1 = Union A1 by Th49;

theorem Th66: :: SETLIM_1:66

for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
lim_inf A1 = Union A1 by Th52;

theorem Th67: :: SETLIM_1:67

for X being set
for A1 being SetSequence of X st A1 is non-increasing holds
lim_sup A1 = Intersection A1 by Th55;

theorem Th68: :: SETLIM_1:68

for X being set
for A1 being SetSequence of X st A1 is non-increasing holds
lim_inf A1 = Intersection A1 by Th59;

theorem Th69: :: SETLIM_1:69

for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
( A1 is convergent & lim A1 = Union A1 )

proof end;

theorem Th70: :: SETLIM_1:70

for X being set
for A1 being SetSequence of X st A1 is non-increasing holds
( A1 is convergent & lim A1 = Intersection A1 )

proof end;

theorem :: SETLIM_1:71

for X being set
for A1 being SetSequence of X st A1 is monotone holds
A1 is convergent

proof end;

definition

let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
:: original: constant
redefine attr S is constant means :: SETLIM_1:def 7
ex A being Element of Si st
for n being Nat holds S . n = A;
compatibility

proof end;

end;

:: deftheorem defines constant SETLIM_1:def 7 :

definition

let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
func @inferior_setsequence S -> SetSequence of Si equals :: SETLIM_1:def 8
inferior_setsequence S;
coherence

proof end;

end;

:: deftheorem defines @inferior_setsequence SETLIM_1:def 8 :

definition

let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
func @superior_setsequence S -> SetSequence of Si equals :: SETLIM_1:def 9
superior_setsequence S;
coherence

proof end;

end;

:: deftheorem defines @superior_setsequence SETLIM_1:def 9 :

theorem :: SETLIM_1:72

for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds @superior_setsequence S is non-increasing ;

theorem :: SETLIM_1:73

for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds @inferior_setsequence S is non-decreasing ;

registration

let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
cluster @superior_setsequence S -> non-increasing ;
coherence ;

end;

registration

let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
cluster @inferior_setsequence S -> non-decreasing ;
coherence ;

end;

definition

let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
func lim_inf S -> Element of Si equals :: SETLIM_1:def 10
Union (@inferior_setsequence S);
coherence by PROB_1:46;

end;

:: deftheorem defines lim_inf SETLIM_1:def 10 :

definition

let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
func lim_sup S -> Element of Si equals :: SETLIM_1:def 11
Intersection (@superior_setsequence S);
coherence

proof end;

end;

:: deftheorem defines lim_sup SETLIM_1:def 11 :

definition

let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
attr S is convergent means :Def12: :: SETLIM_1:def 12
lim_sup S = lim_inf S;

end;

:: deftheorem Def12 defines convergent SETLIM_1:def 12 :

definition

let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
assume A1: S is convergent ;
func lim S -> Element of Si means :Def13: :: SETLIM_1:def 13
( it = lim_sup S & it = lim_inf S );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def13 defines lim SETLIM_1:def 13 :

theorem Th74: :: SETLIM_1:74

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 Nat ex k being Nat st x in S . (n + k) )

proof end;

theorem Th75: :: SETLIM_1:75

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 Nat st
for k being Nat holds x in S . (n + k) )

proof end;

theorem :: SETLIM_1:76

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

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

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 14
Complement S;
coherence

proof end;

end;

:: deftheorem defines @Complement SETLIM_1:def 14 :

theorem Th79: :: SETLIM_1:79

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

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

for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Nat holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
(lim_inf S1) \/ (lim_inf S2) c= lim_inf S3

proof end;

theorem :: SETLIM_1:82

for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Nat holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_inf S3 = (lim_inf S1) /\ (lim_inf S2)

proof end;

theorem :: SETLIM_1:83

for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Nat holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
lim_sup S3 = (lim_sup S1) \/ (lim_sup S2)

proof end;

theorem :: SETLIM_1:84

for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Nat holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2)

proof end;

theorem :: SETLIM_1:85

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 Th86: :: SETLIM_1:86

for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is non-decreasing holds
lim_sup S = Union S

proof end;

theorem Th87: :: SETLIM_1:87

for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is non-decreasing holds
lim_inf S = Union S

proof end;

theorem Th88: :: SETLIM_1:88

for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is non-decreasing holds
( S is convergent & lim S = Union S )

proof end;

theorem Th89: :: SETLIM_1:89

for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is non-increasing holds
lim_sup S = Intersection S

proof end;

theorem Th90: :: SETLIM_1:90

for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is non-increasing holds
lim_inf S = Intersection S

proof end;

theorem Th91: :: SETLIM_1:91

for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is non-increasing holds
( S is convergent & lim S = Intersection S )

proof end;

theorem :: SETLIM_1:92

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;