begin
:: deftheorem defines + MATHMORP:def 1 :
for n being Element of NAT
for p being Point of (TOP-REAL n)
for X being Subset of (TOP-REAL n) holds X + p = { (q + p) where q is Point of (TOP-REAL n) : q in X } ;
:: deftheorem defines ! MATHMORP:def 2 :
for n being Element of NAT
for X being Subset of (TOP-REAL n) holds X ! = { (- q) where q is Point of (TOP-REAL n) : q in X } ;
:: deftheorem defines (-) MATHMORP:def 3 :
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds X (-) B = { y where y is Point of (TOP-REAL n) : B + y c= X } ;
:: deftheorem defines (+) MATHMORP:def 4 :
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds X (+) B = { (y + b) where y, b is Point of (TOP-REAL n) : ( y in X & b in B ) } ;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
Lm1:
for n being Element of NAT
for x, y being Point of (TOP-REAL n) holds {x} + y = {y} + x
theorem
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem
Lm2:
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds (X (-) B) (+) B c= X
theorem Th23:
theorem
theorem
theorem
theorem Th27:
theorem Th28:
theorem
theorem
theorem
theorem
theorem
theorem Th34:
theorem
theorem
theorem Th37:
theorem Th38:
begin
:: deftheorem defines (O) MATHMORP:def 5 :
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds X (O) B = (X (-) B) (+) B;
:: deftheorem defines (o) MATHMORP:def 6 :
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds X (o) B = (X (+) B) (-) B;
theorem
theorem
theorem Th41:
theorem Th42:
theorem
theorem
theorem Th45:
theorem Th46:
theorem
theorem
theorem
theorem Th50:
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem defines (.) MATHMORP:def 7 :
for t being real number
for n being Element of NAT
for A being Subset of (TOP-REAL n) holds t (.) A = { (t * a) where a is Point of (TOP-REAL n) : a in A } ;
theorem
theorem
theorem Th58:
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem
begin
:: deftheorem defines (*) MATHMORP:def 8 :
for n being Element of NAT
for X, B1, B2 being Subset of (TOP-REAL n) holds X (*) B1,B2 = (X (-) B1) /\ ((X ` ) (-) B2);
:: deftheorem defines (&) MATHMORP:def 9 :
for n being Element of NAT
for X, B1, B2 being Subset of (TOP-REAL n) holds X (&) B1,B2 = X \/ (X (*) B1,B2);
:: deftheorem defines (@) MATHMORP:def 10 :
for n being Element of NAT
for X, B1, B2 being Subset of (TOP-REAL n) holds X (@) B1,B2 = X \ (X (*) B1,B2);
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
begin
theorem Th75:
:: deftheorem Def11 defines convex MATHMORP:def 11 :
for V being RealLinearSpace
for B being Subset of V holds
( B is convex iff for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B );
theorem
theorem Th77:
theorem
theorem