:: Some Properties of Extended Real Numbers Operations: absolutevalue, min and max
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 15, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem :: EXTREAL2:1
canceled;
theorem :: EXTREAL2:2
canceled;
theorem :: EXTREAL2:3
canceled;
theorem :: EXTREAL2:4
canceled;
theorem :: EXTREAL2:5
canceled;
theorem :: EXTREAL2:6
canceled;
theorem :: EXTREAL2:7
canceled;
theorem :: EXTREAL2:8
canceled;
theorem :: EXTREAL2:9
canceled;
theorem :: EXTREAL2:10
canceled;
theorem :: EXTREAL2:11
canceled;
theorem :: EXTREAL2:12
canceled;
theorem :: EXTREAL2:13
canceled;
theorem :: EXTREAL2:14
canceled;
theorem :: EXTREAL2:15
canceled;
theorem :: EXTREAL2:16
canceled;
theorem :: EXTREAL2:17
canceled;
theorem :: EXTREAL2:18
canceled;
theorem :: EXTREAL2:19
canceled;
theorem :: EXTREAL2:20
canceled;
theorem :: EXTREAL2:21
canceled;
theorem :: EXTREAL2:22
canceled;
theorem :: EXTREAL2:23
canceled;
theorem :: EXTREAL2:24
canceled;
theorem :: EXTREAL2:25
canceled;
theorem :: EXTREAL2:26
canceled;
theorem :: EXTREAL2:27
canceled;
theorem :: EXTREAL2:28
canceled;
theorem :: EXTREAL2:29
canceled;
theorem :: EXTREAL2:30
canceled;
theorem :: EXTREAL2:31
canceled;
theorem :: EXTREAL2:32
canceled;
theorem :: EXTREAL2:33
canceled;
theorem :: EXTREAL2:34
canceled;
theorem :: EXTREAL2:35
canceled;
theorem :: EXTREAL2:36
canceled;
theorem :: EXTREAL2:37
canceled;
theorem :: EXTREAL2:38
canceled;
theorem :: EXTREAL2:39
canceled;
theorem :: EXTREAL2:40
canceled;
theorem :: EXTREAL2:41
canceled;
theorem :: EXTREAL2:42
canceled;
theorem :: EXTREAL2:43
canceled;
theorem :: EXTREAL2:44
canceled;
theorem :: EXTREAL2:45
canceled;
theorem :: EXTREAL2:46
canceled;
theorem :: EXTREAL2:47
canceled;
theorem :: EXTREAL2:48
canceled;
theorem Th49: :: EXTREAL2:49
theorem :: EXTREAL2:50
theorem Th51: :: EXTREAL2:51
theorem Th52: :: EXTREAL2:52
theorem :: EXTREAL2:53
theorem :: EXTREAL2:54
theorem Th55: :: EXTREAL2:55
theorem :: EXTREAL2:56
theorem Th57: :: EXTREAL2:57
theorem Th58: :: EXTREAL2:58
theorem Th59: :: EXTREAL2:59
theorem Th60: :: EXTREAL2:60
theorem Th61: :: EXTREAL2:61
theorem Th62: :: EXTREAL2:62
theorem :: EXTREAL2:63
theorem :: EXTREAL2:64
theorem :: EXTREAL2:65
theorem Th66: :: EXTREAL2:66
theorem Th67: :: EXTREAL2:67
theorem Th68: :: EXTREAL2:68
theorem :: EXTREAL2:69
theorem :: EXTREAL2:70
theorem :: EXTREAL2:71
theorem :: EXTREAL2:72
theorem :: EXTREAL2:73
theorem :: EXTREAL2:74
canceled;
theorem :: EXTREAL2:75
canceled;
theorem :: EXTREAL2:76
canceled;
theorem :: EXTREAL2:77
canceled;
theorem :: EXTREAL2:78
canceled;
theorem :: EXTREAL2:79
canceled;
theorem :: EXTREAL2:80
theorem :: EXTREAL2:81
canceled;
theorem :: EXTREAL2:82
canceled;
theorem :: EXTREAL2:83
canceled;
theorem :: EXTREAL2:84
canceled;
theorem :: EXTREAL2:85
canceled;
theorem :: EXTREAL2:86
canceled;
theorem :: EXTREAL2:87
canceled;
theorem :: EXTREAL2:88
canceled;
theorem :: EXTREAL2:89
canceled;
theorem :: EXTREAL2:90
canceled;
theorem :: EXTREAL2:91
theorem :: EXTREAL2:92
canceled;
theorem :: EXTREAL2:93
canceled;
theorem :: EXTREAL2:94
canceled;
theorem :: EXTREAL2:95
canceled;
theorem :: EXTREAL2:96
canceled;
theorem :: EXTREAL2:97
canceled;
theorem :: EXTREAL2:98
canceled;
theorem :: EXTREAL2:99
canceled;
theorem :: EXTREAL2:100
theorem Th101: :: EXTREAL2:101
theorem :: EXTREAL2:102