:: by Yuzhong Ding and Xiquan Liang

::

:: Received January 7, 2005

:: Copyright (c) 2005-2012 Association of Mizar Users

begin

definition

let T be non empty addMagma ;

let p be Element of T;

let X be Subset of T;

coherence

{ (q + p) where q is Element of T : q in X } is Subset of T

end;
let p be Element of T;

let X be Subset of T;

coherence

{ (q + p) where q is Element of T : q in X } is Subset of T

proof end;

:: 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 } ;

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 } ;

:: Reflected of X

definition

let T be non empty addLoopStr ;

let X be Subset of T;

coherence

{ (- q) where q is Point of T : q in X } is Subset of T

end;
let X be Subset of T;

coherence

{ (- q) where q is Point of T : q in X } is Subset of T

proof end;

:: 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 } ;

for T being non empty addLoopStr

for X being Subset of T holds X ! = { (- q) where q is Point of T : q in X } ;

:: Set Erosion

definition

let T be non empty addMagma ;

let X, B be Subset of T;

coherence

{ y where y is Point of T : B + y c= X } is Subset of T

end;
let X, B be Subset of T;

coherence

{ y where y is Point of T : B + y c= X } is Subset of T

proof end;

:: 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 } ;

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 } ;

theorem Th1: :: MATHMORP:1

for T being non empty right_complementable add-associative right_zeroed RLSStruct

for B being Subset of T holds (B !) ! = B

for B being Subset of T holds (B !) ! = B

proof end;

theorem Th2: :: MATHMORP:2

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for x being Point of T holds {(0. T)} + x = {x}

for x being Point of T holds {(0. T)} + x = {x}

proof end;

theorem Th3: :: MATHMORP:3

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for B1, B2 being Subset of T

for p being Point of T st B1 c= B2 holds

B1 + p c= B2 + p

for B1, B2 being Subset of T

for p being Point of T st B1 c= B2 holds

B1 + p c= B2 + p

proof end;

theorem Th4: :: MATHMORP:4

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for x being Point of T

for X being Subset of T st X = {} holds

X + x = {}

for x being Point of T

for X being Subset of T st X = {} holds

X + x = {}

proof end;

theorem :: MATHMORP:5

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X being Subset of T holds X (-) {(0. T)} = X

for X being Subset of T holds X (-) {(0. T)} = X

proof end;

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

proof end;

theorem :: MATHMORP:6

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X being Subset of T holds X (+) {(0. T)} = X

for X being Subset of T holds X (+) {(0. T)} = X

proof end;

theorem :: MATHMORP:7

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X being Subset of T

for x being Point of T holds X (+) {x} = X + x

for X being Subset of T

for x being Point of T holds X (+) {x} = X + x

proof end;

theorem Th8: :: MATHMORP:8

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y being Subset of T st Y = {} holds

X (-) Y = the carrier of T

for X, Y being Subset of T st Y = {} holds

X (-) Y = the carrier of T

proof end;

theorem Th9: :: MATHMORP:9

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y, B being Subset of T st X c= Y holds

( X (-) B c= Y (-) B & X (+) B c= Y (+) B )

for X, Y, B being Subset of T st X c= Y holds

( X (-) B c= Y (-) B & X (+) B c= Y (+) B )

proof end;

theorem Th10: :: MATHMORP:10

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for B1, B2, X being Subset of T st B1 c= B2 holds

( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 )

for B1, B2, X being Subset of T st B1 c= B2 holds

( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 )

proof end;

theorem :: MATHMORP:11

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for B, X being Subset of T st 0. T in B holds

( X (-) B c= X & X c= X (+) B )

for B, X being Subset of T st 0. T in B holds

( X (-) B c= X & X c= X (+) B )

proof end;

theorem Th12: :: MATHMORP:12

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y being Subset of T holds X (+) Y = Y (+) X

for X, Y being Subset of T holds X (+) Y = Y (+) X

proof end;

Lm2: 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 )

proof end;

theorem Th13: :: MATHMORP:13

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for Y, X being Subset of T

for y, x being Point of T holds

( Y + y c= X + x iff Y + (y - x) c= X )

for Y, X being Subset of T

for y, x being Point of T holds

( Y + y c= X + x iff Y + (y - x) c= X )

proof end;

theorem Th14: :: MATHMORP:14

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y being Subset of T

for p being Point of T holds (X + p) (-) Y = (X (-) Y) + p

for X, Y being Subset of T

for p being Point of T holds (X + p) (-) Y = (X (-) Y) + p

proof end;

theorem Th15: :: MATHMORP:15

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y being Subset of T

for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p

for X, Y being Subset of T

for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p

proof end;

theorem Th16: :: MATHMORP:16

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X being Subset of T

for x, y being Point of T holds (X + x) + y = X + (x + y)

for X being Subset of T

for x, y being Point of T holds (X + x) + y = X + (x + y)

proof end;

theorem Th17: :: MATHMORP:17

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y being Subset of T

for p being Point of T holds X (-) (Y + p) = (X (-) Y) + (- p)

for X, Y being Subset of T

for p being Point of T holds X (-) (Y + p) = (X (-) Y) + (- p)

proof end;

theorem :: MATHMORP:18

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y being Subset of T

for p being Point of T holds X (+) (Y + p) = (X (+) Y) + p

for X, Y being Subset of T

for p being Point of T holds X (+) (Y + p) = (X (+) Y) + p

proof end;

theorem Th19: :: MATHMORP:19

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T

for x being Point of T st x in X holds

B + x c= B (+) X

for X, B being Subset of T

for x being Point of T st x in X holds

B + x c= B (+) X

proof end;

theorem Th20: :: MATHMORP:20

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T holds X c= (X (+) B) (-) B

for X, B being Subset of T holds X c= (X (+) B) (-) B

proof end;

theorem Th21: :: MATHMORP:21

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X being Subset of T holds X + (0. T) = X

for X being Subset of T holds X + (0. T) = X

proof end;

theorem :: MATHMORP:22

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X being Subset of T

for x being Point of T holds X (-) {x} = X + (- x)

for X being Subset of T

for x being Point of T holds X (-) {x} = X + (- x)

proof end;

Lm3: 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

proof end;

theorem Th23: :: MATHMORP:23

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Y) (-) Z

for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Y) (-) Z

proof end;

theorem :: MATHMORP:24

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Z) (-) Y

for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Z) (-) Y

proof end;

theorem :: MATHMORP:25

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y, Z being Subset of T holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z

for X, Y, Z being Subset of T holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z

proof end;

theorem :: MATHMORP:26

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y, Z being Subset of T holds X (+) (Y (+) Z) = (X (+) Y) (+) Z

for X, Y, Z being Subset of T holds X (+) (Y (+) Z) = (X (+) Y) (+) Z

proof end;

theorem Th27: :: MATHMORP:27

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for B, C being Subset of T

for y being Point of T holds (B \/ C) + y = (B + y) \/ (C + y)

for B, C being Subset of T

for y being Point of T holds (B \/ C) + y = (B + y) \/ (C + y)

proof end;

theorem Th28: :: MATHMORP:28

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for B, C being Subset of T

for y being Point of T holds (B /\ C) + y = (B + y) /\ (C + y)

for B, C being Subset of T

for y being Point of T holds (B /\ C) + y = (B + y) /\ (C + y)

proof end;

theorem :: MATHMORP:29

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B, C being Subset of T holds X (-) (B \/ C) = (X (-) B) /\ (X (-) C)

for X, B, C being Subset of T holds X (-) (B \/ C) = (X (-) B) /\ (X (-) C)

proof end;

theorem :: MATHMORP:30

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B, C being Subset of T holds X (+) (B \/ C) = (X (+) B) \/ (X (+) C)

for X, B, C being Subset of T holds X (+) (B \/ C) = (X (+) B) \/ (X (+) C)

proof end;

theorem :: MATHMORP:31

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B, Y being Subset of T holds (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B

for X, B, Y being Subset of T holds (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B

proof end;

theorem :: MATHMORP:32

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y, B being Subset of T holds (X \/ Y) (+) B = (X (+) B) \/ (Y (+) B)

for X, Y, B being Subset of T holds (X \/ Y) (+) B = (X (+) B) \/ (Y (+) B)

proof end;

theorem :: MATHMORP:33

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y, B being Subset of T holds (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B)

for X, Y, B being Subset of T holds (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B)

proof end;

theorem Th34: :: MATHMORP:34

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y, B being Subset of T holds (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B)

for X, Y, B being Subset of T holds (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B)

proof end;

theorem :: MATHMORP:35

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for B, X, Y being Subset of T holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)

for B, X, Y being Subset of T holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)

proof end;

theorem :: MATHMORP:36

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for B, X, Y being Subset of T holds (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y)

for B, X, Y being Subset of T holds (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y)

proof end;

theorem Th37: :: MATHMORP:37

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T holds ((X `) (-) B) ` = X (+) (B !)

for X, B being Subset of T holds ((X `) (-) B) ` = X (+) (B !)

proof end;

theorem Th38: :: MATHMORP:38

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T holds (X (-) B) ` = (X `) (+) (B !)

for X, B being Subset of T holds (X (-) B) ` = (X `) (+) (B !)

proof end;

begin

:: 2. The definition of Adjunction Opening and Closing and

:: their Algebraic Properties

:: Adjunction Opening

:: their Algebraic Properties

:: Adjunction Opening

definition
end;

:: deftheorem defines (O) MATHMORP:def 4 :

for T being non empty addLoopStr

for X, B being Subset of T holds X (O) B = (X (-) B) (+) B;

for T being non empty addLoopStr

for X, B being Subset of T holds X (O) B = (X (-) B) (+) B;

:: Adjunction Closing

definition
end;

:: 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;

for T being non empty addLoopStr

for X, B being Subset of T holds X (o) B = (X (+) B) (-) B;

theorem :: MATHMORP:39

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T holds ((X `) (O) (B !)) ` = X (o) B

for X, B being Subset of T holds ((X `) (O) (B !)) ` = X (o) B

proof end;

theorem :: MATHMORP:40

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T holds ((X `) (o) (B !)) ` = X (O) B

for X, B being Subset of T holds ((X `) (o) (B !)) ` = X (O) B

proof end;

theorem Th41: :: MATHMORP:41

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T holds

( X (O) B c= X & X c= X (o) B )

for X, B being Subset of T holds

( X (O) B c= X & X c= X (o) B )

proof end;

theorem Th42: :: MATHMORP:42

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X being Subset of T holds X (O) X = X

for X being Subset of T holds X (O) X = X

proof end;

theorem :: MATHMORP:43

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T holds

( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B )

for X, B being Subset of T holds

( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B )

proof end;

theorem :: MATHMORP:44

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T holds

( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B )

for X, B being Subset of T holds

( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B )

proof end;

theorem Th45: :: MATHMORP:45

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y, B being Subset of T st X c= Y holds

( X (O) B c= Y (O) B & X (o) B c= Y (o) B )

for X, Y, B being Subset of T st X c= Y holds

( X (O) B c= Y (O) B & X (o) B c= Y (o) B )

proof end;

theorem Th46: :: MATHMORP:46

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y being Subset of T

for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p

for X, Y being Subset of T

for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p

proof end;

theorem :: MATHMORP:47

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y being Subset of T

for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p

for X, Y being Subset of T

for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p

proof end;

theorem :: MATHMORP:48

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for C, B, X being Subset of T st C c= B holds

X (O) B c= (X (-) C) (+) B

for C, B, X being Subset of T st C c= B holds

X (O) B c= (X (-) C) (+) B

proof end;

theorem :: MATHMORP:49

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for B, C, X being Subset of T st B c= C holds

X (o) B c= (X (+) C) (-) B

for B, C, X being Subset of T st B c= C holds

X (o) B c= (X (+) C) (-) B

proof end;

theorem Th50: :: MATHMORP:50

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y being Subset of T holds

( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y )

for X, Y being Subset of T holds

( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y )

proof end;

theorem :: MATHMORP:51

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, Y being Subset of T holds

( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )

for X, Y being Subset of T holds

( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )

proof end;

theorem :: MATHMORP:52

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T holds (X (O) B) (O) B = X (O) B

for X, B being Subset of T holds (X (O) B) (O) B = X (O) B

proof end;

theorem :: MATHMORP:53

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B being Subset of T holds (X (o) B) (o) B = X (o) B by Th50;

for X, B being Subset of T holds (X (o) B) (o) B = X (o) B by Th50;

theorem :: MATHMORP:54

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X, B, Y being Subset of T holds X (O) B c= (X \/ Y) (O) B

for X, B, Y being Subset of T holds X (O) B c= (X \/ Y) (O) B

proof end;

theorem :: MATHMORP:55

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for B, B1, X being Subset of T st B = B (O) B1 holds

X (O) B c= X (O) B1

for B, B1, X being Subset of T st B = B (O) B1 holds

X (O) B c= X (O) B1

proof end;

begin

:: 3.The definition of Scaling transformation and its Algebraic Properties

:: Scaling transformation

:: Scaling transformation

definition

let t be real number ;

let T be non empty RLSStruct ;

let A be Subset of T;

coherence

{ (t * a) where a is Point of T : a in A } is Subset of T

end;
let T be non empty RLSStruct ;

let A be Subset of T;

coherence

{ (t * a) where a is Point of T : a in A } is Subset of T

proof end;

:: deftheorem defines (.) MATHMORP:def 6 :

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 } ;

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 :: MATHMORP:56

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct

for X being Subset of T st X = {} holds

0 (.) X = {}

for X being Subset of T st X = {} holds

0 (.) X = {}

proof end;

theorem :: MATHMORP:57

for n being Element of NAT

for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0. (TOP-REAL n))}

for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0. (TOP-REAL n))}

proof end;

theorem Th60: :: MATHMORP:60

for t, s being real number

for n being Element of NAT

for X being Subset of (TOP-REAL n) holds (t * s) (.) X = t (.) (s (.) X)

for n being Element of NAT

for X being Subset of (TOP-REAL n) holds (t * s) (.) X = t (.) (s (.) X)

proof end;

theorem Th61: :: MATHMORP:61

for t being real number

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) st X c= Y holds

t (.) X c= t (.) Y

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) st X c= Y holds

t (.) X c= t (.) Y

proof end;

theorem Th62: :: MATHMORP:62

for t being real number

for n being Element of NAT

for X being Subset of (TOP-REAL n)

for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x)

for n being Element of NAT

for X being Subset of (TOP-REAL n)

for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x)

proof end;

theorem Th63: :: MATHMORP:63

for t being real number

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) holds t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y)

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) holds t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y)

proof end;

theorem Th64: :: MATHMORP:64

for t being real number

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) st t <> 0 holds

t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y)

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) st t <> 0 holds

t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y)

proof end;

theorem :: MATHMORP:65

for t being real number

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) st t <> 0 holds

t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y)

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) st t <> 0 holds

t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y)

proof end;

theorem :: MATHMORP:66

for t being real number

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) st t <> 0 holds

t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) st t <> 0 holds

t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)

proof end;

begin

:: Algebraic Properties.

:: "Hit or Miss" Transformation

:: "Hit or Miss" Transformation

definition

let T be non empty RLSStruct ;

let X, B1, B2 be Subset of T;

coherence

(X (-) B1) /\ ((X `) (-) B2) is Subset of T ;

end;
let X, B1, B2 be Subset of T;

coherence

(X (-) B1) /\ ((X `) (-) B2) is Subset of T ;

:: deftheorem defines (*) MATHMORP:def 7 :

for T being non empty RLSStruct

for X, B1, B2 being Subset of T holds X (*) (B1,B2) = (X (-) B1) /\ ((X `) (-) B2);

for T being non empty RLSStruct

for X, B1, B2 being Subset of T holds X (*) (B1,B2) = (X (-) B1) /\ ((X `) (-) B2);

:: Thickening

definition

let T be non empty RLSStruct ;

let X, B1, B2 be Subset of T;

coherence

X \/ (X (*) (B1,B2)) is Subset of T ;

end;
let X, B1, B2 be Subset of T;

coherence

X \/ (X (*) (B1,B2)) is Subset of T ;

:: deftheorem defines (&) MATHMORP:def 8 :

for T being non empty RLSStruct

for X, B1, B2 being Subset of T holds X (&) (B1,B2) = X \/ (X (*) (B1,B2));

for T being non empty RLSStruct

for X, B1, B2 being Subset of T holds X (&) (B1,B2) = X \/ (X (*) (B1,B2));

:: Thinning

definition

let T be non empty RLSStruct ;

let X, B1, B2 be Subset of T;

coherence

X \ (X (*) (B1,B2)) is Subset of T ;

end;
let X, B1, B2 be Subset of T;

coherence

X \ (X (*) (B1,B2)) is Subset of T ;

:: 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));

for T being non empty RLSStruct

for X, B1, B2 being Subset of T holds X (@) (B1,B2) = X \ (X (*) (B1,B2));

theorem :: MATHMORP:67

for n being Element of NAT

for B1, X, B2 being Subset of (TOP-REAL n) st B1 = {} holds

X (*) (B1,B2) = (X `) (-) B2

for B1, X, B2 being Subset of (TOP-REAL n) st B1 = {} holds

X (*) (B1,B2) = (X `) (-) B2

proof end;

theorem :: MATHMORP:68

for n being Element of NAT

for B2, X, B1 being Subset of (TOP-REAL n) st B2 = {} holds

X (*) (B1,B2) = X (-) B1

for B2, X, B1 being Subset of (TOP-REAL n) st B2 = {} holds

X (*) (B1,B2) = X (-) B1

proof end;

theorem :: MATHMORP:69

for n being Element of NAT

for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds

X (*) (B1,B2) c= X

for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds

X (*) (B1,B2) c= X

proof end;

theorem :: MATHMORP:70

for n being Element of NAT

for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds

(X (*) (B1,B2)) /\ X = {}

for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds

(X (*) (B1,B2)) /\ X = {}

proof end;

theorem :: MATHMORP:71

for n being Element of NAT

for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds

X (&) (B1,B2) = X

for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds

X (&) (B1,B2) = X

proof end;

theorem :: MATHMORP:72

for n being Element of NAT

for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds

X (@) (B1,B2) = X

for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds

X (@) (B1,B2) = X

proof end;

theorem :: MATHMORP:73

for n being Element of NAT

for X, B2, B1 being Subset of (TOP-REAL n) holds X (@) (B2,B1) = ((X `) (&) (B1,B2)) `

for X, B2, B1 being Subset of (TOP-REAL n) holds X (@) (B2,B1) = ((X `) (&) (B1,B2)) `

proof end;

begin

:: Adjunction Closing on Convex sets

theorem Th74: :: MATHMORP:74

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 )

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 )

proof end;

definition

let V be RealLinearSpace;

let B be Subset of V;

( 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 ) by Th74;

end;
let B be Subset of V;

redefine attr B is convex means :Def10: :: MATHMORP:def 10

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;

compatibility 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;

( 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 ) by Th74;

:: deftheorem Def10 defines convex MATHMORP:def 10 :

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 );

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 Th76: :: MATHMORP:76

for n being Element of NAT

for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds

( X (+) B is convex & X (-) B is convex )

for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds

( X (+) B is convex & X (-) B is convex )

proof end;

theorem :: MATHMORP:77

for n being Element of NAT

for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds

( X (O) B is convex & X (o) B is convex )

for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds

( X (O) B is convex & X (o) B is convex )

proof end;

theorem :: MATHMORP:78

for t, s being real number

for n being Element of NAT

for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds

(s + t) (.) B = (s (.) B) (+) (t (.) B)

for n being Element of NAT

for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds

(s + t) (.) B = (s (.) B) (+) (t (.) B)

proof end;

:: Translation of X according to p