:: Collective Operations on Number-Membered Sets
:: by Artur Korni{\l}owicz
::
:: Received December 19, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem defines -- MEMBER_1:def 1 :
theorem Th1: :: MEMBER_1:1
theorem Th2: :: MEMBER_1:2
Lm1:
for F, G being ext-real-membered set st F c= G holds
-- F c= -- G
theorem Th3: :: MEMBER_1:3
theorem :: MEMBER_1:4
theorem Th5: :: MEMBER_1:5
theorem Th6: :: MEMBER_1:6
theorem Th7: :: MEMBER_1:7
theorem Th8: :: MEMBER_1:8
theorem Th9: :: MEMBER_1:9
theorem Th10: :: MEMBER_1:10
:: deftheorem defines -- MEMBER_1:def 2 :
theorem Th11: :: MEMBER_1:11
theorem Th12: :: MEMBER_1:12
Lm2:
for A, B being complex-membered set st A c= B holds
-- A c= -- B
theorem Th13: :: MEMBER_1:13
theorem :: MEMBER_1:14
theorem Th15: :: MEMBER_1:15
theorem Th16: :: MEMBER_1:16
theorem Th17: :: MEMBER_1:17
theorem Th18: :: MEMBER_1:18
theorem Th19: :: MEMBER_1:19
theorem Th20: :: MEMBER_1:20
:: deftheorem defines "" MEMBER_1:def 3 :
theorem Th21: :: MEMBER_1:21
theorem :: MEMBER_1:22
theorem Th23: :: MEMBER_1:23
theorem Th24: :: MEMBER_1:24
theorem :: MEMBER_1:25
theorem Th26: :: MEMBER_1:26
theorem Th27: :: MEMBER_1:27
:: deftheorem defines "" MEMBER_1:def 4 :
theorem Th28: :: MEMBER_1:28
theorem Th29: :: MEMBER_1:29
Lm3:
for A, B being complex-membered set st A c= B holds
A "" c= B ""
theorem Th30: :: MEMBER_1:30
theorem :: MEMBER_1:31
theorem Th32: :: MEMBER_1:32
theorem Th33: :: MEMBER_1:33
theorem Th34: :: MEMBER_1:34
theorem Th35: :: MEMBER_1:35
theorem Th36: :: MEMBER_1:36
theorem Th37: :: MEMBER_1:37
theorem Th38: :: MEMBER_1:38
:: deftheorem defines ++ MEMBER_1:def 5 :
theorem Th39: :: MEMBER_1:39
theorem :: MEMBER_1:40
theorem Th41: :: MEMBER_1:41
theorem Th42: :: MEMBER_1:42
theorem Th43: :: MEMBER_1:43
theorem Th44: :: MEMBER_1:44
theorem Th45: :: MEMBER_1:45
:: deftheorem defines ++ MEMBER_1:def 6 :
theorem Th46: :: 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
theorem Th52: :: MEMBER_1:52
theorem Th53: :: MEMBER_1:53
:: deftheorem defines -- MEMBER_1:def 7 :
theorem Th54: :: MEMBER_1:54
theorem Th55: :: MEMBER_1:55
theorem :: MEMBER_1:56
theorem :: MEMBER_1:57
theorem :: MEMBER_1:58
Lm4:
for F, G being ext-real-membered set holds -- (F ++ G) = (-- F) ++ (-- G)
theorem :: MEMBER_1:59
theorem Th60: :: MEMBER_1:60
theorem :: MEMBER_1:61
theorem :: MEMBER_1:62
theorem :: MEMBER_1:63
theorem :: MEMBER_1:64
:: deftheorem defines -- MEMBER_1:def 8 :
theorem Th65: :: MEMBER_1:65
theorem Th66: :: MEMBER_1:66
theorem Th67: :: MEMBER_1:67
Lm5:
for A, B being complex-membered set holds -- (A ++ B) = (-- A) ++ (-- B)
theorem :: MEMBER_1:68
theorem :: MEMBER_1:69
theorem :: MEMBER_1:70
theorem Th71: :: MEMBER_1:71
theorem :: MEMBER_1:72
theorem :: MEMBER_1:73
theorem :: MEMBER_1:74
theorem Th75: :: MEMBER_1:75
theorem :: MEMBER_1:76
theorem :: MEMBER_1:77
theorem :: MEMBER_1:78
:: deftheorem defines ** MEMBER_1:def 9 :
theorem Th79: :: MEMBER_1:79
theorem Th80: :: MEMBER_1:80
theorem Th81: :: MEMBER_1:81
theorem Th82: :: MEMBER_1:82
theorem Th83: :: MEMBER_1:83
theorem :: MEMBER_1:84
theorem Th85: :: MEMBER_1:85
theorem Th86: :: MEMBER_1:86
theorem Th87: :: MEMBER_1:87
theorem Th88: :: MEMBER_1:88
:: deftheorem defines ** MEMBER_1:def 10 :
theorem Th89: :: MEMBER_1:89
theorem Th90: :: MEMBER_1:90
theorem :: MEMBER_1:91
theorem Th92: :: MEMBER_1:92
theorem Th93: :: MEMBER_1:93
theorem Th94: :: MEMBER_1:94
theorem Th95: :: MEMBER_1:95
theorem Th96: :: MEMBER_1:96
theorem Th97: :: MEMBER_1:97
theorem Th98: :: MEMBER_1:98
theorem Th99: :: MEMBER_1:99
theorem Th100: :: MEMBER_1:100
:: deftheorem defines /// MEMBER_1:def 11 :
theorem Th101: :: MEMBER_1:101
theorem Th102: :: MEMBER_1:102
theorem :: MEMBER_1:103
theorem :: MEMBER_1:104
theorem :: MEMBER_1:105
theorem :: MEMBER_1:106
theorem :: MEMBER_1:107
theorem :: 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
:: deftheorem defines /// MEMBER_1:def 12 :
theorem Th115: :: MEMBER_1:115
theorem Th116: :: MEMBER_1:116
theorem :: MEMBER_1:117
theorem :: MEMBER_1:118
theorem :: MEMBER_1:119
theorem :: MEMBER_1:120
theorem :: MEMBER_1:121
theorem :: 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
:: deftheorem defines ++ MEMBER_1:def 13 :
theorem Th132: :: MEMBER_1:132
theorem Th133: :: MEMBER_1:133
theorem Th134: :: MEMBER_1:134
theorem Th135: :: MEMBER_1:135
theorem :: MEMBER_1:136
theorem Th137: :: MEMBER_1:137
theorem Th138: :: MEMBER_1:138
theorem Th139: :: MEMBER_1:139
theorem Th140: :: MEMBER_1:140
:: deftheorem defines ++ MEMBER_1:def 14 :
theorem Th141: :: MEMBER_1:141
theorem Th142: :: MEMBER_1:142
theorem Th143: :: MEMBER_1:143
theorem Th144: :: MEMBER_1:144
theorem :: MEMBER_1:145
theorem :: MEMBER_1:146
theorem :: MEMBER_1:147
theorem :: MEMBER_1:148
theorem Th149: :: MEMBER_1:149
theorem Th150: :: MEMBER_1:150
theorem Th151: :: MEMBER_1:151
:: deftheorem defines -- MEMBER_1:def 15 :
theorem Th152: :: MEMBER_1:152
theorem Th153: :: MEMBER_1:153
theorem Th154: :: MEMBER_1:154
theorem Th155: :: MEMBER_1:155
theorem :: MEMBER_1:156
theorem Th157: :: MEMBER_1:157
theorem Th158: :: MEMBER_1:158
theorem Th159: :: MEMBER_1:159
:: deftheorem defines -- MEMBER_1:def 16 :
theorem Th160: :: MEMBER_1:160
theorem Th161: :: MEMBER_1:161
theorem Th162: :: MEMBER_1:162
theorem Th163: :: MEMBER_1:163
theorem :: MEMBER_1:164
theorem Th165: :: MEMBER_1:165
theorem Th166: :: MEMBER_1:166
theorem Th167: :: MEMBER_1:167
:: deftheorem defines -- MEMBER_1:def 17 :
theorem Th168: :: MEMBER_1:168
theorem Th169: :: MEMBER_1:169
theorem :: MEMBER_1:170
theorem :: MEMBER_1:171
theorem :: MEMBER_1:172
theorem :: MEMBER_1:173
theorem :: MEMBER_1:174
theorem :: MEMBER_1:175
:: deftheorem defines -- MEMBER_1:def 18 :
theorem Th176: :: MEMBER_1:176
theorem Th177: :: MEMBER_1:177
theorem Th178: :: MEMBER_1:178
theorem Th179: :: MEMBER_1:179
theorem :: MEMBER_1:180
theorem :: MEMBER_1:181
theorem :: MEMBER_1:182
theorem :: MEMBER_1:183
theorem :: MEMBER_1:184
theorem :: MEMBER_1:185
:: deftheorem defines ** MEMBER_1:def 19 :
theorem Th186: :: MEMBER_1:186
theorem Th187: :: MEMBER_1:187
theorem Th188: :: MEMBER_1:188
theorem :: MEMBER_1:189
theorem Th190: :: MEMBER_1:190
theorem Th191: :: MEMBER_1:191
theorem :: MEMBER_1:192
:: deftheorem defines ** MEMBER_1:def 20 :
theorem Th193: :: MEMBER_1:193
theorem Th194: :: MEMBER_1:194
theorem Th195: :: MEMBER_1:195
theorem Th196: :: MEMBER_1:196
theorem :: MEMBER_1:197
theorem Th198: :: MEMBER_1:198
theorem Th199: :: MEMBER_1:199
theorem Th200: :: MEMBER_1:200
theorem Th201: :: MEMBER_1:201
theorem :: MEMBER_1:202
theorem :: MEMBER_1:203
theorem :: MEMBER_1:204
theorem :: MEMBER_1:205
theorem :: MEMBER_1:206
theorem :: MEMBER_1:207
theorem Th208: :: MEMBER_1:208
theorem :: MEMBER_1:209
:: deftheorem defines /// MEMBER_1:def 21 :
theorem Th210: :: MEMBER_1:210
theorem Th211: :: MEMBER_1:211
theorem :: MEMBER_1:212
:: deftheorem defines /// MEMBER_1:def 22 :
theorem Th213: :: MEMBER_1:213
theorem Th214: :: MEMBER_1:214
theorem Th215: :: MEMBER_1:215
theorem Th216: :: MEMBER_1:216
theorem :: MEMBER_1:217
theorem :: MEMBER_1:218
theorem :: MEMBER_1:219
theorem :: MEMBER_1:220
theorem :: MEMBER_1:221
theorem :: MEMBER_1:222
:: deftheorem defines /// MEMBER_1:def 23 :
theorem Th223: :: MEMBER_1:223
theorem Th224: :: MEMBER_1:224
theorem :: MEMBER_1:225
:: deftheorem defines /// MEMBER_1:def 24 :
theorem Th226: :: MEMBER_1:226
theorem Th227: :: MEMBER_1:227
theorem Th228: :: MEMBER_1:228
theorem Th229: :: MEMBER_1:229
theorem :: MEMBER_1:230
theorem :: MEMBER_1:231
theorem :: MEMBER_1:232
theorem :: MEMBER_1:233
theorem Th234: :: MEMBER_1:234
theorem :: MEMBER_1:235