:: Basic Properties of Extended Real NumbersAdam Grabowski
:: by Andrzej Trybulec, Yatsuka Nakamura, Artur Korni{\l}owicz and
::
:: Received January 22, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: deftheorem defines [. XXREAL_1:def 1 :
:: deftheorem defines [. XXREAL_1:def 2 :
:: deftheorem defines ]. XXREAL_1:def 3 :
:: deftheorem defines ]. XXREAL_1:def 4 :
theorem Th1: :: XXREAL_1:1
theorem Th2: :: XXREAL_1:2
theorem Th3: :: XXREAL_1:3
theorem Th4: :: XXREAL_1:4
theorem Th5: :: XXREAL_1:5
theorem Th6: :: XXREAL_1:6
theorem Th7: :: XXREAL_1:7
theorem Th8: :: XXREAL_1:8
theorem Th9: :: XXREAL_1:9
theorem :: XXREAL_1:10
theorem :: XXREAL_1:11
theorem Th12: :: XXREAL_1:12
theorem Th13: :: XXREAL_1:13
theorem Th14: :: XXREAL_1:14
theorem Th15: :: XXREAL_1:15
theorem Th16: :: XXREAL_1:16
theorem Th17: :: XXREAL_1:17
theorem Th18: :: XXREAL_1:18
theorem Th19: :: XXREAL_1:19
theorem Th20: :: XXREAL_1:20
theorem Th21: :: XXREAL_1:21
theorem Th22: :: XXREAL_1:22
theorem Th23: :: XXREAL_1:23
theorem Th24: :: XXREAL_1:24
theorem Th25: :: XXREAL_1:25
theorem :: XXREAL_1:26
theorem Th27: :: XXREAL_1:27
theorem Th28: :: XXREAL_1:28
theorem Th29: :: XXREAL_1:29
theorem :: XXREAL_1:30
theorem :: XXREAL_1:31
theorem :: XXREAL_1:32
theorem :: XXREAL_1:33
theorem Th34: :: XXREAL_1:34
theorem Th35: :: XXREAL_1:35
theorem Th36: :: XXREAL_1:36
theorem Th37: :: XXREAL_1:37
theorem Th38: :: XXREAL_1:38
theorem Th39: :: XXREAL_1:39
theorem Th40: :: XXREAL_1:40
theorem Th41: :: XXREAL_1:41
theorem Th42: :: XXREAL_1:42
theorem Th43: :: XXREAL_1:43
theorem Th44: :: XXREAL_1:44
theorem Th45: :: XXREAL_1:45
theorem Th46: :: XXREAL_1:46
theorem Th47: :: XXREAL_1:47
theorem Th48: :: XXREAL_1:48
theorem Th49: :: XXREAL_1:49
theorem Th50: :: XXREAL_1:50
theorem Th51: :: XXREAL_1:51
theorem Th52: :: XXREAL_1:52
theorem Th53: :: XXREAL_1:53
theorem Th54: :: XXREAL_1:54
theorem Th55: :: XXREAL_1:55
theorem Th56: :: XXREAL_1:56
theorem Th57: :: XXREAL_1:57
theorem Th58: :: XXREAL_1:58
theorem Th59: :: XXREAL_1:59
theorem Th60: :: XXREAL_1:60
theorem Th61: :: XXREAL_1:61
theorem Th62: :: XXREAL_1:62
theorem Th63: :: XXREAL_1:63
theorem Th64: :: XXREAL_1:64
theorem Th65: :: XXREAL_1:65
theorem :: XXREAL_1:66
theorem :: XXREAL_1:67
theorem :: XXREAL_1:68
theorem :: XXREAL_1:69
theorem :: XXREAL_1:70
theorem :: XXREAL_1:71
theorem :: XXREAL_1:72
theorem :: XXREAL_1:73
theorem :: XXREAL_1:74
theorem :: XXREAL_1:75
theorem :: XXREAL_1:76
theorem :: XXREAL_1:77
theorem :: XXREAL_1:78
theorem :: XXREAL_1:79
theorem :: XXREAL_1:80
theorem :: XXREAL_1:81
theorem :: XXREAL_1:82
theorem :: XXREAL_1:83
theorem :: XXREAL_1:84
theorem Th85: :: XXREAL_1:85
theorem :: XXREAL_1:86
theorem :: XXREAL_1:87
theorem :: XXREAL_1:88
theorem :: XXREAL_1:89
theorem :: XXREAL_1:90
theorem :: XXREAL_1:91
theorem :: XXREAL_1:92
theorem :: XXREAL_1:93
theorem :: XXREAL_1:94
theorem :: XXREAL_1:95
theorem :: XXREAL_1:96
theorem :: XXREAL_1:97
theorem :: XXREAL_1:98
theorem :: XXREAL_1:99
theorem :: XXREAL_1:100
theorem :: XXREAL_1:101
theorem :: XXREAL_1:102
theorem :: XXREAL_1:103
theorem :: XXREAL_1:104
theorem :: XXREAL_1:105
theorem :: XXREAL_1:106
theorem :: XXREAL_1:107
theorem :: XXREAL_1:108
theorem :: XXREAL_1:109
theorem :: XXREAL_1:110
theorem :: XXREAL_1:111
theorem :: XXREAL_1:112
theorem :: XXREAL_1:113
theorem :: XXREAL_1:114
theorem :: XXREAL_1:115
theorem :: XXREAL_1:116
theorem :: XXREAL_1:117
theorem :: XXREAL_1:118
theorem :: XXREAL_1:119
theorem :: XXREAL_1:120
theorem :: XXREAL_1:121
theorem :: XXREAL_1:122
theorem :: XXREAL_1:123
theorem :: XXREAL_1:124
theorem :: XXREAL_1:125
theorem :: XXREAL_1:126
theorem :: XXREAL_1:127
theorem Th128: :: XXREAL_1:128
theorem Th129: :: XXREAL_1:129
theorem Th130: :: XXREAL_1:130
theorem Th131: :: XXREAL_1:131
theorem Th132: :: XXREAL_1:132
theorem :: XXREAL_1:133
theorem :: XXREAL_1:134
theorem :: XXREAL_1:135
theorem :: XXREAL_1:136
theorem :: XXREAL_1:137
theorem :: XXREAL_1:138
theorem :: XXREAL_1:139
theorem :: XXREAL_1:140
theorem :: XXREAL_1:141
theorem :: XXREAL_1:142
theorem :: XXREAL_1:143
theorem :: XXREAL_1:144
theorem :: XXREAL_1:145
theorem :: XXREAL_1:146
theorem :: XXREAL_1:147
theorem :: XXREAL_1:148
theorem :: XXREAL_1:149
theorem :: XXREAL_1:150
theorem :: XXREAL_1:151
theorem Th152: :: XXREAL_1:152
theorem :: XXREAL_1:153
theorem Th154: :: XXREAL_1:154
theorem :: XXREAL_1:155
theorem :: XXREAL_1:156
theorem :: XXREAL_1:157
theorem :: XXREAL_1:158
theorem Th159: :: XXREAL_1:159
theorem Th160: :: XXREAL_1:160
theorem :: XXREAL_1:161
theorem :: XXREAL_1:162
for
r,
s,
p,
q being
ext-real number st
[.r,s.[ meets [.p,q.[ holds
[.r,s.[ \/ [.p,q.[ = [.(min r,p),(max s,q).[
theorem :: XXREAL_1:163
theorem :: XXREAL_1:164
for
r,
s,
p,
q being
ext-real number st
].r,s.] meets ].p,q.] holds
].r,s.] \/ ].p,q.] = ].(min r,p),(max s,q).]
theorem :: XXREAL_1:165
theorem Th166: :: XXREAL_1:166
theorem Th167: :: XXREAL_1:167
theorem :: XXREAL_1:168
theorem Th169: :: XXREAL_1:169
theorem :: XXREAL_1:170
theorem Th171: :: XXREAL_1:171
theorem :: XXREAL_1:172
theorem Th173: :: XXREAL_1:173
theorem Th174: :: XXREAL_1:174
theorem Th175: :: XXREAL_1:175
theorem :: XXREAL_1:176
theorem :: XXREAL_1:177
theorem Th178: :: XXREAL_1:178
theorem :: XXREAL_1:179
theorem :: XXREAL_1:180
theorem :: XXREAL_1:181
theorem Th182: :: XXREAL_1:182
theorem Th183: :: XXREAL_1:183
theorem Th184: :: XXREAL_1:184
theorem Th185: :: XXREAL_1:185
theorem Th186: :: XXREAL_1:186
theorem Th187: :: XXREAL_1:187
theorem Th188: :: XXREAL_1:188
theorem Th189: :: XXREAL_1:189
theorem Th190: :: XXREAL_1:190
theorem Th191: :: XXREAL_1:191
theorem Th192: :: XXREAL_1:192
theorem Th193: :: XXREAL_1:193
theorem Th194: :: XXREAL_1:194
theorem Th195: :: XXREAL_1:195
theorem Th196: :: XXREAL_1:196
theorem Th197: :: XXREAL_1:197
theorem :: XXREAL_1:198
theorem :: XXREAL_1:199
theorem :: XXREAL_1:200
theorem :: XXREAL_1:201
theorem :: XXREAL_1:202
theorem :: XXREAL_1:203
theorem :: XXREAL_1:204
theorem :: XXREAL_1:205
theorem :: XXREAL_1:206
theorem :: XXREAL_1:207
theorem :: XXREAL_1:208
theorem :: XXREAL_1:209
theorem :: XXREAL_1:210
theorem :: XXREAL_1:211
theorem :: XXREAL_1:212
theorem :: XXREAL_1:213
theorem :: XXREAL_1:214
theorem :: XXREAL_1:215
theorem :: XXREAL_1:216
theorem :: XXREAL_1:217
theorem :: XXREAL_1:218
theorem :: XXREAL_1:219
theorem :: XXREAL_1:220
theorem :: XXREAL_1:221
theorem :: XXREAL_1:222
theorem :: XXREAL_1:223
theorem Th224: :: XXREAL_1:224
theorem Th225: :: XXREAL_1:225
theorem Th226: :: XXREAL_1:226
theorem Th227: :: XXREAL_1:227
theorem Th228: :: XXREAL_1:228
theorem :: XXREAL_1:229
theorem :: XXREAL_1:230
theorem :: XXREAL_1:231
theorem :: XXREAL_1:232
theorem :: XXREAL_1:233
theorem :: XXREAL_1:234
theorem :: XXREAL_1:235
theorem :: XXREAL_1:236
theorem :: XXREAL_1:237
theorem :: XXREAL_1:238
theorem :: XXREAL_1:239
theorem :: XXREAL_1:240
theorem :: XXREAL_1:241
theorem :: XXREAL_1:242
theorem :: XXREAL_1:243
theorem :: XXREAL_1:244
theorem :: XXREAL_1:245
theorem :: XXREAL_1:246
theorem :: XXREAL_1:247
theorem :: XXREAL_1:248
theorem :: XXREAL_1:249
theorem :: XXREAL_1:250
theorem :: XXREAL_1:251
theorem :: XXREAL_1:252
theorem :: XXREAL_1:253
theorem :: XXREAL_1:254
theorem :: XXREAL_1:255
theorem :: XXREAL_1:256
theorem :: XXREAL_1:257
theorem :: XXREAL_1:258
theorem :: XXREAL_1:259
theorem :: XXREAL_1:260
theorem :: XXREAL_1:261
theorem :: XXREAL_1:262
theorem :: XXREAL_1:263
theorem :: XXREAL_1:264
theorem :: XXREAL_1:265
theorem :: XXREAL_1:266
theorem :: XXREAL_1:267
theorem :: XXREAL_1:268
theorem :: XXREAL_1:269
theorem :: XXREAL_1:270
theorem :: XXREAL_1:271
theorem :: XXREAL_1:272
theorem :: XXREAL_1:273
theorem :: XXREAL_1:274
theorem :: XXREAL_1:275
theorem :: XXREAL_1:276
theorem :: XXREAL_1:277
theorem :: XXREAL_1:278
theorem :: XXREAL_1:279
theorem :: XXREAL_1:280
theorem :: XXREAL_1:281
theorem :: XXREAL_1:282
theorem :: XXREAL_1:283
theorem :: XXREAL_1:284
theorem :: XXREAL_1:285
theorem :: XXREAL_1:286
theorem :: XXREAL_1:287
theorem :: XXREAL_1:288
theorem :: XXREAL_1:289
theorem :: XXREAL_1:290
theorem :: XXREAL_1:291
theorem :: XXREAL_1:292
theorem :: XXREAL_1:293
theorem :: XXREAL_1:294
theorem :: XXREAL_1:295
theorem :: XXREAL_1:296
theorem Th297: :: XXREAL_1:297
theorem Th298: :: XXREAL_1:298
theorem Th299: :: XXREAL_1:299
theorem Th300: :: XXREAL_1:300
theorem Th301: :: XXREAL_1:301
theorem Th302: :: XXREAL_1:302
theorem Th303: :: XXREAL_1:303
theorem Th304: :: XXREAL_1:304
theorem Th305: :: XXREAL_1:305
theorem Th306: :: XXREAL_1:306
theorem Th307: :: XXREAL_1:307
theorem Th308: :: XXREAL_1:308
theorem Th309: :: XXREAL_1:309
theorem Th310: :: XXREAL_1:310
theorem Th311: :: XXREAL_1:311
theorem Th312: :: XXREAL_1:312
theorem Th313: :: XXREAL_1:313
theorem Th314: :: XXREAL_1:314
theorem Th315: :: XXREAL_1:315
theorem Th316: :: XXREAL_1:316
theorem Th317: :: XXREAL_1:317
theorem Th318: :: XXREAL_1:318
theorem Th319: :: XXREAL_1:319
theorem Th320: :: XXREAL_1:320
theorem Th321: :: XXREAL_1:321
theorem Th322: :: XXREAL_1:322
theorem Th323: :: XXREAL_1:323
theorem Th324: :: XXREAL_1:324
theorem Th325: :: XXREAL_1:325
theorem Th326: :: XXREAL_1:326
theorem Th327: :: XXREAL_1:327
theorem Th328: :: XXREAL_1:328
theorem Th329: :: XXREAL_1:329
theorem Th330: :: XXREAL_1:330
theorem Th331: :: XXREAL_1:331
theorem Th332: :: XXREAL_1:332
theorem Th333: :: XXREAL_1:333
theorem Th334: :: XXREAL_1:334
theorem Th335: :: XXREAL_1:335
theorem Th336: :: XXREAL_1:336
theorem Th337: :: XXREAL_1:337
theorem Th338: :: XXREAL_1:338
theorem Th339: :: XXREAL_1:339
theorem Th340: :: XXREAL_1:340
theorem Th341: :: XXREAL_1:341
theorem Th342: :: XXREAL_1:342
theorem :: XXREAL_1:343
theorem :: XXREAL_1:344
theorem :: XXREAL_1:345
theorem :: XXREAL_1:346
theorem :: XXREAL_1:347
theorem :: XXREAL_1:348
theorem Th349: :: XXREAL_1:349
theorem Th350: :: XXREAL_1:350
theorem :: XXREAL_1:351
theorem :: XXREAL_1:352
theorem :: XXREAL_1:353
theorem :: XXREAL_1:354
theorem :: XXREAL_1:355
theorem :: XXREAL_1:356
theorem :: XXREAL_1:357
theorem :: XXREAL_1:358
theorem :: XXREAL_1:359
theorem :: XXREAL_1:360
theorem :: XXREAL_1:361
theorem :: XXREAL_1:362
theorem :: XXREAL_1:363
theorem :: XXREAL_1:364
theorem :: XXREAL_1:365
theorem :: XXREAL_1:366
theorem :: XXREAL_1:367
theorem :: XXREAL_1:368
theorem :: XXREAL_1:369
theorem :: XXREAL_1:370
theorem :: XXREAL_1:371
theorem :: XXREAL_1:372
theorem :: XXREAL_1:373
theorem :: XXREAL_1:374
theorem :: XXREAL_1:375
theorem :: XXREAL_1:376
theorem :: XXREAL_1:377
theorem :: XXREAL_1:378
theorem :: XXREAL_1:379
theorem :: XXREAL_1:380
theorem :: XXREAL_1:381
theorem :: XXREAL_1:382
theorem :: XXREAL_1:383
theorem :: XXREAL_1:384
theorem :: XXREAL_1:385
theorem :: XXREAL_1:386
theorem :: XXREAL_1:387
theorem :: XXREAL_1:388
theorem :: XXREAL_1:389
theorem :: XXREAL_1:390
theorem :: XXREAL_1:391
theorem :: XXREAL_1:392
theorem :: XXREAL_1:393
theorem :: XXREAL_1:394
theorem :: XXREAL_1:395
theorem :: XXREAL_1:396
theorem :: XXREAL_1:397
theorem :: XXREAL_1:398
theorem :: XXREAL_1:399
theorem :: XXREAL_1:400
theorem Th401: :: XXREAL_1:401
theorem Th402: :: XXREAL_1:402
theorem Th403: :: XXREAL_1:403
theorem Th404: :: XXREAL_1:404
theorem :: XXREAL_1:405
theorem :: XXREAL_1:406
theorem :: XXREAL_1:407
theorem :: XXREAL_1:408
theorem :: XXREAL_1:409
theorem :: XXREAL_1:410
theorem :: XXREAL_1:411
theorem :: XXREAL_1:412
theorem :: XXREAL_1:413
theorem :: XXREAL_1:414
theorem :: XXREAL_1:415
theorem :: XXREAL_1:416
theorem :: XXREAL_1:417
theorem :: XXREAL_1:418
theorem :: XXREAL_1:419
theorem :: XXREAL_1:420
theorem :: XXREAL_1:421
theorem :: XXREAL_1:422
theorem :: XXREAL_1:423
theorem :: XXREAL_1:424
theorem :: XXREAL_1:425
theorem :: XXREAL_1:426
theorem :: XXREAL_1:427
theorem :: XXREAL_1:428