:: The Limit of a Real Function at Infinity. Halflines.Real Sequence Divergent to Infinity
:: by Jaros{\l}aw Kotowicz
::
:: Received August 20, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for g, r, r1 being real number st 0 < g & r <= r1 holds
( r - g < r1 & r < r1 + g )
Lm2:
for seq being Real_Sequence
for f1, f2 being PartFunc of REAL , REAL st rng seq c= dom (f1 + f2) holds
( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 )
Lm3:
for seq being Real_Sequence
for f1, f2 being PartFunc of REAL , REAL st rng seq c= dom (f1 (#) f2) holds
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 )
:: deftheorem defines left_closed_halfline LIMFUNC1:def 1 :
:: deftheorem defines right_closed_halfline LIMFUNC1:def 2 :
:: deftheorem defines right_open_halfline LIMFUNC1:def 3 :
theorem :: LIMFUNC1:1
canceled;
theorem :: LIMFUNC1:2
canceled;
theorem :: LIMFUNC1:3
canceled;
theorem :: LIMFUNC1:4
canceled;
theorem :: LIMFUNC1:5
canceled;
theorem :: LIMFUNC1:6
canceled;
theorem :: LIMFUNC1:7
canceled;
theorem :: LIMFUNC1:8
canceled;
theorem :: LIMFUNC1:9
canceled;
theorem :: LIMFUNC1:10
canceled;
theorem :: LIMFUNC1:11
canceled;
theorem :: LIMFUNC1:12
canceled;
theorem :: LIMFUNC1:13
canceled;
theorem :: LIMFUNC1:14
canceled;
theorem :: LIMFUNC1:15
canceled;
theorem :: LIMFUNC1:16
canceled;
theorem :: LIMFUNC1:17
canceled;
theorem :: LIMFUNC1:18
canceled;
theorem :: LIMFUNC1:19
canceled;
theorem :: LIMFUNC1:20
canceled;
theorem :: LIMFUNC1:21
canceled;
theorem :: LIMFUNC1:22
canceled;
theorem :: LIMFUNC1:23
canceled;
theorem :: LIMFUNC1:24
canceled;
theorem :: LIMFUNC1:25
canceled;
theorem Th26: :: LIMFUNC1:26
theorem Th27: :: LIMFUNC1:27
theorem Th28: :: LIMFUNC1:28
theorem Th29: :: LIMFUNC1:29
theorem Th30: :: LIMFUNC1:30
:: deftheorem Def4 defines divergent_to+infty LIMFUNC1:def 4 :
:: deftheorem Def5 defines divergent_to-infty LIMFUNC1:def 5 :
theorem :: LIMFUNC1:31
canceled;
theorem :: LIMFUNC1:32
canceled;
theorem :: LIMFUNC1:33
theorem Th34: :: LIMFUNC1:34
theorem Th35: :: LIMFUNC1:35
theorem Th36: :: LIMFUNC1:36
theorem Th37: :: LIMFUNC1:37
theorem Th38: :: LIMFUNC1:38
theorem Th39: :: LIMFUNC1:39
theorem Th40: :: LIMFUNC1:40
theorem Th41: :: LIMFUNC1:41
theorem :: LIMFUNC1:42
theorem :: LIMFUNC1:43
theorem :: LIMFUNC1:44
theorem :: LIMFUNC1:45
theorem :: LIMFUNC1:46
theorem Th47: :: LIMFUNC1:47
set s1 = incl NAT ;
Lm7:
for n being Element of NAT holds (incl NAT ) . n = n
by FUNCT_1:35;
theorem Th48: :: LIMFUNC1:48
theorem Th49: :: LIMFUNC1:49
theorem :: LIMFUNC1:50
theorem Th51: :: LIMFUNC1:51
theorem Th52: :: LIMFUNC1:52
theorem Th53: :: LIMFUNC1:53
theorem Th54: :: LIMFUNC1:54
theorem :: LIMFUNC1:55
theorem Th56: :: LIMFUNC1:56
theorem Th57: :: LIMFUNC1:57
theorem :: LIMFUNC1:58
theorem :: LIMFUNC1:59
theorem :: LIMFUNC1:60
theorem Th61: :: LIMFUNC1:61
theorem Th62: :: LIMFUNC1:62
theorem Th63: :: LIMFUNC1:63
theorem Th64: :: LIMFUNC1:64
theorem Th65: :: LIMFUNC1:65
theorem :: LIMFUNC1:66
theorem :: LIMFUNC1:67
theorem :: LIMFUNC1:68
theorem Th69: :: LIMFUNC1:69
theorem Th70: :: LIMFUNC1:70
:: deftheorem Def6 defines convergent_in+infty LIMFUNC1:def 6 :
:: deftheorem Def7 defines divergent_in+infty_to+infty LIMFUNC1:def 7 :
:: deftheorem Def8 defines divergent_in+infty_to-infty LIMFUNC1:def 8 :
:: deftheorem Def9 defines convergent_in-infty LIMFUNC1:def 9 :
:: deftheorem Def10 defines divergent_in-infty_to+infty LIMFUNC1:def 10 :
:: deftheorem Def11 defines divergent_in-infty_to-infty LIMFUNC1:def 11 :
theorem :: LIMFUNC1:71
canceled;
theorem :: LIMFUNC1:72
canceled;
theorem :: LIMFUNC1:73
canceled;
theorem :: LIMFUNC1:74
canceled;
theorem :: LIMFUNC1:75
canceled;
theorem :: LIMFUNC1:76
canceled;
theorem :: LIMFUNC1:77
theorem :: LIMFUNC1:78
theorem :: LIMFUNC1:79
theorem :: LIMFUNC1:80
theorem :: LIMFUNC1:81
theorem :: LIMFUNC1:82
theorem :: LIMFUNC1:83
theorem :: LIMFUNC1:84
theorem :: LIMFUNC1:85
theorem :: LIMFUNC1:86
theorem :: LIMFUNC1:87
theorem :: LIMFUNC1:88
theorem :: LIMFUNC1:89
theorem :: LIMFUNC1:90
theorem :: LIMFUNC1:91
theorem :: LIMFUNC1:92
theorem :: LIMFUNC1:93
theorem :: LIMFUNC1:94
theorem Th95: :: LIMFUNC1:95
theorem :: LIMFUNC1:96
theorem Th97: :: LIMFUNC1:97
theorem :: LIMFUNC1:98
theorem Th99: :: LIMFUNC1:99
theorem :: LIMFUNC1:100
theorem Th101: :: LIMFUNC1:101
theorem :: LIMFUNC1:102
theorem Th103: :: LIMFUNC1:103
theorem Th104: :: LIMFUNC1:104
theorem Th105: :: LIMFUNC1:105
theorem Th106: :: LIMFUNC1:106
theorem :: LIMFUNC1:107
theorem :: LIMFUNC1:108
theorem :: LIMFUNC1:109
theorem :: LIMFUNC1:110
:: deftheorem Def12 defines lim_in+infty LIMFUNC1:def 12 :
:: deftheorem Def13 defines lim_in-infty LIMFUNC1:def 13 :
theorem :: LIMFUNC1:111
canceled;
theorem :: LIMFUNC1:112
canceled;
theorem :: LIMFUNC1:113
theorem :: LIMFUNC1:114
theorem Th115: :: LIMFUNC1:115
theorem Th116: :: LIMFUNC1:116
theorem Th117: :: LIMFUNC1:117
theorem :: LIMFUNC1:118
theorem :: LIMFUNC1:119
theorem :: LIMFUNC1:120
theorem Th121: :: LIMFUNC1:121
theorem Th122: :: LIMFUNC1:122
theorem :: LIMFUNC1:123
theorem Th124: :: LIMFUNC1:124
theorem Th125: :: LIMFUNC1:125
theorem Th126: :: LIMFUNC1:126
theorem :: LIMFUNC1:127
theorem :: LIMFUNC1:128
theorem :: LIMFUNC1:129
theorem Th130: :: LIMFUNC1:130
theorem Th131: :: LIMFUNC1:131
theorem :: LIMFUNC1:132
theorem :: LIMFUNC1:133
theorem :: LIMFUNC1:134
theorem Th135: :: LIMFUNC1:135
theorem :: LIMFUNC1:136
theorem Th137: :: LIMFUNC1:137
theorem :: LIMFUNC1:138
theorem :: LIMFUNC1:139
theorem :: LIMFUNC1:140
theorem :: LIMFUNC1:141
theorem :: LIMFUNC1:142
theorem :: LIMFUNC1:143
theorem :: LIMFUNC1:144
theorem :: LIMFUNC1:145
theorem :: LIMFUNC1:146
theorem :: LIMFUNC1:147
theorem :: LIMFUNC1:148
theorem :: LIMFUNC1:149
theorem :: LIMFUNC1:150