:: Collective Operations on Number-Membered Sets
:: by Artur Korni{\l}owicz
::
:: Received December 19, 2008
:: Copyright (c) 2008 Association of Mizar Users
Lm1:
for f, g being ext-real number holds - (f + g) = (- f) - g
theorem Th1: :: MEMBER_1:1
theorem Th2: :: MEMBER_1:2
theorem Th3: :: MEMBER_1:3
theorem Th4: :: MEMBER_1:4
theorem Th5: :: MEMBER_1:5
theorem Th6: :: MEMBER_1:6
:: deftheorem defines -- MEMBER_1:def 1 :
theorem Th7: :: MEMBER_1:7
theorem Th8: :: MEMBER_1:8
Lm2:
for F, G being ext-real-membered set st F c= G holds
-- F c= -- G
theorem Th9: :: MEMBER_1:9
theorem :: MEMBER_1:10
theorem Th11: :: MEMBER_1:11
theorem Th12: :: MEMBER_1:12
theorem Th13: :: MEMBER_1:13
theorem Th14: :: MEMBER_1:14
theorem Th15: :: MEMBER_1:15
theorem Th16: :: MEMBER_1:16
:: deftheorem defines -- MEMBER_1:def 2 :
theorem Th17: :: MEMBER_1:17
theorem Th18: :: MEMBER_1:18
Lm3:
for A, B being complex-membered set st A c= B holds
-- A c= -- B
theorem Th19: :: MEMBER_1:19
theorem :: MEMBER_1:20
theorem Th21: :: MEMBER_1:21
theorem Th22: :: MEMBER_1:22
theorem Th23: :: MEMBER_1:23
theorem Th24: :: MEMBER_1:24
theorem Th25: :: MEMBER_1:25
theorem Th26: :: MEMBER_1:26
:: deftheorem defines "" MEMBER_1:def 3 :
theorem Th27: :: MEMBER_1:27
theorem :: MEMBER_1:28
theorem Th29: :: MEMBER_1:29
theorem Th30: :: MEMBER_1:30
theorem :: MEMBER_1:31
theorem Th32: :: MEMBER_1:32
theorem Th33: :: MEMBER_1:33
:: deftheorem defines "" MEMBER_1:def 4 :
theorem Th34: :: MEMBER_1:34
theorem Th35: :: MEMBER_1:35
Lm4:
for A, B being complex-membered set st A c= B holds
A "" c= B ""
theorem Th36: :: MEMBER_1:36
theorem :: MEMBER_1:37
theorem Th38: :: MEMBER_1:38
theorem Th39: :: MEMBER_1:39
theorem Th40: :: MEMBER_1:40
theorem Th41: :: MEMBER_1:41
theorem Th42: :: MEMBER_1:42
theorem Th43: :: MEMBER_1:43
theorem Th44: :: MEMBER_1:44
:: deftheorem defines ++ MEMBER_1:def 5 :
theorem Th45: :: MEMBER_1:45
theorem :: MEMBER_1:46
theorem Th47: :: MEMBER_1:47
theorem Th48: :: MEMBER_1:48
theorem Th49: :: MEMBER_1:49
theorem Th50: :: MEMBER_1:50
theorem Th51: :: MEMBER_1:51
:: deftheorem defines ++ MEMBER_1:def 6 :
theorem Th52: :: MEMBER_1:52
theorem Th53: :: MEMBER_1:53
theorem Th54: :: MEMBER_1:54
theorem Th55: :: MEMBER_1:55
theorem Th56: :: MEMBER_1:56
theorem Th57: :: MEMBER_1:57
theorem Th58: :: MEMBER_1:58
theorem Th59: :: MEMBER_1:59
:: deftheorem defines -- MEMBER_1:def 7 :
theorem Th60: :: MEMBER_1:60
theorem Th61: :: MEMBER_1:61
theorem :: MEMBER_1:62
theorem :: MEMBER_1:63
theorem :: MEMBER_1:64
Lm5:
for F, G being ext-real-membered set holds -- (F ++ G) = (-- F) ++ (-- G)
theorem :: MEMBER_1:65
theorem Th66: :: MEMBER_1:66
theorem :: MEMBER_1:67
theorem :: MEMBER_1:68
theorem :: MEMBER_1:69
theorem :: MEMBER_1:70
:: deftheorem defines -- MEMBER_1:def 8 :
theorem Th71: :: MEMBER_1:71
theorem Th72: :: MEMBER_1:72
theorem Th73: :: MEMBER_1:73
Lm6:
for A, B being complex-membered set holds -- (A ++ B) = (-- A) ++ (-- B)
theorem :: MEMBER_1:74
theorem :: MEMBER_1:75
theorem :: MEMBER_1:76
theorem Th77: :: MEMBER_1:77
theorem :: MEMBER_1:78
theorem :: MEMBER_1:79
theorem :: MEMBER_1:80
theorem Th81: :: MEMBER_1:81
theorem :: MEMBER_1:82
theorem :: MEMBER_1:83
theorem :: MEMBER_1:84
:: deftheorem defines ** MEMBER_1:def 9 :
theorem Th85: :: MEMBER_1:85
theorem Th86: :: MEMBER_1:86
theorem Th87: :: MEMBER_1:87
theorem Th88: :: MEMBER_1:88
theorem Th89: :: MEMBER_1:89
theorem :: MEMBER_1:90
theorem Th91: :: MEMBER_1:91
theorem Th92: :: MEMBER_1:92
theorem Th93: :: MEMBER_1:93
theorem Th94: :: MEMBER_1:94
:: deftheorem defines ** MEMBER_1:def 10 :
theorem Th95: :: MEMBER_1:95
theorem Th96: :: MEMBER_1:96
theorem :: MEMBER_1:97
theorem Th98: :: MEMBER_1:98
theorem Th99: :: MEMBER_1:99
theorem Th100: :: MEMBER_1:100
theorem Th101: :: MEMBER_1:101
theorem Th102: :: MEMBER_1:102
theorem Th103: :: MEMBER_1:103
theorem Th104: :: MEMBER_1:104
theorem Th105: :: MEMBER_1:105
theorem Th106: :: MEMBER_1:106
:: deftheorem defines /// MEMBER_1:def 11 :
theorem Th107: :: MEMBER_1:107
theorem Th108: :: MEMBER_1:108
theorem :: MEMBER_1:109
theorem :: MEMBER_1:110
theorem :: MEMBER_1:111
theorem :: MEMBER_1:112
theorem :: MEMBER_1:113
theorem :: MEMBER_1:114
theorem :: MEMBER_1:115
theorem :: MEMBER_1:116
theorem :: MEMBER_1:117
theorem :: MEMBER_1:118
theorem :: MEMBER_1:119
theorem :: MEMBER_1:120
:: deftheorem defines /// MEMBER_1:def 12 :
theorem Th121: :: MEMBER_1:121
theorem Th122: :: MEMBER_1:122
theorem :: MEMBER_1:123
theorem :: MEMBER_1:124
theorem :: MEMBER_1:125
theorem :: MEMBER_1:126
theorem :: MEMBER_1:127
theorem :: MEMBER_1:128
theorem :: MEMBER_1:129
theorem :: MEMBER_1:130
theorem :: MEMBER_1:131
theorem :: MEMBER_1:132
theorem :: MEMBER_1:133
theorem :: MEMBER_1:134
theorem :: MEMBER_1:135
theorem :: MEMBER_1:136
theorem :: MEMBER_1:137
:: deftheorem defines ++ MEMBER_1:def 13 :
theorem Th138: :: MEMBER_1:138
theorem Th139: :: MEMBER_1:139
theorem Th140: :: MEMBER_1:140
theorem Th141: :: MEMBER_1:141
theorem :: MEMBER_1:142
theorem Th143: :: MEMBER_1:143
theorem Th144: :: MEMBER_1:144
theorem Th145: :: MEMBER_1:145
theorem Th146: :: MEMBER_1:146
:: deftheorem defines ++ MEMBER_1:def 14 :
theorem Th147: :: MEMBER_1:147
theorem Th148: :: MEMBER_1:148
theorem Th149: :: MEMBER_1:149
theorem Th150: :: MEMBER_1:150
theorem :: MEMBER_1:151
theorem :: MEMBER_1:152
theorem :: MEMBER_1:153
theorem :: MEMBER_1:154
theorem Th155: :: MEMBER_1:155
theorem Th156: :: MEMBER_1:156
theorem Th157: :: MEMBER_1:157
:: deftheorem defines -- MEMBER_1:def 15 :
theorem Th158: :: MEMBER_1:158
theorem Th159: :: MEMBER_1:159
theorem Th160: :: MEMBER_1:160
theorem Th161: :: MEMBER_1:161
theorem :: MEMBER_1:162
theorem Th163: :: MEMBER_1:163
theorem Th164: :: MEMBER_1:164
theorem Th165: :: MEMBER_1:165
:: deftheorem defines -- MEMBER_1:def 16 :
theorem Th166: :: MEMBER_1:166
theorem Th167: :: MEMBER_1:167
theorem Th168: :: MEMBER_1:168
theorem Th169: :: MEMBER_1:169
theorem :: MEMBER_1:170
theorem Th171: :: MEMBER_1:171
theorem Th172: :: MEMBER_1:172
theorem Th173: :: MEMBER_1:173
:: deftheorem defines -- MEMBER_1:def 17 :
theorem Th174: :: MEMBER_1:174
theorem Th175: :: MEMBER_1:175
theorem :: MEMBER_1:176
theorem :: MEMBER_1:177
theorem :: MEMBER_1:178
theorem :: MEMBER_1:179
theorem :: MEMBER_1:180
theorem :: MEMBER_1:181
:: deftheorem defines -- MEMBER_1:def 18 :
theorem Th182: :: MEMBER_1:182
theorem Th183: :: MEMBER_1:183
theorem Th184: :: MEMBER_1:184
theorem Th185: :: MEMBER_1:185
theorem :: MEMBER_1:186
theorem :: MEMBER_1:187
theorem :: MEMBER_1:188
theorem :: MEMBER_1:189
theorem :: MEMBER_1:190
theorem :: MEMBER_1:191
:: deftheorem defines ** MEMBER_1:def 19 :
theorem Th192: :: MEMBER_1:192
theorem Th193: :: MEMBER_1:193
theorem Th194: :: MEMBER_1:194
theorem :: MEMBER_1:195
theorem Th196: :: MEMBER_1:196
theorem Th197: :: MEMBER_1:197
theorem :: MEMBER_1:198
:: deftheorem defines ** MEMBER_1:def 20 :
theorem Th199: :: MEMBER_1:199
theorem Th200: :: MEMBER_1:200
theorem Th201: :: MEMBER_1:201
theorem Th202: :: MEMBER_1:202
theorem :: MEMBER_1:203
theorem Th204: :: MEMBER_1:204
theorem Th205: :: MEMBER_1:205
theorem Th206: :: MEMBER_1:206
theorem Th207: :: MEMBER_1:207
theorem :: MEMBER_1:208
theorem :: MEMBER_1:209
theorem :: MEMBER_1:210
theorem :: MEMBER_1:211
theorem :: MEMBER_1:212
theorem :: MEMBER_1:213
theorem Th214: :: MEMBER_1:214
theorem :: MEMBER_1:215
:: deftheorem defines /// MEMBER_1:def 21 :
theorem Th216: :: MEMBER_1:216
theorem Th217: :: MEMBER_1:217
theorem :: MEMBER_1:218
:: deftheorem defines /// MEMBER_1:def 22 :
theorem Th219: :: MEMBER_1:219
theorem Th220: :: MEMBER_1:220
theorem Th221: :: MEMBER_1:221
theorem Th222: :: MEMBER_1:222
theorem :: MEMBER_1:223
theorem :: MEMBER_1:224
theorem :: MEMBER_1:225
theorem :: MEMBER_1:226
theorem :: MEMBER_1:227
theorem :: MEMBER_1:228
:: deftheorem defines /// MEMBER_1:def 23 :
theorem Th229: :: MEMBER_1:229
theorem Th230: :: MEMBER_1:230
theorem :: MEMBER_1:231
:: deftheorem defines /// MEMBER_1:def 24 :
theorem Th232: :: MEMBER_1:232
theorem Th233: :: MEMBER_1:233
theorem Th234: :: MEMBER_1:234
theorem Th235: :: MEMBER_1:235
theorem :: MEMBER_1:236
theorem :: MEMBER_1:237
theorem :: MEMBER_1:238
theorem :: MEMBER_1:239
theorem Th240: :: MEMBER_1:240
theorem :: MEMBER_1:241