:: Infimum and Supremum of the Set of Real Numbers. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: SUPINF_1:1
:: deftheorem SUPINF_1:def 1 :
canceled;
:: deftheorem Def2 defines +Inf-like SUPINF_1:def 2 :
theorem :: SUPINF_1:2
canceled;
theorem :: SUPINF_1:3
canceled;
theorem :: SUPINF_1:4
theorem :: SUPINF_1:5
canceled;
theorem :: SUPINF_1:6
:: deftheorem SUPINF_1:def 3 :
canceled;
:: deftheorem Def4 defines -Inf-like SUPINF_1:def 4 :
theorem :: SUPINF_1:7
canceled;
theorem :: SUPINF_1:8
theorem :: SUPINF_1:9
canceled;
theorem :: SUPINF_1:10
canceled;
theorem :: SUPINF_1:11
:: deftheorem SUPINF_1:def 5 :
canceled;
:: deftheorem SUPINF_1:def 6 :
canceled;
:: deftheorem defines <= SUPINF_1:def 7 :
theorem :: SUPINF_1:12
canceled;
theorem :: SUPINF_1:13
canceled;
theorem :: SUPINF_1:14
canceled;
theorem :: SUPINF_1:15
canceled;
theorem :: SUPINF_1:16
canceled;
theorem :: SUPINF_1:17
canceled;
theorem :: SUPINF_1:18
canceled;
theorem :: SUPINF_1:19
canceled;
theorem :: SUPINF_1:20
canceled;
theorem :: SUPINF_1:21
canceled;
theorem :: SUPINF_1:22
canceled;
theorem :: SUPINF_1:23
canceled;
theorem :: SUPINF_1:24
canceled;
theorem :: SUPINF_1:25
canceled;
theorem :: SUPINF_1:26
canceled;
theorem :: SUPINF_1:27
canceled;
theorem :: SUPINF_1:28
canceled;
theorem :: SUPINF_1:29
canceled;
theorem :: SUPINF_1:30
canceled;
theorem :: SUPINF_1:31
canceled;
theorem :: SUPINF_1:32
canceled;
theorem :: SUPINF_1:33
canceled;
theorem :: SUPINF_1:34
canceled;
theorem :: SUPINF_1:35
canceled;
theorem :: SUPINF_1:36
canceled;
theorem :: SUPINF_1:37
canceled;
theorem :: SUPINF_1:38
canceled;
theorem :: SUPINF_1:39
canceled;
theorem :: SUPINF_1:40
theorem :: SUPINF_1:41
:: deftheorem SUPINF_1:def 8 :
canceled;
:: deftheorem SUPINF_1:def 9 :
canceled;
:: deftheorem SUPINF_1:def 10 :
canceled;
:: deftheorem defines bounded_above SUPINF_1:def 11 :
:: deftheorem defines bounded_below SUPINF_1:def 12 :
theorem :: SUPINF_1:42
canceled;
theorem :: SUPINF_1:43
canceled;
theorem :: SUPINF_1:44
canceled;
theorem :: SUPINF_1:45
canceled;
theorem :: SUPINF_1:46
canceled;
theorem :: SUPINF_1:47
canceled;
theorem :: SUPINF_1:48
canceled;
theorem :: SUPINF_1:49
canceled;
theorem :: SUPINF_1:50
canceled;
:: deftheorem SUPINF_1:def 13 :
canceled;
:: deftheorem Def14 defines SetMajorant SUPINF_1:def 14 :
theorem :: SUPINF_1:51
canceled;
theorem :: SUPINF_1:52
canceled;
theorem :: SUPINF_1:53
:: deftheorem Def15 defines SetMinorant SUPINF_1:def 15 :
theorem :: SUPINF_1:54
canceled;
theorem :: SUPINF_1:55
canceled;
theorem :: SUPINF_1:56
canceled;
theorem :: SUPINF_1:57
theorem :: SUPINF_1:58
canceled;
theorem :: SUPINF_1:59
canceled;
theorem :: SUPINF_1:60
canceled;
theorem :: SUPINF_1:61
canceled;
theorem :: SUPINF_1:62
canceled;
theorem :: SUPINF_1:63
canceled;
theorem :: SUPINF_1:64
canceled;
theorem :: SUPINF_1:65
canceled;
theorem :: SUPINF_1:66
canceled;
theorem :: SUPINF_1:67
canceled;
theorem :: SUPINF_1:68
canceled;
theorem :: SUPINF_1:69
canceled;
theorem :: SUPINF_1:70
canceled;
theorem :: SUPINF_1:71
canceled;
theorem :: SUPINF_1:72
canceled;
theorem :: SUPINF_1:73
canceled;
theorem :: SUPINF_1:74
canceled;
theorem :: SUPINF_1:75
canceled;
theorem :: SUPINF_1:76
canceled;
theorem :: SUPINF_1:77
canceled;
theorem :: SUPINF_1:78
canceled;
theorem :: SUPINF_1:79
canceled;
theorem :: SUPINF_1:80
canceled;
theorem :: SUPINF_1:81
canceled;
theorem :: SUPINF_1:82
theorem :: SUPINF_1:83
canceled;
theorem :: SUPINF_1:84
canceled;
theorem :: SUPINF_1:85
canceled;
theorem :: SUPINF_1:86
canceled;
theorem :: SUPINF_1:87
canceled;
theorem :: SUPINF_1:88
canceled;
theorem :: SUPINF_1:89
canceled;
theorem :: SUPINF_1:90
canceled;
theorem :: SUPINF_1:91
canceled;
theorem :: SUPINF_1:92
canceled;
theorem :: SUPINF_1:93
canceled;
theorem :: SUPINF_1:94
canceled;
theorem :: SUPINF_1:95
canceled;
theorem :: SUPINF_1:96
canceled;
theorem :: SUPINF_1:97
canceled;
theorem :: SUPINF_1:98
canceled;
theorem :: SUPINF_1:99
canceled;
theorem :: SUPINF_1:100
canceled;
theorem :: SUPINF_1:101
canceled;
theorem :: SUPINF_1:102
canceled;
theorem :: SUPINF_1:103
canceled;
theorem :: SUPINF_1:104
canceled;
theorem :: SUPINF_1:105
canceled;
theorem :: SUPINF_1:106
canceled;
theorem :: SUPINF_1:107
canceled;
theorem :: SUPINF_1:108
canceled;
:: deftheorem SUPINF_1:def 16 :
canceled;
:: deftheorem SUPINF_1:def 17 :
canceled;
:: deftheorem SUPINF_1:def 18 :
canceled;
:: deftheorem Def19 defines SUP SUPINF_1:def 19 :
theorem :: SUPINF_1:109
canceled;
theorem :: SUPINF_1:110
canceled;
theorem :: SUPINF_1:111
canceled;
theorem Th112: :: SUPINF_1:112
theorem Th113: :: SUPINF_1:113
theorem :: SUPINF_1:114
:: deftheorem Def20 defines INF SUPINF_1:def 20 :
theorem :: SUPINF_1:115
canceled;
theorem :: SUPINF_1:116
canceled;
theorem Th117: :: SUPINF_1:117
theorem Th118: :: SUPINF_1:118
theorem :: SUPINF_1:119