:: Monotone Real Sequences. Subsequences
:: by Jaros{\l}aw Kotowicz
::
:: Received November 23, 1989
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for n, m being Element of NAT st n < m holds
ex k being Element of NAT st m = (n + 1) + k
Lm2:
for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . n < seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) & ( ( for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) implies for n, m being Element of NAT st n < m holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st n < m holds
seq . n < seq . m ) implies for n being Element of NAT holds seq . n < seq . (n + 1) ) )
Lm3:
for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . (n + 1) < seq . n ) implies for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) & ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies for n being Element of NAT holds seq . (n + 1) < seq . n ) )
Lm4:
for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . n <= seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n <= seq . (n + k) ) & ( ( for n, k being Element of NAT holds seq . n <= seq . (n + k) ) implies for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) implies for n being Element of NAT holds seq . n <= seq . (n + 1) ) )
Lm5:
for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . (n + 1) <= seq . n ) implies for n, k being Element of NAT holds seq . (n + k) <= seq . n ) & ( ( for n, k being Element of NAT holds seq . (n + k) <= seq . n ) implies for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) implies for n being Element of NAT holds seq . (n + 1) <= seq . n ) )
:: deftheorem Def1 defines increasing SEQM_3:def 1 :
:: deftheorem Def2 defines decreasing SEQM_3:def 2 :
:: deftheorem Def3 defines non-decreasing SEQM_3:def 3 :
:: deftheorem Def4 defines non-increasing SEQM_3:def 4 :
Lm6:
for f being Real_Sequence holds
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
Lm7:
for f being Real_Sequence holds
( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) )
Lm8:
for f being Real_Sequence holds
( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) )
Lm9:
for f being Real_Sequence holds
( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) )
:: deftheorem SEQM_3:def 5 :
canceled;
:: deftheorem SEQM_3:def 6 :
canceled;
:: deftheorem Def7 defines monotone SEQM_3:def 7 :
theorem :: SEQM_3:1
canceled;
theorem :: SEQM_3:2
canceled;
theorem :: SEQM_3:3
canceled;
theorem :: SEQM_3:4
canceled;
theorem :: SEQM_3:5
canceled;
theorem :: SEQM_3:6
canceled;
theorem Th7: :: SEQM_3:7
theorem :: SEQM_3:8
theorem Th9: :: SEQM_3:9
theorem Th10: :: SEQM_3:10
theorem Th11: :: SEQM_3:11
theorem Th12: :: SEQM_3:12
theorem Th13: :: SEQM_3:13
theorem Th14: :: SEQM_3:14
theorem :: SEQM_3:15
canceled;
theorem :: SEQM_3:16
canceled;
theorem :: SEQM_3:17
canceled;
theorem :: SEQM_3:18
canceled;
theorem :: SEQM_3:19
theorem :: SEQM_3:20
theorem Th21: :: SEQM_3:21
theorem Th22: :: SEQM_3:22
theorem :: SEQM_3:23
canceled;
theorem :: SEQM_3:24
canceled;
theorem :: SEQM_3:25
canceled;
theorem :: SEQM_3:26
canceled;
theorem :: SEQM_3:27
canceled;
Lm11:
( incl NAT is increasing & incl NAT is natural-valued )
Lm11A:
( id NAT is increasing & id NAT is natural-valued )
;
Lm6A:
for f being sequence of NAT holds
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
theorem :: SEQM_3:28
canceled;
theorem :: SEQM_3:29
theorem :: SEQM_3:30
canceled;
theorem :: SEQM_3:31
canceled;
:: deftheorem SEQM_3:def 8 :
canceled;
:: deftheorem SEQM_3:def 9 :
canceled;
:: deftheorem SEQM_3:def 10 :
canceled;
:: deftheorem defines increasing SEQM_3:def 11 :
:: deftheorem defines decreasing SEQM_3:def 12 :
:: deftheorem defines non-decreasing SEQM_3:def 13 :
:: deftheorem defines non-increasing SEQM_3:def 14 :
theorem :: SEQM_3:32
canceled;
theorem :: SEQM_3:33
theorem :: SEQM_3:34
canceled;
theorem :: SEQM_3:35
canceled;
theorem :: SEQM_3:36
canceled;
theorem Th37: :: SEQM_3:37
theorem Th38: :: SEQM_3:38
theorem :: SEQM_3:39
theorem :: SEQM_3:40
canceled;
theorem Th41: :: SEQM_3:41
theorem Th42: :: SEQM_3:42
theorem :: SEQM_3:43
theorem :: SEQM_3:44
theorem :: SEQM_3:45
canceled;
theorem :: SEQM_3:46
canceled;
theorem :: SEQM_3:47
canceled;
theorem :: SEQM_3:48
canceled;
theorem :: SEQM_3:49
theorem :: SEQM_3:50
theorem Th51: :: SEQM_3:51
theorem Th52: :: SEQM_3:52
theorem :: SEQM_3:53
theorem :: SEQM_3:54
canceled;
theorem :: SEQM_3:55
canceled;
theorem Th56: :: SEQM_3:56
theorem Th57: :: SEQM_3:57
theorem :: SEQM_3:58
theorem :: SEQM_3:59
theorem :: SEQM_3:60
theorem :: SEQM_3:61
theorem :: SEQM_3:62
theorem Th63: :: SEQM_3:63
theorem :: SEQM_3:64
theorem :: SEQM_3:65
canceled;
theorem :: SEQM_3:66
canceled;
theorem :: SEQM_3:67
canceled;
theorem Th68: :: SEQM_3:68
theorem :: SEQM_3:69
canceled;
theorem :: SEQM_3:70
theorem :: SEQM_3:71
canceled;
theorem :: SEQM_3:72
canceled;
theorem :: SEQM_3:73
canceled;
theorem :: SEQM_3:74
canceled;
theorem :: SEQM_3:75
canceled;
theorem :: SEQM_3:76
canceled;
theorem :: SEQM_3:77
theorem :: SEQM_3:78
theorem :: SEQM_3:79
canceled;
theorem :: SEQM_3:80