:: SETLIM_1 semantic presentation

Lemma1: for b₁, b₂ being Nat holds
( not b₁ <= b₂ or b₁ = b₂ or b₁ + 1 <= b₂ )

proof end;

theorem Th1: :: SETLIM_1:1

for b₁, b₂ being set st b₁ <> {} & ( for b₃ being set st b₃ in b₁ holds
b₃ = b₂ ) holds
union b₁ = b₂

proof end;

theorem Th2: :: SETLIM_1:2

for b₁, b₂ being set st b₁ <> {} & ( for b₃ being set st b₃ in b₁ holds
b₃ = b₂ ) holds
meet b₁ = b₂

proof end;

theorem Th3: :: SETLIM_1:3

for b₁ being set
for b₂ being Function of NAT ,b₁
for b₃ being Nat holds { (b₂ . b₄) where B is Nat : b₃ <= b₄ } <> {}

proof end;

theorem Th4: :: SETLIM_1:4

for b₁, b₂ being Nat
for b₃ being set
for b₄ being Function of NAT ,b₃ holds b₄ . (b₁ + b₂) in { (b₄ . b₅) where B is Nat : b₁ <= b₅ }

proof end;

theorem Th5: :: SETLIM_1:5

for b₁ being Nat
for b₂ being set
for b₃ being Function of NAT ,b₂ holds { (b₃ . b₄) where B is Nat : b₁ <= b₄ } = { (b₃ . b₄) where B is Nat : b₁ + 1 <= b₄ } \/ {(b₃ . b₁)}

proof end;

theorem Th6: :: SETLIM_1:6

for b₁ being Nat
for b₂, b₃ being set
for b₄ being Function of NAT ,b₂ holds
( ( for b₅ being Nat holds b₃ in b₄ . (b₁ + b₅) ) iff for b₅ being set st b₅ in { (b₄ . b₆) where B is Nat : b₁ <= b₆ } holds
b₃ in b₅ )

proof end;

theorem Th7: :: SETLIM_1:7

for b₁ being set
for b₂ being non empty set
for b₃ being Function of NAT ,b₂ holds
( b₁ in rng b₃ iff ex b₄ being Nat st b₁ = b₃ . b₄ )

proof end;

theorem Th8: :: SETLIM_1:8

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂ holds
( rng b₃ <> {} & b₃ <> {} )

proof end;

theorem Th9: :: SETLIM_1:9

for b₁ being non empty set
for b₂ being Function of NAT ,b₁ holds rng b₂ = { (b₂ . b₃) where B is Nat : 0 <= b₃ }

proof end;

theorem Th10: :: SETLIM_1:10

for b₁ being Nat
for b₂ being non empty set
for b₃ being Function of NAT ,b₂ holds rng (b₃ ^\ b₁) = { (b₃ . b₄) where B is Nat : b₁ <= b₄ }

proof end;

theorem Th11: :: SETLIM_1:11

canceled;

theorem Th12: :: SETLIM_1:12

for b₁, b₂ being set
for b₃ being SetSequence of b₁ holds
( b₂ in meet (rng b₃) iff for b₄ being Nat holds b₂ in b₃ . b₄ )

proof end;

theorem Th13: :: SETLIM_1:13

for b₁ being set
for b₂ being SetSequence of b₁ holds Intersection b₂ = meet (rng b₂)

proof end;

theorem Th14: :: SETLIM_1:14

for b₁ being set
for b₂ being SetSequence of b₁ holds Intersection b₂ c= Union b₂

proof end;

theorem Th15: :: SETLIM_1:15

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st ( for b₄ being Nat holds b₃ . b₄ = b₂ ) holds
Union b₃ = b₂

proof end;

theorem Th16: :: SETLIM_1:16

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st ( for b₄ being Nat holds b₃ . b₄ = b₂ ) holds
Intersection b₃ = b₂

proof end;

theorem Th17: :: SETLIM_1:17

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is constant holds
Union b₂ = Intersection b₂

proof end;

Lemma16: for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is constant & the_value_of b₃ = b₂ holds
for b₄ being Nat holds
( b₃ . b₄ = b₂ & Union b₃ = b₂ & Intersection b₃ = b₂ )

proof end;

theorem Th18: :: SETLIM_1:18

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is constant & the_value_of b₃ = b₂ holds
for b₄ being Nat holds union { (b₃ . b₅) where B is Nat : b₄ <= b₅ } = b₂

proof end;

theorem Th19: :: SETLIM_1:19

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is constant & the_value_of b₃ = b₂ holds
for b₄ being Nat holds meet { (b₃ . b₅) where B is Nat : b₄ <= b₅ } = b₂

proof end;

theorem Th20: :: SETLIM_1:20

for b₁ being set
for b₂ being SetSequence of b₁ ex b₃ being Function of NAT , bool b₁ st
for b₄ being Nat
for b₅ being set st b₅ = { (b₂ . b₆) where B is Nat : b₄ <= b₆ } holds
b₃ . b₄ = meet b₅

proof end;

theorem Th21: :: SETLIM_1:21

for b₁ being set
for b₂ being SetSequence of b₁ ex b₃ being Function of NAT , bool b₁ st
for b₄ being Nat
for b₅ being set st b₅ = { (b₂ . b₆) where B is Nat : b₄ <= b₆ } holds
b₃ . b₄ = union b₅

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
attr a₂ is monotone means :Def1: :: SETLIM_1:def 1
( a₂ is non-decreasing or a₂ is non-increasing );

end;

:: deftheorem Def1 defines monotone SETLIM_1:def 1 :

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
func inferior_setsequence c₂ -> SetSequence of a₁ means :Def2: :: SETLIM_1:def 2
for b₁ being Nat
for b₂ being set st b₂ = { (a₂ . b₃) where B is Nat : b₁ <= b₃ } holds
a₃ . b₁ = meet b₂;
existence by Th20;
uniqueness

proof end;

end;

:: deftheorem Def2 defines inferior_setsequence SETLIM_1:def 2 :

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
func superior_setsequence c₂ -> SetSequence of a₁ means :Def3: :: SETLIM_1:def 3
for b₁ being Nat
for b₂ being set st b₂ = { (a₂ . b₃) where B is Nat : b₁ <= b₃ } holds
a₃ . b₁ = union b₂;
existence by Th21;
uniqueness

proof end;

end;

:: deftheorem Def3 defines superior_setsequence SETLIM_1:def 3 :

theorem Th22: :: SETLIM_1:22

for b₁ being set
for b₂ being SetSequence of b₁ holds (inferior_setsequence b₂) . 0 = Intersection b₂

proof end;

theorem Th23: :: SETLIM_1:23

for b₁ being set
for b₂ being SetSequence of b₁ holds (superior_setsequence b₂) . 0 = Union b₂

proof end;

theorem Th24: :: SETLIM_1:24

for b₁ being Nat
for b₂, b₃ being set
for b₄ being SetSequence of b₂ holds
( b₃ in (inferior_setsequence b₄) . b₁ iff for b₅ being Nat holds b₃ in b₄ . (b₁ + b₅) )

proof end;

theorem Th25: :: SETLIM_1:25

for b₁ being Nat
for b₂, b₃ being set
for b₄ being SetSequence of b₂ holds
( b₃ in (superior_setsequence b₄) . b₁ iff ex b₅ being Nat st b₃ in b₄ . (b₁ + b₅) )

proof end;

theorem Th26: :: SETLIM_1:26

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds (inferior_setsequence b₃) . b₁ = ((inferior_setsequence b₃) . (b₁ + 1)) /\ (b₃ . b₁)

proof end;

theorem Th27: :: SETLIM_1:27

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds (superior_setsequence b₃) . b₁ = ((superior_setsequence b₃) . (b₁ + 1)) \/ (b₃ . b₁)

proof end;

theorem Th28: :: SETLIM_1:28

for b₁ being set
for b₂ being SetSequence of b₁ holds inferior_setsequence b₂ is non-decreasing

proof end;

theorem Th29: :: SETLIM_1:29

for b₁ being set
for b₂ being SetSequence of b₁ holds superior_setsequence b₂ is non-increasing

proof end;

theorem Th30: :: SETLIM_1:30

for b₁ being set
for b₂ being SetSequence of b₁ holds
( inferior_setsequence b₂ is monotone & superior_setsequence b₂ is monotone )

proof end;

registration

let c₁ be set ;
let c₂ be SetSequence of c₁;
cluster inferior_setsequence a₂ -> non-decreasing ;
coherence by Th28;

end;

registration

let c₁ be set ;
let c₂ be SetSequence of c₁;
cluster superior_setsequence a₂ -> non-increasing ;
coherence by Th29;

end;

theorem Th31: :: SETLIM_1:31

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds Intersection b₃ c= (inferior_setsequence b₃) . b₁

proof end;

theorem Th32: :: SETLIM_1:32

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds (superior_setsequence b₃) . b₁ c= Union b₃

proof end;

theorem Th33: :: SETLIM_1:33

for b₁ being set
for b₂ being SetSequence of b₁
for b₃ being Nat holds { (b₂ . b₄) where B is Nat : b₃ <= b₄ } is Subset-Family of b₁

proof end;

theorem Th34: :: SETLIM_1:34

canceled;

theorem Th35: :: SETLIM_1:35

for b₁ being set
for b₂ being SetSequence of b₁ holds Union b₂ = (Intersection (Complement b₂)) `

proof end;

theorem Th36: :: SETLIM_1:36

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds (inferior_setsequence b₃) . b₁ = ((superior_setsequence (Complement b₃)) . b₁) `

proof end;

theorem Th37: :: SETLIM_1:37

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ holds (superior_setsequence b₃) . b₁ = ((inferior_setsequence (Complement b₃)) . b₁) `

proof end;

theorem Th38: :: SETLIM_1:38

for b₁ being set
for b₂ being SetSequence of b₁ holds Complement (inferior_setsequence b₂) = superior_setsequence (Complement b₂)

proof end;

theorem Th39: :: SETLIM_1:39

for b₁ being set
for b₂ being SetSequence of b₁ holds Complement (superior_setsequence b₂) = inferior_setsequence (Complement b₂)

proof end;

theorem Th40: :: SETLIM_1:40

for b₁ being set
for b₂, b₃, b₄ being SetSequence of b₁ st ( for b₅ being Nat holds b₂ . b₅ = (b₃ . b₅) \/ (b₄ . b₅) ) holds
for b₅ being Nat holds ((inferior_setsequence b₃) . b₅) \/ ((inferior_setsequence b₄) . b₅) c= (inferior_setsequence b₂) . b₅

proof end;

theorem Th41: :: SETLIM_1:41

for b₁ being set
for b₂, b₃, b₄ being SetSequence of b₁ st ( for b₅ being Nat holds b₂ . b₅ = (b₃ . b₅) /\ (b₄ . b₅) ) holds
for b₅ being Nat holds (inferior_setsequence b₂) . b₅ = ((inferior_setsequence b₃) . b₅) /\ ((inferior_setsequence b₄) . b₅)

proof end;

theorem Th42: :: SETLIM_1:42

for b₁ being set
for b₂, b₃, b₄ being SetSequence of b₁ st ( for b₅ being Nat holds b₂ . b₅ = (b₃ . b₅) \/ (b₄ . b₅) ) holds
for b₅ being Nat holds (superior_setsequence b₂) . b₅ = ((superior_setsequence b₃) . b₅) \/ ((superior_setsequence b₄) . b₅)

proof end;

theorem Th43: :: SETLIM_1:43

for b₁ being set
for b₂, b₃, b₄ being SetSequence of b₁ st ( for b₅ being Nat holds b₂ . b₅ = (b₃ . b₅) /\ (b₄ . b₅) ) holds
for b₅ being Nat holds (superior_setsequence b₂) . b₅ c= ((superior_setsequence b₃) . b₅) /\ ((superior_setsequence b₄) . b₅)

proof end;

theorem Th44: :: SETLIM_1:44

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is constant & the_value_of b₃ = b₂ holds
for b₄ being Nat holds (inferior_setsequence b₃) . b₄ = b₂

proof end;

theorem Th45: :: SETLIM_1:45

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is constant & the_value_of b₃ = b₂ holds
for b₄ being Nat holds (superior_setsequence b₃) . b₄ = b₂

proof end;

theorem Th46: :: SETLIM_1:46

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
b₃ . b₁ c= (superior_setsequence b₃) . (b₁ + 1)

proof end;

theorem Th47: :: SETLIM_1:47

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
(superior_setsequence b₃) . b₁ = (superior_setsequence b₃) . (b₁ + 1)

proof end;

theorem Th48: :: SETLIM_1:48

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
(superior_setsequence b₃) . b₁ = Union b₃

proof end;

theorem Th49: :: SETLIM_1:49

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-decreasing holds
Intersection (superior_setsequence b₂) = Union b₂

proof end;

theorem Th50: :: SETLIM_1:50

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
b₃ . b₁ c= (inferior_setsequence b₃) . (b₁ + 1)

proof end;

theorem Th51: :: SETLIM_1:51

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
(inferior_setsequence b₃) . b₁ = b₃ . b₁

proof end;

theorem Th52: :: SETLIM_1:52

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-decreasing holds
inferior_setsequence b₂ = b₂

proof end;

theorem Th53: :: SETLIM_1:53

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ st b₃ is non-increasing holds
(superior_setsequence b₃) . (b₁ + 1) c= b₃ . b₁

proof end;

theorem Th54: :: SETLIM_1:54

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ st b₃ is non-increasing holds
(superior_setsequence b₃) . b₁ = b₃ . b₁

proof end;

theorem Th55: :: SETLIM_1:55

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-increasing holds
superior_setsequence b₂ = b₂

proof end;

theorem Th56: :: SETLIM_1:56

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ st b₃ is non-increasing holds
(inferior_setsequence b₃) . (b₁ + 1) c= b₃ . b₁

proof end;

theorem Th57: :: SETLIM_1:57

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ st b₃ is non-increasing holds
(inferior_setsequence b₃) . b₁ = (inferior_setsequence b₃) . (b₁ + 1)

proof end;

theorem Th58: :: SETLIM_1:58

for b₁ being Nat
for b₂ being set
for b₃ being SetSequence of b₂ st b₃ is non-increasing holds
(inferior_setsequence b₃) . b₁ = Intersection b₃

proof end;

theorem Th59: :: SETLIM_1:59

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-increasing holds
Union (inferior_setsequence b₂) = Intersection b₂

proof end;

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
redefine func lim_inf c₂ -> Element of bool a₁ equals :: SETLIM_1:def 4
Union (inferior_setsequence a₂);
compatibility

proof end;

end;

:: deftheorem Def4 defines lim_inf SETLIM_1:def 4 :

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
redefine func lim_sup c₂ -> Element of bool a₁ equals :: SETLIM_1:def 5
Intersection (superior_setsequence a₂);
compatibility

proof end;

end;

:: deftheorem Def5 defines lim_sup SETLIM_1:def 5 :

definition

let c₁ be set ;
let c₂ be SetSequence of c₁;
assume E51: c₂ is convergent ;
func lim c₂ -> Subset of a₁ means :Def6: :: SETLIM_1:def 6
( a₃ = lim_sup a₂ & a₃ = lim_inf a₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines lim SETLIM_1:def 6 :

theorem Th60: :: SETLIM_1:60

for b₁ being set
for b₂ being SetSequence of b₁ holds Intersection b₂ c= lim_inf b₂

proof end;

theorem Th61: :: SETLIM_1:61

for b₁ being set
for b₂ being SetSequence of b₁ holds lim_inf b₂ = lim (inferior_setsequence b₂)

proof end;

theorem Th62: :: SETLIM_1:62

for b₁ being set
for b₂ being SetSequence of b₁ holds lim_sup b₂ = lim (superior_setsequence b₂)

proof end;

theorem Th63: :: SETLIM_1:63

for b₁ being set
for b₂ being SetSequence of b₁ holds lim_sup b₂ = (lim_inf (Complement b₂)) `

proof end;

theorem Th64: :: SETLIM_1:64

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SetSequence of b₁ st b₃ is constant & the_value_of b₃ = b₂ holds
( b₃ is convergent & lim b₃ = b₂ & lim_inf b₃ = b₂ & lim_sup b₃ = b₂ )

proof end;

theorem Th65: :: SETLIM_1:65

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-decreasing holds
lim_sup b₂ = Union b₂ by Th49;

theorem Th66: :: SETLIM_1:66

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-decreasing holds
lim_inf b₂ = Union b₂ by Th52;

theorem Th67: :: SETLIM_1:67

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-increasing holds
lim_sup b₂ = Intersection b₂ by Th55;

theorem Th68: :: SETLIM_1:68

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-increasing holds
lim_inf b₂ = Intersection b₂ by Th59;

theorem Th69: :: SETLIM_1:69

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-decreasing holds
( b₂ is convergent & lim b₂ = Union b₂ )

proof end;

theorem Th70: :: SETLIM_1:70

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is non-increasing holds
( b₂ is convergent & lim b₂ = Intersection b₂ )

proof end;

theorem Th71: :: SETLIM_1:71

for b₁ being set
for b₂ being SetSequence of b₁ st b₂ is monotone holds
b₂ is convergent

proof end;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
redefine attr constant as a₃ is constant means :: SETLIM_1:def 7
ex b₁ being Element of a₂ st
for b₂ being Nat holds a₃ . b₂ = b₁;
compatibility

proof end;

end;

:: deftheorem Def7 defines constant SETLIM_1:def 7 :

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
func @inferior_setsequence c₃ -> SetSequence of a₂ equals :: SETLIM_1:def 8
inferior_setsequence a₃;
coherence

proof end;

end;

:: deftheorem Def8 defines @inferior_setsequence SETLIM_1:def 8 :

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
func @superior_setsequence c₃ -> SetSequence of a₂ equals :: SETLIM_1:def 9
superior_setsequence a₃;
coherence

proof end;

end;

:: deftheorem Def9 defines @superior_setsequence SETLIM_1:def 9 :

theorem Th72: :: SETLIM_1:72

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds @superior_setsequence b₃ is non-increasing ;

theorem Th73: :: SETLIM_1:73

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds @inferior_setsequence b₃ is non-decreasing ;

registration

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
cluster @superior_setsequence a₃ -> non-increasing ;
coherence ;

end;

registration

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
cluster @inferior_setsequence a₃ -> non-decreasing ;
coherence ;

end;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
func lim_inf c₃ -> Element of a₂ equals :: SETLIM_1:def 10
Union (@inferior_setsequence a₃);
coherence by PROB_1:46;

end;

:: deftheorem Def10 defines lim_inf SETLIM_1:def 10 :

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
func lim_sup c₃ -> Element of a₂ equals :: SETLIM_1:def 11
Intersection (@superior_setsequence a₃);
coherence

proof end;

end;

:: deftheorem Def11 defines lim_sup SETLIM_1:def 11 :

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
attr a₃ is convergent means :Def12: :: SETLIM_1:def 12
lim_sup a₃ = lim_inf a₃;

end;

:: deftheorem Def12 defines convergent SETLIM_1:def 12 :

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
assume E60: c₃ is convergent ;
func lim c₃ -> Element of a₂ means :Def13: :: SETLIM_1:def 13
( a₄ = lim_sup a₃ & a₄ = lim_inf a₃ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def13 defines lim SETLIM_1:def 13 :

theorem Th74: :: SETLIM_1:74

for b₁, b₂ being set
for b₃ being SigmaField of b₁
for b₄ being SetSequence of b₃ holds
( b₂ in lim_sup b₄ iff for b₅ being Nat ex b₆ being Nat st b₂ in b₄ . (b₅ + b₆) )

proof end;

theorem Th75: :: SETLIM_1:75

for b₁, b₂ being set
for b₃ being SigmaField of b₁
for b₄ being SetSequence of b₃ holds
( b₂ in lim_inf b₄ iff ex b₅ being Nat st
for b₆ being Nat holds b₂ in b₄ . (b₅ + b₆) )

proof end;

theorem Th76: :: SETLIM_1:76

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds Intersection b₃ c= lim_inf b₃

proof end;

theorem Th77: :: SETLIM_1:77

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds lim_sup b₃ c= Union b₃

proof end;

theorem Th78: :: SETLIM_1:78

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds lim_inf b₃ c= lim_sup b₃

proof end;

definition

let c₁ be set ;
let c₂ be SigmaField of c₁;
let c₃ be SetSequence of c₂;
func @Complement c₃ -> SetSequence of a₂ equals :: SETLIM_1:def 14
Complement a₃;
coherence

proof end;

end;

:: deftheorem Def14 defines @Complement SETLIM_1:def 14 :

theorem Th79: :: SETLIM_1:79

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds lim_inf b₃ = (lim_sup (@Complement b₃)) `

proof end;

theorem Th80: :: SETLIM_1:80

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ holds lim_sup b₃ = (lim_inf (@Complement b₃)) `

proof end;

theorem Th81: :: SETLIM_1:81

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄, b₅ being SetSequence of b₂ st ( for b₆ being Nat holds b₃ . b₆ = (b₄ . b₆) \/ (b₅ . b₆) ) holds
(lim_inf b₄) \/ (lim_inf b₅) c= lim_inf b₃

proof end;

theorem Th82: :: SETLIM_1:82

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄, b₅ being SetSequence of b₂ st ( for b₆ being Nat holds b₃ . b₆ = (b₄ . b₆) /\ (b₅ . b₆) ) holds
lim_inf b₃ = (lim_inf b₄) /\ (lim_inf b₅)

proof end;

theorem Th83: :: SETLIM_1:83

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄, b₅ being SetSequence of b₂ st ( for b₆ being Nat holds b₃ . b₆ = (b₄ . b₆) \/ (b₅ . b₆) ) holds
lim_sup b₃ = (lim_sup b₄) \/ (lim_sup b₅)

proof end;

theorem Th84: :: SETLIM_1:84

for b₁ being set
for b₂ being SigmaField of b₁
for b₃, b₄, b₅ being SetSequence of b₂ st ( for b₆ being Nat holds b₃ . b₆ = (b₄ . b₆) /\ (b₅ . b₆) ) holds
lim_sup b₃ c= (lim_sup b₄) /\ (lim_sup b₅)

proof end;

theorem Th85: :: SETLIM_1:85

for b₁ being set
for b₂ being Subset of b₁
for b₃ being SigmaField of b₁
for b₄ being SetSequence of b₃ st b₄ is constant & the_value_of b₄ = b₂ holds
( b₄ is convergent & lim b₄ = b₂ & lim_inf b₄ = b₂ & lim_sup b₄ = b₂ )

proof end;

theorem Th86: :: SETLIM_1:86

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
lim_sup b₃ = Union b₃

proof end;

theorem Th87: :: SETLIM_1:87

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
lim_inf b₃ = Union b₃

proof end;

theorem Th88: :: SETLIM_1:88

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is non-decreasing holds
( b₃ is convergent & lim b₃ = Union b₃ )

proof end;

theorem Th89: :: SETLIM_1:89

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is non-increasing holds
lim_sup b₃ = Intersection b₃

proof end;

theorem Th90: :: SETLIM_1:90

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is non-increasing holds
lim_inf b₃ = Intersection b₃

proof end;

theorem Th91: :: SETLIM_1:91

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is non-increasing holds
( b₃ is convergent & lim b₃ = Intersection b₃ )

proof end;

theorem Th92: :: SETLIM_1:92

for b₁ being set
for b₂ being SigmaField of b₁
for b₃ being SetSequence of b₂ st b₃ is monotone holds
b₃ is convergent

proof end;