begin
:: deftheorem defines + MATHMORP:def 1 :
for T being non empty addMagma
for p being Element of T
for X being Subset of T holds X + p = { (q + p) where q is Element of T : q in X } ;
:: deftheorem defines ! MATHMORP:def 2 :
for T being non empty addLoopStr
for X being Subset of T holds X ! = { (- q) where q is Point of T : q in X } ;
:: deftheorem defines (-) MATHMORP:def 3 :
for T being non empty addMagma
for X, B being Subset of T holds X (-) B = { y where y is Point of T : B + y c= X } ;
:: deftheorem MATHMORP:def 4 :
canceled;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
Lm1:
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x, y being Point of T holds {x} + y = {y} + x
theorem
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
E52:
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for p, x being Point of T holds
( (p - x) + x = p & (p + x) - x = p )
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem
Lm2:
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T 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 T being non empty addLoopStr
for X, B being Subset of T holds X (O) B = (X (-) B) (+) B;
:: deftheorem defines (o) MATHMORP:def 6 :
for T being non empty addLoopStr
for X, B being Subset of T 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 T being non empty RLSStruct
for A being Subset of T holds t (.) A = { (t * a) where a is Point of T : 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 T being non empty RLSStruct
for X, B1, B2 being Subset of T holds X (*) (B1,B2) = (X (-) B1) /\ ((X `) (-) B2);
:: deftheorem defines (&) MATHMORP:def 9 :
for T being non empty RLSStruct
for X, B1, B2 being Subset of T holds X (&) (B1,B2) = X \/ (X (*) (B1,B2));
:: deftheorem defines (@) MATHMORP:def 10 :
for T being non empty RLSStruct
for X, B1, B2 being Subset of T 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