:: Collective Operations on Number-Membered Sets
:: by Artur Korni{\l}owicz
::
:: Received December 19, 2008
:: Copyright (c) 2008-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, MEMBERED, XCMPLX_0, XXREAL_0, ARYTM_1,
RELAT_1, TARSKI, XBOOLE_0, ARYTM_3, RAT_1, INT_1, CARD_1, MEMBER_1,
NAT_1, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, RAT_1, INT_1, MEMBERED, XXREAL_3, XXREAL_0;
constructors XCMPLX_0, RAT_1, MEMBERED, ENUMSET1, BINOP_2, XXREAL_3;
registrations XREAL_0, INT_1, RAT_1, ORDINAL1, MEMBERED, XCMPLX_0, NAT_1,
XXREAL_3, XBOOLE_0;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin
reserve w, w1, w2 for Element of ExtREAL;
reserve c, c1, c2 for Complex;
reserve A, B, C, D for complex-membered set;
reserve F, G, H, I for ext-real-membered set;
reserve a, b, s, t, z for Complex;
reserve f, g, h, i, j for ExtReal;
reserve r for Real;
reserve e for set;
definition
let w;
redefine func -w -> Element of ExtREAL;
redefine func w" -> Element of ExtREAL;
let w1;
redefine func w*w1 -> Element of ExtREAL;
end;
registration
let a, b, c, d be Complex;
cluster {a,b,c,d} -> complex-membered;
end;
registration
let a, b, c, d be ExtReal;
cluster {a,b,c,d} -> ext-real-membered;
end;
definition
let F be ext-real-membered set;
func --F -> ext-real-membered set equals
:: MEMBER_1:def 1
{-w: w in F};
involutiveness;
end;
theorem :: MEMBER_1:1
f in F iff -f in --F;
theorem :: MEMBER_1:2
-f in F iff f in --F;
registration
let F be empty set;
cluster --F -> empty;
end;
registration
let F be ext-real-membered non empty set;
cluster --F -> non empty;
end;
theorem :: MEMBER_1:3
F c= G iff --F c= --G;
theorem :: MEMBER_1:4
--F = --G implies F = G;
theorem :: MEMBER_1:5
-- (F \/ G) = (--F) \/ (--G);
theorem :: MEMBER_1:6
-- (F /\ G) = (--F) /\ (--G);
theorem :: MEMBER_1:7
-- (F \ G) = (--F) \ (--G);
theorem :: MEMBER_1:8
-- (F \+\ G) = (--F) \+\ (--G);
theorem :: MEMBER_1:9
--{f} = {-f};
theorem :: MEMBER_1:10
--{f,g} = {-f,-g};
definition
let A be complex-membered set;
func --A -> complex-membered set equals
:: MEMBER_1:def 2
{-c: c in A};
involutiveness;
end;
theorem :: MEMBER_1:11
a in A iff -a in --A;
theorem :: MEMBER_1:12
-a in A iff a in --A;
registration
let A be empty set;
cluster --A -> empty;
end;
registration
let A be complex-membered non empty set;
cluster --A -> non empty;
end;
registration
let A be real-membered set;
cluster --A -> real-membered;
end;
registration
let A be rational-membered set;
cluster --A -> rational-membered;
end;
registration
let A be integer-membered set;
cluster --A -> integer-membered;
end;
registration
let A be real-membered set, F be ext-real-membered set;
identify --A with --F when A = F;
end;
theorem :: MEMBER_1:13
A c= B iff --A c= --B;
theorem :: MEMBER_1:14
--A = --B implies A = B;
theorem :: MEMBER_1:15
-- (A \/ B) = (--A) \/ (--B);
theorem :: MEMBER_1:16
-- (A /\ B) = (--A) /\ (--B);
theorem :: MEMBER_1:17
-- (A \ B) = (--A) \ (--B);
theorem :: MEMBER_1:18
-- (A \+\ B) = (--A) \+\ (--B);
theorem :: MEMBER_1:19
--{a} = {-a};
theorem :: MEMBER_1:20
--{a,b} = {-a,-b};
definition
let F be ext-real-membered set;
func F"" -> ext-real-membered set equals
:: MEMBER_1:def 3
{w": w in F};
end;
theorem :: MEMBER_1:21
f in F implies f" in F"";
registration
let F be empty set;
cluster F"" -> empty;
end;
registration
let F be ext-real-membered non empty set;
cluster F"" -> non empty;
end;
theorem :: MEMBER_1:22
F c= G implies F"" c= G"";
theorem :: MEMBER_1:23
(F \/ G)"" = (F"") \/ (G"");
theorem :: MEMBER_1:24
(F /\ G)"" c= (F"") /\ (G"");
theorem :: MEMBER_1:25
--(F"") = (--F)"";
theorem :: MEMBER_1:26
{f}"" = {f"};
theorem :: MEMBER_1:27
{f,g}"" = {f",g"};
definition
let A be complex-membered set;
func A"" -> complex-membered set equals
:: MEMBER_1:def 4
{c": c in A};
involutiveness;
end;
theorem :: MEMBER_1:28
a in A iff a" in A"";
theorem :: MEMBER_1:29
a" in A iff a in A"";
registration
let A be empty set;
cluster A"" -> empty;
end;
registration
let A be complex-membered non empty set;
cluster A"" -> non empty;
end;
registration
let A be real-membered set;
cluster A"" -> real-membered;
end;
registration
let A be rational-membered set;
cluster A"" -> rational-membered;
end;
registration
let A be real-membered set, F be ext-real-membered set;
identify A"" with F"" when A = F;
end;
theorem :: MEMBER_1:30
A c= B iff A"" c= B"";
theorem :: MEMBER_1:31
A"" = B"" implies A = B;
theorem :: MEMBER_1:32
(A \/ B)"" = (A"") \/ (B"");
theorem :: MEMBER_1:33
(A /\ B)"" = (A"") /\ (B"");
theorem :: MEMBER_1:34
(A \ B)"" = (A"") \ (B"");
theorem :: MEMBER_1:35
(A \+\ B)"" = (A"") \+\ (B"");
theorem :: MEMBER_1:36
--(A"") = (--A)"";
theorem :: MEMBER_1:37
{a}"" = {a"};
theorem :: MEMBER_1:38
{a,b}"" = {a",b"};
definition
let F, G be ext-real-membered set;
func F++G -> set equals
:: MEMBER_1:def 5
{w1+w2: w1 in F & w2 in G};
commutativity;
end;
theorem :: MEMBER_1:39
f in F & g in G implies f+g in F++G;
registration
let F be empty set;
let G be ext-real-membered set;
cluster F++G -> empty;
cluster G++F -> empty;
end;
registration
let F, G be ext-real-membered non empty set;
cluster F++G -> non empty;
end;
registration
let F, G be ext-real-membered set;
cluster F++G -> ext-real-membered;
end;
theorem :: MEMBER_1:40
F c= G & H c= I implies F++H c= G++I;
theorem :: MEMBER_1:41
F ++ (G \/ H) = (F++G) \/ (F++H);
theorem :: MEMBER_1:42
F ++ (G /\ H) c= (F++G) /\ (F++H);
theorem :: MEMBER_1:43
{f}++{g} = {f+g};
theorem :: MEMBER_1:44
{f}++{g,h} = {f+g,f+h};
theorem :: MEMBER_1:45
{f,g}++{h,i} = {f+h,f+i,g+h,g+i};
definition
let A, B be complex-membered set;
func A++B -> set equals
:: MEMBER_1:def 6
{c1+c2: c1 in A & c2 in B};
commutativity;
end;
theorem :: MEMBER_1:46
a in A & b in B implies a+b in A++B;
registration
let A be empty set;
let B be complex-membered set;
cluster A++B -> empty;
cluster B++A -> empty;
end;
registration
let A, B be complex-membered non empty set;
cluster A++B -> non empty;
end;
registration
let A, B be complex-membered set;
cluster A++B -> complex-membered;
end;
registration
let A, B be real-membered set;
cluster A++B -> real-membered;
end;
registration
let A, B be rational-membered set;
cluster A++B -> rational-membered;
end;
registration
let A, B be integer-membered set;
cluster A++B -> integer-membered;
end;
registration
let A, B be natural-membered set;
cluster A++B -> natural-membered;
end;
registration
let A, B be real-membered set, F, G be ext-real-membered set;
identify A++B with F++G when A = F, B = G;
end;
theorem :: MEMBER_1:47
A c= B & C c= D implies A++C c= B++D;
theorem :: MEMBER_1:48
A ++ (B \/ C) = (A++B) \/ (A++C);
theorem :: MEMBER_1:49
A ++ (B /\ C) c= (A++B) /\ (A++C);
theorem :: MEMBER_1:50
(A++B)++C = A++(B++C);
theorem :: MEMBER_1:51
{a}++{b} = {a+b};
theorem :: MEMBER_1:52
{a}++{s,t} = {a+s,a+t};
theorem :: MEMBER_1:53
{a,b}++{s,t} = {a+s,a+t,b+s,b+t};
definition
let F, G be ext-real-membered set;
func F--G -> set equals
:: MEMBER_1:def 7
F ++ --G;
end;
theorem :: MEMBER_1:54
F--G = {w1-w2: w1 in F & w2 in G};
theorem :: MEMBER_1:55
f in F & g in G implies f-g in F--G;
registration
let F be empty set;
let G be ext-real-membered set;
cluster F--G -> empty;
cluster G--F -> empty;
end;
registration
let F, G be ext-real-membered non empty set;
cluster F--G -> non empty;
end;
registration
let F, G be ext-real-membered set;
cluster F--G -> ext-real-membered;
end;
theorem :: MEMBER_1:56
F c= G & H c= I implies F--H c= G--I;
theorem :: MEMBER_1:57
F -- (G \/ H) = (F--G) \/ (F--H);
theorem :: MEMBER_1:58
F -- (G /\ H) c= (F--G) /\ (F--H);
theorem :: MEMBER_1:59
--(F++G) = (--F) -- G;
theorem :: MEMBER_1:60
--(F--G) = (--F) ++ G;
theorem :: MEMBER_1:61
{f}--{g} = {f-g};
theorem :: MEMBER_1:62
{f}--{h,i} = {f-h,f-i};
theorem :: MEMBER_1:63
{f,g}--{h} = {f-h,g-h};
theorem :: MEMBER_1:64
{f,g}--{h,i} = {f-h,f-i,g-h,g-i};
definition
let A, B be complex-membered set;
func A--B -> set equals
:: MEMBER_1:def 8
A ++ --B;
end;
theorem :: MEMBER_1:65
A--B = {c1-c2: c1 in A & c2 in B};
theorem :: MEMBER_1:66
a in A & b in B implies a-b in A--B;
registration
let A be empty set;
let B be complex-membered set;
cluster A--B -> empty;
cluster B--A -> empty;
end;
registration
let A, B be complex-membered non empty set;
cluster A--B -> non empty;
end;
registration
let A, B be complex-membered set;
cluster A--B -> complex-membered;
end;
registration
let A, B be real-membered set;
cluster A--B -> real-membered;
end;
registration
let A, B be rational-membered set;
cluster A--B -> rational-membered;
end;
registration
let A, B be integer-membered set;
cluster A--B -> integer-membered;
end;
registration
let A, B be real-membered set, F, G be ext-real-membered set;
identify A--B with F--G when A = F, B = G;
end;
theorem :: MEMBER_1:67
A c= B & C c= D implies A--C c= B--D;
theorem :: MEMBER_1:68
A -- (B \/ C) = (A--B) \/ (A--C);
theorem :: MEMBER_1:69
A -- (B /\ C) c= (A--B) /\ (A--C);
theorem :: MEMBER_1:70
--(A++B) = (--A) -- B;
theorem :: MEMBER_1:71
--(A--B) = (--A) ++ B;
theorem :: MEMBER_1:72
A++(B--C) = A++B--C;
theorem :: MEMBER_1:73
A--(B++C) = A--B--C;
theorem :: MEMBER_1:74
A--(B--C) = A--B++C;
theorem :: MEMBER_1:75
{a}--{b} = {a-b};
theorem :: MEMBER_1:76
{a}--{s,t} = {a-s,a-t};
theorem :: MEMBER_1:77
{a,b}--{s} = {a-s,b-s};
theorem :: MEMBER_1:78
{a,b}--{s,t} = {a-s,a-t,b-s,b-t};
definition
let F, G be ext-real-membered set;
func F**G -> set equals
:: MEMBER_1:def 9
{w1*w2: w1 in F & w2 in G};
commutativity;
end;
registration
let F be empty set;
let G be ext-real-membered set;
cluster F**G -> empty;
cluster G**F -> empty;
end;
registration
let F, G be ext-real-membered set;
cluster F**G -> ext-real-membered;
end;
theorem :: MEMBER_1:79
f in F & g in G implies f*g in F**G;
registration
let F, G be ext-real-membered non empty set;
cluster F**G -> non empty;
end;
theorem :: MEMBER_1:80
(F**G)**H = F**(G**H);
theorem :: MEMBER_1:81
F c= G & H c= I implies F**H c= G**I;
theorem :: MEMBER_1:82
F ** (G \/ H) = (F**G) \/ (F**H);
theorem :: MEMBER_1:83
F ** (G /\ H) c= (F**G) /\ (F**H);
theorem :: MEMBER_1:84
F**--G = --(F**G);
theorem :: MEMBER_1:85
(F**G)"" = (F"") ** (G"");
theorem :: MEMBER_1:86
{f}**{g} = {f*g};
theorem :: MEMBER_1:87
{f}**{h,i} = {f*h,f*i};
theorem :: MEMBER_1:88
{f,g}**{h,i} = {f*h,f*i,g*h,g*i};
definition
let A, B be complex-membered set;
func A**B -> set equals
:: MEMBER_1:def 10
{c1*c2: c1 in A & c2 in B};
commutativity;
end;
theorem :: MEMBER_1:89
a in A & b in B implies a*b in A**B;
registration
let A be empty set;
let B be complex-membered set;
cluster A**B -> empty;
cluster B**A -> empty;
end;
registration
let A, B be complex-membered non empty set;
cluster A**B -> non empty;
end;
registration
let A, B be complex-membered set;
cluster A**B -> complex-membered;
end;
registration
let A, B be real-membered set;
cluster A**B -> real-membered;
end;
registration
let A, B be rational-membered set;
cluster A**B -> rational-membered;
end;
registration
let A, B be integer-membered set;
cluster A**B -> integer-membered;
end;
registration
let A, B be natural-membered set;
cluster A**B -> natural-membered;
end;
registration
let A, B be real-membered set, F, G be ext-real-membered set;
identify A**B with F**G when A = F, B = G;
end;
theorem :: MEMBER_1:90
(A**B)**C = A**(B**C);
theorem :: MEMBER_1:91
A c= B & C c= D implies A**C c= B**D;
theorem :: MEMBER_1:92
A ** (B \/ C) = (A**B) \/ (A**C);
theorem :: MEMBER_1:93
A ** (B /\ C) c= (A**B) /\ (A**C);
theorem :: MEMBER_1:94
A**--B = --(A**B);
theorem :: MEMBER_1:95
A**(B++C) c= A**B ++ A**C;
theorem :: MEMBER_1:96
A**(B--C) c= A**B -- A**C;
theorem :: MEMBER_1:97
(A**B)"" = (A"") ** (B"");
theorem :: MEMBER_1:98
{a}**{b} = {a*b};
theorem :: MEMBER_1:99
{a}**{s,t} = {a*s,a*t};
theorem :: MEMBER_1:100
{a,b}**{s,t} = {a*s,a*t,b*s,b*t};
definition
let F, G be ext-real-membered set;
func F///G -> set equals
:: MEMBER_1:def 11
F**(G"");
end;
theorem :: MEMBER_1:101
F///G = {w1/w2: w1 in F & w2 in G};
theorem :: MEMBER_1:102
f in F & g in G implies f/g in F///G;
registration
let F be empty set;
let G be ext-real-membered set;
cluster F///G -> empty;
cluster G///F -> empty;
end;
registration
let F, G be ext-real-membered non empty set;
cluster F///G -> non empty;
end;
registration
let F, G be ext-real-membered set;
cluster F///G -> ext-real-membered;
end;
theorem :: MEMBER_1:103
F c= G & H c= I implies F///H c= G///I;
theorem :: MEMBER_1:104
(F \/ G) /// H = (F///H) \/ (G///H);
theorem :: MEMBER_1:105
(F /\ G) /// H c= (F///H) /\ (G///H);
theorem :: MEMBER_1:106
F /// (G \/ H) = (F///G) \/ (F///H);
theorem :: MEMBER_1:107
F /// (G /\ H) c= (F///G) /\ (F///H);
theorem :: MEMBER_1:108
(F**G)///H = F**(G///H);
theorem :: MEMBER_1:109
(F///G)**H = (F**H)///G;
theorem :: MEMBER_1:110
(F///G)///H = F///(G**H);
theorem :: MEMBER_1:111
{f}///{g} = {f/g};
theorem :: MEMBER_1:112
{f}///{h,i} = {f/h,f/i};
theorem :: MEMBER_1:113
{f,g}///{h} = {f/h,g/h};
theorem :: MEMBER_1:114
{f,g}///{h,i} = {f/h,f/i,g/h,g/i};
definition
let A, B be complex-membered set;
func A///B -> set equals
:: MEMBER_1:def 12
A**(B"");
end;
theorem :: MEMBER_1:115
A///B = {c1/c2: c1 in A & c2 in B};
theorem :: MEMBER_1:116
a in A & b in B implies a/b in A///B;
registration
let A be empty set;
let B be complex-membered set;
cluster A///B -> empty;
cluster B///A -> empty;
end;
registration
let A, B be complex-membered non empty set;
cluster A///B -> non empty;
end;
registration
let A, B be complex-membered set;
cluster A///B -> complex-membered;
end;
registration
let A, B be real-membered set;
cluster A///B -> real-membered;
end;
registration
let A, B be rational-membered set;
cluster A///B -> rational-membered;
end;
registration
let A, B be real-membered set, F, G be ext-real-membered set;
identify A///B with F///G when A = F, B = G;
end;
theorem :: MEMBER_1:117
A c= B & C c= D implies A///C c= B///D;
theorem :: MEMBER_1:118
A /// (B \/ C) = (A///B) \/ (A///C);
theorem :: MEMBER_1:119
A /// (B /\ C) c= (A///B) /\ (A///C);
theorem :: MEMBER_1:120
A///--B = --(A///B);
theorem :: MEMBER_1:121
(--A)///B = --(A///B);
theorem :: MEMBER_1:122
(A++B)///C c= A///C ++ B///C;
theorem :: MEMBER_1:123
(A--B)///C c= A///C -- B///C;
theorem :: MEMBER_1:124
(A**B)///C = A**(B///C);
theorem :: MEMBER_1:125
(A///B)**C = (A**C)///B;
theorem :: MEMBER_1:126
(A///B)///C = A///(B**C);
theorem :: MEMBER_1:127
A///(B///C) = (A**C)///B;
theorem :: MEMBER_1:128
{a}///{b} = {a/b};
theorem :: MEMBER_1:129
{a}///{s,t} = {a/s,a/t};
theorem :: MEMBER_1:130
{a,b}///{s} = {a/s,b/s};
theorem :: MEMBER_1:131
{a,b}///{s,t} = {a/s,a/t,b/s,b/t};
definition
let F be ext-real-membered set;
let f be ExtReal;
func f++F -> set equals
:: MEMBER_1:def 13
{f}++F;
end;
theorem :: MEMBER_1:132
g in G implies f+g in f++G;
theorem :: MEMBER_1:133
f++F = {f+w: w in F};
theorem :: MEMBER_1:134
e in f++F implies ex w st e = f+w & w in F;
registration
let F be empty set;
let f be ExtReal;
cluster f++F -> empty;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster f++F -> non empty;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster f++F -> ext-real-membered;
end;
theorem :: MEMBER_1:135
r++F c= r++G implies F c= G;
theorem :: MEMBER_1:136
r++F = r++G implies F = G;
theorem :: MEMBER_1:137
r ++ (F /\ G) = (r++F) /\ (r++G);
theorem :: MEMBER_1:138
(f++F) \ (f++G) c= f ++ (F \ G);
theorem :: MEMBER_1:139
r ++ (F \ G) = (r++F) \ (r++G);
theorem :: MEMBER_1:140
r ++ (F \+\ G) = (r++F) \+\ (r++G);
definition
let A be complex-membered set;
let a be Complex;
func a++A -> set equals
:: MEMBER_1:def 14
{a}++A;
end;
theorem :: MEMBER_1:141
b in A implies a+b in a++A;
theorem :: MEMBER_1:142
a++A = {a+c: c in A};
theorem :: MEMBER_1:143
e in a++A implies ex c st e = a+c & c in A;
registration
let A be empty set;
let a be Complex;
cluster a++A -> empty;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster a++A -> non empty;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster a++A -> complex-membered;
end;
registration
let A be real-membered set;
let a be Real;
cluster a++A -> real-membered;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster a++A -> rational-membered;
end;
registration
let A be integer-membered set;
let a be Integer;
cluster a++A -> integer-membered;
end;
registration
let A be natural-membered set;
let a be Nat;
cluster a++A -> natural-membered;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify a++A with f++F when a = f, A = F;
end;
theorem :: MEMBER_1:144
A c= B iff a++A c= a++B;
theorem :: MEMBER_1:145
a++A = a++B implies A = B;
theorem :: MEMBER_1:146
0++A = A;
theorem :: MEMBER_1:147
(a+b)++A = a++(b++A);
theorem :: MEMBER_1:148
a++(A++B) = (a++A)++B;
theorem :: MEMBER_1:149
a ++ (A /\ B) = (a++A) /\ (a++B);
theorem :: MEMBER_1:150
a ++ (A \ B) = (a++A) \ (a++B);
theorem :: MEMBER_1:151
a ++ (A \+\ B) = (a++A) \+\ (a++B);
definition
let F be ext-real-membered set;
let f be ExtReal;
func f--F -> set equals
:: MEMBER_1:def 15
{f}--F;
end;
theorem :: MEMBER_1:152
g in G implies f-g in f--G;
theorem :: MEMBER_1:153
f--F = {f-w: w in F};
theorem :: MEMBER_1:154
e in f--F implies ex w st e = f-w & w in F;
registration
let F be empty set;
let f be ExtReal;
cluster f--F -> empty;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster f--F -> non empty;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster f--F -> ext-real-membered;
end;
theorem :: MEMBER_1:155
r--F c= r--G implies F c= G;
theorem :: MEMBER_1:156
r--F = r--G implies F = G;
theorem :: MEMBER_1:157
r -- (F/\G) = (r--F) /\ (r--G);
theorem :: MEMBER_1:158
r -- (F\G) = (r--F) \ (r--G);
theorem :: MEMBER_1:159
r -- (F\+\G) = (r--F) \+\ (r--G);
definition
let A be complex-membered set;
let a be Complex;
func a--A -> set equals
:: MEMBER_1:def 16
{a}--A;
end;
theorem :: MEMBER_1:160
b in A implies a-b in a--A;
theorem :: MEMBER_1:161
a--A = {a-c: c in A};
theorem :: MEMBER_1:162
e in a--A implies ex c st e = a-c & c in A;
registration
let A be empty set;
let a be Complex;
cluster a--A -> empty;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster a--A -> non empty;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster a--A -> complex-membered;
end;
registration
let A be real-membered set;
let a be Real;
cluster a--A -> real-membered;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster a--A -> rational-membered;
end;
registration
let A be integer-membered set;
let a be Integer;
cluster a--A -> integer-membered;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify a--A with f--F when a = f, A = F;
end;
theorem :: MEMBER_1:163
A c= B iff a--A c= a--B;
theorem :: MEMBER_1:164
a--A = a--B implies A = B;
theorem :: MEMBER_1:165
a -- (A/\B) = (a--A) /\ (a--B);
theorem :: MEMBER_1:166
a -- (A\B) = (a--A) \ (a--B);
theorem :: MEMBER_1:167
a -- (A\+\B) = (a--A) \+\ (a--B);
definition
let F be ext-real-membered set;
let f be ExtReal;
func F--f -> set equals
:: MEMBER_1:def 17
F--{f};
end;
theorem :: MEMBER_1:168
g in G implies g-f in G--f;
theorem :: MEMBER_1:169
F--f = {w-f: w in F};
theorem :: MEMBER_1:170
e in F--f implies ex w st e = w-f & w in F;
registration
let F be empty set;
let f be ExtReal;
cluster F--f -> empty;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster F--f -> non empty;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster F--f -> ext-real-membered;
end;
theorem :: MEMBER_1:171
F -- f = -- (f -- F);
theorem :: MEMBER_1:172
f -- F = -- (F -- f);
theorem :: MEMBER_1:173
(F/\G) -- r = (F--r) /\ (G--r);
theorem :: MEMBER_1:174
(F\G) -- r = (F--r) \ (G--r);
theorem :: MEMBER_1:175
(F\+\G) -- r = (F--r) \+\ (G--r);
definition
let A be complex-membered set;
let a be Complex;
func A--a -> set equals
:: MEMBER_1:def 18
A--{a};
end;
theorem :: MEMBER_1:176
b in A implies b-a in A--a;
theorem :: MEMBER_1:177
A--a = {c-a: c in A};
theorem :: MEMBER_1:178
e in A--a implies ex c st e = c-a & c in A;
registration
let A be empty set;
let a be Complex;
cluster A--a -> empty;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster A--a -> non empty;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster A--a -> complex-membered;
end;
registration
let A be real-membered set;
let a be Real;
cluster A--a -> real-membered;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster A--a -> rational-membered;
end;
registration
let A be integer-membered set;
let a be Integer;
cluster A--a -> integer-membered;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify A--a with F--f when a = f, A = F;
end;
theorem :: MEMBER_1:179
A c= B iff A--a c= B--a;
theorem :: MEMBER_1:180
A--a = B--a implies A = B;
theorem :: MEMBER_1:181
A -- a = -- (a -- A);
theorem :: MEMBER_1:182
a -- A = -- (A -- a);
theorem :: MEMBER_1:183
(A/\B) -- a = (A--a) /\ (B--a);
theorem :: MEMBER_1:184
(A\B) -- a = (A--a) \ (B--a);
theorem :: MEMBER_1:185
(A\+\B) -- a = (A--a) \+\ (B--a);
definition
let F be ext-real-membered set;
let f be ExtReal;
func f**F -> set equals
:: MEMBER_1:def 19
{f}**F;
end;
theorem :: MEMBER_1:186
g in G implies f*g in f**G;
theorem :: MEMBER_1:187
f**F = {f*w: w in F};
theorem :: MEMBER_1:188
e in f**F implies ex w st e = f*w & w in F;
registration
let F be empty set;
let f be ExtReal;
cluster f**F -> empty;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster f**F -> non empty;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster f**F -> ext-real-membered;
end;
theorem :: MEMBER_1:189
r <> 0 implies r ** (F/\G) = (r**F) /\ (r**G);
theorem :: MEMBER_1:190
(f**F) \ (f**G) c= f ** (F \ G);
theorem :: MEMBER_1:191
r <> 0 implies r ** (F\G) = (r**F) \ (r**G);
theorem :: MEMBER_1:192
r <> 0 implies r ** (F\+\G) = (r**F) \+\ (r**G);
definition
let A be complex-membered set;
let a be Complex;
func a**A -> set equals
:: MEMBER_1:def 20
{a}**A;
end;
theorem :: MEMBER_1:193
b in A implies a*b in a**A;
theorem :: MEMBER_1:194
a**A = {a*c: c in A};
theorem :: MEMBER_1:195
e in a**A implies ex c st e = a*c & c in A;
registration
let A be empty set;
let a be Complex;
cluster a**A -> empty;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster a**A -> non empty;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster a**A -> complex-membered;
end;
registration
let A be real-membered set;
let a be Real;
cluster a**A -> real-membered;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster a**A -> rational-membered;
end;
registration
let A be integer-membered set;
let a be Integer;
cluster a**A -> integer-membered;
end;
registration
let A be natural-membered set;
let a be Nat;
cluster a**A -> natural-membered;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify a**A with f**F when a = f, A = F;
end;
theorem :: MEMBER_1:196
a <> 0 & a**A c= a**B implies A c= B;
theorem :: MEMBER_1:197
a <> 0 & a**A = a**B implies A = B;
theorem :: MEMBER_1:198
a <> 0 implies a ** (A/\B) = (a**A) /\ (a**B);
theorem :: MEMBER_1:199
a <> 0 implies a ** (A\B) = (a**A) \ (a**B);
theorem :: MEMBER_1:200
a <> 0 implies a ** (A\+\B) = (a**A) \+\ (a**B);
theorem :: MEMBER_1:201
0**A c= {0};
theorem :: MEMBER_1:202
A <> {} implies 0**A = {0};
theorem :: MEMBER_1:203
1**A = A;
theorem :: MEMBER_1:204
(a*b)**A = a**(b**A);
theorem :: MEMBER_1:205
a**(A**B) = (a**A)**B;
theorem :: MEMBER_1:206
(a+b)**A c= a**A ++ b**A;
theorem :: MEMBER_1:207
(a-b)**A c= a**A -- b**A;
theorem :: MEMBER_1:208
a**(B++C) = a**B++a**C;
theorem :: MEMBER_1:209
a**(B--C) = a**B--a**C;
definition
let F be ext-real-membered set;
let f be ExtReal;
func f///F -> set equals
:: MEMBER_1:def 21
{f}///F;
end;
theorem :: MEMBER_1:210
g in G implies f/g in f///G;
theorem :: MEMBER_1:211
f///F = {f/w: w in F};
theorem :: MEMBER_1:212
e in f///F implies ex w st e = f/w & w in F;
registration
let F be empty set;
let f be ExtReal;
cluster f///F -> empty;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster f///F -> non empty;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster f///F -> ext-real-membered;
end;
definition
let A be complex-membered set;
let a be Complex;
func a///A -> set equals
:: MEMBER_1:def 22
{a}///A;
end;
theorem :: MEMBER_1:213
b in A implies a/b in a///A;
theorem :: MEMBER_1:214
a///A = {a/c: c in A};
theorem :: MEMBER_1:215
e in a///A implies ex c st e = a/c & c in A;
registration
let A be empty set;
let a be Complex;
cluster a///A -> empty;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster a///A -> non empty;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster a///A -> complex-membered;
end;
registration
let A be real-membered set;
let a be Real;
cluster a///A -> real-membered;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster a///A -> rational-membered;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify a///A with f///F when a = f, A = F;
end;
theorem :: MEMBER_1:216
a <> 0 & a///A c= a///B implies A c= B;
theorem :: MEMBER_1:217
a <> 0 & a///A = a///B implies A = B;
theorem :: MEMBER_1:218
a <> 0 implies a /// (A/\B) = (a///A) /\ (a///B);
theorem :: MEMBER_1:219
a <> 0 implies a /// (A\B) = (a///A) \ (a///B);
theorem :: MEMBER_1:220
a <> 0 implies a /// (A\+\B) = (a///A) \+\ (a///B);
theorem :: MEMBER_1:221
(a+b)///A c= a///A ++ b///A;
theorem :: MEMBER_1:222
(a-b)///A c= a///A -- b///A;
definition
let F be ext-real-membered set;
let f be ExtReal;
func F///f -> set equals
:: MEMBER_1:def 23
F///{f};
end;
theorem :: MEMBER_1:223
g in G implies g/f in G///f;
theorem :: MEMBER_1:224
F///f = {w/f: w in F};
theorem :: MEMBER_1:225
e in F///f implies ex w st e = w/f & w in F;
registration
let F be empty set;
let f be ExtReal;
cluster F///f -> empty;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster F///f -> non empty;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster F///f -> ext-real-membered;
end;
definition
let A be complex-membered set;
let a be Complex;
func A///a -> set equals
:: MEMBER_1:def 24
A///{a};
end;
theorem :: MEMBER_1:226
b in A implies b/a in A///a;
theorem :: MEMBER_1:227
A///a = {c/a: c in A};
theorem :: MEMBER_1:228
e in A///a implies ex c st e = c/a & c in A;
registration
let A be empty set;
let a be Complex;
cluster A///a -> empty;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster A///a -> non empty;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster A///a -> complex-membered;
end;
registration
let A be real-membered set;
let a be Real;
cluster A///a -> real-membered;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster A///a -> rational-membered;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify A///a with F///f when a = f, A = F;
end;
theorem :: MEMBER_1:229
a <> 0 & A///a c= B///a implies A c= B;
theorem :: MEMBER_1:230
a <> 0 & A///a = B///a implies A = B;
theorem :: MEMBER_1:231
a <> 0 implies (A/\B) /// a = (A///a) /\ (B///a);
theorem :: MEMBER_1:232
a <> 0 implies (A\B) /// a = (A///a) \ (B///a);
theorem :: MEMBER_1:233
a <> 0 implies (A\+\B) /// a = (A///a) \+\ (B///a);
theorem :: MEMBER_1:234
(A++B)///a = A///a ++ B///a;
theorem :: MEMBER_1:235
(A--B)///a = A///a -- B///a;