:: Inferior Limit and Superior Limit of Sequences of Real Numbers
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received April 29, 2005
:: Copyright (c) 2005 Association of Mizar Users
Lm1:
for r1, r2, s being real number st 0 < s & r1 <= r2 holds
( r1 < r2 + s & r1 - s < r2 )
theorem Th1: :: RINFSUP1:1
:: deftheorem defines sup RINFSUP1:def 1 :
:: deftheorem defines inf RINFSUP1:def 2 :
theorem Th2: :: RINFSUP1:2
theorem Th3: :: RINFSUP1:3
theorem Th4: :: RINFSUP1:4
theorem Th5: :: RINFSUP1:5
theorem Th6: :: RINFSUP1:6
theorem Th7: :: RINFSUP1:7
theorem Th8: :: RINFSUP1:8
theorem Th9: :: RINFSUP1:9
theorem Th10: :: RINFSUP1:10
theorem :: RINFSUP1:11
theorem :: RINFSUP1:12
theorem Th13: :: RINFSUP1:13
theorem Th14: :: RINFSUP1:14
theorem Th15: :: RINFSUP1:15
theorem Th16: :: RINFSUP1:16
:: deftheorem Def3 defines nonnegative RINFSUP1:def 3 :
theorem Th17: :: RINFSUP1:17
theorem Th18: :: RINFSUP1:18
theorem :: RINFSUP1:19
theorem Th20: :: RINFSUP1:20
theorem Th21: :: RINFSUP1:21
theorem Th22: :: RINFSUP1:22
theorem Th23: :: RINFSUP1:23
theorem Th24: :: RINFSUP1:24
theorem Th25: :: RINFSUP1:25
theorem Th26: :: RINFSUP1:26
theorem Th27: :: RINFSUP1:27
theorem :: RINFSUP1:28
theorem Th29: :: RINFSUP1:29
theorem Th30: :: RINFSUP1:30
theorem Th31: :: RINFSUP1:31
theorem Th32: :: RINFSUP1:32
theorem Th33: :: RINFSUP1:33
theorem Th34: :: RINFSUP1:34
theorem Th35: :: RINFSUP1:35
theorem Th36: :: RINFSUP1:36
theorem Th37: :: RINFSUP1:37
:: deftheorem Def4 defines inferior_realsequence RINFSUP1:def 4 :
:: deftheorem Def5 defines superior_realsequence RINFSUP1:def 5 :
theorem Th38: :: RINFSUP1:38
theorem Th39: :: RINFSUP1:39
theorem Th40: :: RINFSUP1:40
theorem Th41: :: RINFSUP1:41
theorem Th42: :: RINFSUP1:42
theorem Th43: :: RINFSUP1:43
theorem Th44: :: RINFSUP1:44
theorem Th45: :: RINFSUP1:45
theorem Th46: :: RINFSUP1:46
theorem Th47: :: RINFSUP1:47
theorem Th48: :: RINFSUP1:48
theorem Th49: :: RINFSUP1:49
theorem Th50: :: RINFSUP1:50
theorem Th51: :: RINFSUP1:51
theorem Th52: :: RINFSUP1:52
theorem Th53: :: RINFSUP1:53
theorem :: RINFSUP1:54
theorem Th55: :: RINFSUP1:55
theorem Th56: :: RINFSUP1:56
theorem Th57: :: RINFSUP1:57
theorem Th58: :: RINFSUP1:58
theorem Th59: :: RINFSUP1:59
theorem Th60: :: RINFSUP1:60
theorem Th61: :: RINFSUP1:61
theorem Th62: :: RINFSUP1:62
theorem Th63: :: RINFSUP1:63
theorem Th64: :: RINFSUP1:64
theorem :: RINFSUP1:65
Lm2:
for n being Element of NAT
for seq being Real_Sequence st seq is non-decreasing holds
(inferior_realsequence seq) . n = seq . n
theorem :: RINFSUP1:66
theorem Th67: :: RINFSUP1:67
theorem Th68: :: RINFSUP1:68
theorem Th69: :: RINFSUP1:69
theorem :: RINFSUP1:70
theorem :: RINFSUP1:71
Lm3:
for n being Element of NAT
for seq being Real_Sequence st seq is non-increasing holds
(superior_realsequence seq) . n = seq . n
theorem :: RINFSUP1:72
theorem Th73: :: RINFSUP1:73
theorem Th74: :: RINFSUP1:74
theorem Th75: :: RINFSUP1:75
theorem :: RINFSUP1:76
theorem Th77: :: RINFSUP1:77
theorem :: RINFSUP1:78
theorem :: RINFSUP1:79
theorem :: RINFSUP1:80
theorem Th81: :: RINFSUP1:81
theorem Th82: :: RINFSUP1:82
:: deftheorem defines lim_sup RINFSUP1:def 6 :
:: deftheorem defines lim_inf RINFSUP1:def 7 :
theorem Th83: :: RINFSUP1:83
theorem Th84: :: RINFSUP1:84
theorem :: RINFSUP1:85
theorem Th86: :: RINFSUP1:86
theorem Th87: :: RINFSUP1:87
theorem :: RINFSUP1:88
theorem :: RINFSUP1:89
theorem Th90: :: RINFSUP1:90
theorem :: RINFSUP1:91
theorem Th92: :: RINFSUP1:92
theorem :: RINFSUP1:93
theorem :: RINFSUP1:94
theorem :: RINFSUP1:95