:: Inferior Limit, Superior Limit and Convergence of Sequences of ExtendedReal Numbers
:: by Hiroshi Yamazaki , Noboru Endou , Yasunari Shidama and Hiroyuki Okazaki
::
:: Received August 28, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: RINFSUP2:1
theorem :: RINFSUP2:2
theorem Th3: :: RINFSUP2:3
theorem :: RINFSUP2:4
:: deftheorem defines sup RINFSUP2:def 1 :
:: deftheorem defines inf RINFSUP2:def 2 :
:: deftheorem Def3 defines bounded_below RINFSUP2:def 3 :
:: deftheorem Def4 defines bounded_above RINFSUP2:def 4 :
:: deftheorem Def5 defines bounded RINFSUP2:def 5 :
theorem Th5: :: RINFSUP2:5
:: deftheorem Def6 defines inferior_realsequence RINFSUP2:def 6 :
:: deftheorem Def7 defines superior_realsequence RINFSUP2:def 7 :
theorem :: RINFSUP2:6
theorem Th7: :: RINFSUP2:7
theorem Th8: :: RINFSUP2:8
Lm1:
for seq being ExtREAL_sequence holds superior_realsequence seq is non-increasing
Lm2:
for seq being ExtREAL_sequence holds inferior_realsequence seq is non-decreasing
:: deftheorem RINFSUP2:def 8 :
canceled;
:: deftheorem RINFSUP2:def 9 :
canceled;
:: deftheorem RINFSUP2:def 10 :
canceled;
:: deftheorem RINFSUP2:def 11 :
canceled;
:: deftheorem defines lim_sup RINFSUP2:def 12 :
:: deftheorem defines lim_inf RINFSUP2:def 13 :
theorem Th9: :: RINFSUP2:9
theorem Th10: :: RINFSUP2:10
theorem Th11: :: RINFSUP2:11
theorem Th12: :: RINFSUP2:12
theorem Th13: :: RINFSUP2:13
theorem Th14: :: RINFSUP2:14
theorem Th15: :: RINFSUP2:15
theorem Th16: :: RINFSUP2:16
theorem Th17: :: RINFSUP2:17
theorem Th18: :: RINFSUP2:18
theorem Th19: :: RINFSUP2:19
theorem Th20: :: RINFSUP2:20
theorem :: RINFSUP2:21
theorem :: RINFSUP2:22
theorem Th23: :: RINFSUP2:23
theorem Th24: :: RINFSUP2:24
theorem Th25: :: RINFSUP2:25
theorem Th26: :: RINFSUP2:26
theorem :: RINFSUP2:27
theorem Th28: :: RINFSUP2:28
theorem Th29: :: RINFSUP2:29
theorem Th30: :: RINFSUP2:30
theorem Th31: :: RINFSUP2:31
Lm4:
for seq being ExtREAL_sequence st seq is bounded & seq is non-increasing holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq )
Lm5:
for seq being ExtREAL_sequence st seq is bounded & seq is non-decreasing holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq )
theorem Th32: :: RINFSUP2:32
theorem Th33: :: RINFSUP2:33
theorem Th34: :: RINFSUP2:34
theorem Th35: :: RINFSUP2:35
theorem Th36: :: RINFSUP2:36
theorem Th37: :: RINFSUP2:37
theorem Th38: :: RINFSUP2:38
theorem :: RINFSUP2:39
Lm6:
for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = +infty holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
Lm7:
for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = -infty holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
Lm8:
for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq in REAL holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
theorem Th40: :: RINFSUP2:40
theorem :: RINFSUP2:41