:: by Hiroshi Yamazaki , Czes\l aw Byli\'nski and Katsumi Wasaki

::

:: Received September 21, 2011

:: Copyright (c) 2011-2021 Association of Mizar Users

definition

let E be RealLinearSpace;

let A, B be binary-image of E;

coherence

{ z where z is Element of E : for b being Element of E st b in B holds

z - b in A } is binary-image of E;

end;
let A, B be binary-image of E;

func A (-) B -> binary-image of E equals :: MORPH_01:def 1

{ z where z is Element of E : for b being Element of E st b in B holds

z - b in A } ;

correctness { z where z is Element of E : for b being Element of E st b in B holds

z - b in A } ;

coherence

{ z where z is Element of E : for b being Element of E st b in B holds

z - b in A } is binary-image of E;

proof end;

:: deftheorem defines (-) MORPH_01:def 1 :

for E being RealLinearSpace

for A, B being binary-image of E holds A (-) B = { z where z is Element of E : for b being Element of E st b in B holds

z - b in A } ;

for E being RealLinearSpace

for A, B being binary-image of E holds A (-) B = { z where z is Element of E : for b being Element of E st b in B holds

z - b in A } ;

notation
end;

theorem Th1: :: MORPH_01:1

for E being RealLinearSpace

for A, B being Subset of E st B = {} holds

( A (+) B = B & B (+) A = B & A (-) B = the carrier of E )

for A, B being Subset of E st B = {} holds

( A (+) B = B & B (+) A = B & A (-) B = the carrier of E )

proof end;

theorem Th3: :: MORPH_01:3

for E being RealLinearSpace

for A, B being Subset of E st B = the carrier of E & A <> {} holds

( A (+) B = B & B (+) A = B )

for A, B being Subset of E st B = the carrier of E & A <> {} holds

( A (+) B = B & B (+) A = B )

proof end;

theorem :: MORPH_01:5

for E being RealLinearSpace

for A, B being binary-image of E holds A (+) B = union { (b + A) where b is Element of E : b in B }

for A, B being binary-image of E holds A (+) B = union { (b + A) where b is Element of E : b in B }

proof end;

definition
end;

theorem :: MORPH_01:6

for E being RealLinearSpace

for A, B being non empty binary-image of E holds A (-) B = meet { (b + A) where b is Element of E : b in B }

for A, B being non empty binary-image of E holds A (-) B = meet { (b + A) where b is Element of E : b in B }

proof end;

theorem Th7: :: MORPH_01:7

for E being RealLinearSpace

for A, B being non empty binary-image of E holds A (+) B = { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} }

for A, B being non empty binary-image of E holds A (+) B = { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} }

proof end;

theorem Th8: :: MORPH_01:8

for E being RealLinearSpace

for A, B being non empty binary-image of E holds A (-) B = { v where v is Element of E : v + ((- 1) * B) c= A }

for A, B being non empty binary-image of E holds A (-) B = { v where v is Element of E : v + ((- 1) * B) c= A }

proof end;

theorem Th9: :: MORPH_01:9

for E being RealLinearSpace

for A, B being non empty binary-image of E holds

( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )

for A, B being non empty binary-image of E holds

( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )

proof end;

Lm1: for E being non empty Abelian addLoopStr

for A, B being Subset of E holds A (+) B = B (+) A

proof end;

definition

let E be non empty Abelian addLoopStr ;

let A, B be Subset of E;

:: original: +

redefine func A (+) B -> Element of K10( the carrier of E);

commutativity

for A, B being Subset of E holds A + B = B + A by Lm1;

end;
let A, B be Subset of E;

:: original: +

redefine func A (+) B -> Element of K10( the carrier of E);

commutativity

for A, B being Subset of E holds A + B = B + A by Lm1;

theorem Th10: :: MORPH_01:10

for E being non empty add-associative addLoopStr

for A, B, C being Subset of E holds (A + B) + C = A + (B + C)

for A, B, C being Subset of E holds (A + B) + C = A + (B + C)

proof end;

theorem :: MORPH_01:11

for E being RealLinearSpace

for A, B, C being non empty binary-image of E holds (A (+) B) (+) C = A (+) (B (+) C) by Th10;

for A, B, C being non empty binary-image of E holds (A (+) B) (+) C = A (+) (B (+) C) by Th10;

theorem Th12: :: MORPH_01:12

for E being RealLinearSpace

for F being binary-image-family of E

for B being non empty binary-image of E holds (union F) (+) B = union { (X (+) B) where X is binary-image of E : X in F }

for F being binary-image-family of E

for B being non empty binary-image of E holds (union F) (+) B = union { (X (+) B) where X is binary-image of E : X in F }

proof end;

theorem :: MORPH_01:13

for E being RealLinearSpace

for F being binary-image-family of E

for A being non empty binary-image of E holds A (+) (union F) = union { (A (+) X) where X is binary-image of E : X in F }

for F being binary-image-family of E

for A being non empty binary-image of E holds A (+) (union F) = union { (A (+) X) where X is binary-image of E : X in F }

proof end;

theorem Th14: :: MORPH_01:14

for E being RealLinearSpace

for F being binary-image-family of E

for B being non empty binary-image of E holds (meet F) (+) B c= meet { (X (+) B) where X is binary-image of E : X in F }

for F being binary-image-family of E

for B being non empty binary-image of E holds (meet F) (+) B c= meet { (X (+) B) where X is binary-image of E : X in F }

proof end;

theorem :: MORPH_01:15

for E being RealLinearSpace

for F being binary-image-family of E

for A being non empty binary-image of E holds A (+) (meet F) c= meet { (A (+) X) where X is binary-image of E : X in F }

for F being binary-image-family of E

for A being non empty binary-image of E holds A (+) (meet F) c= meet { (A (+) X) where X is binary-image of E : X in F }

proof end;

theorem Th17: :: MORPH_01:17

for E being RealLinearSpace

for v being Element of E

for A, B being non empty binary-image of E holds

( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )

for v being Element of E

for A, B being non empty binary-image of E holds

( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )

proof end;

theorem Th18: :: MORPH_01:18

for E being RealLinearSpace

for F being binary-image-family of E

for B being non empty binary-image of E holds (meet F) (-) B = meet { (X (-) B) where X is binary-image of E : X in F }

for F being binary-image-family of E

for B being non empty binary-image of E holds (meet F) (-) B = meet { (X (-) B) where X is binary-image of E : X in F }

proof end;

theorem :: MORPH_01:19

for E being RealLinearSpace

for F being binary-image-family of E

for B being non empty binary-image of E holds meet { (B (-) X) where X is binary-image of E : X in F } c= B (-) (meet F)

for F being binary-image-family of E

for B being non empty binary-image of E holds meet { (B (-) X) where X is binary-image of E : X in F } c= B (-) (meet F)

proof end;

theorem :: MORPH_01:20

for E being RealLinearSpace

for F being binary-image-family of E

for B being non empty binary-image of E holds union { (X (-) B) where X is binary-image of E : X in F } c= (union F) (-) B

for F being binary-image-family of E

for B being non empty binary-image of E holds union { (X (-) B) where X is binary-image of E : X in F } c= (union F) (-) B

proof end;

theorem :: MORPH_01:21

for E being RealLinearSpace

for F being binary-image-family of E

for B being non empty binary-image of E st F <> {} holds

B (-) (union F) = meet { (B (-) X) where X is binary-image of E : X in F }

for F being binary-image-family of E

for B being non empty binary-image of E st F <> {} holds

B (-) (union F) = meet { (B (-) X) where X is binary-image of E : X in F }

proof end;

theorem Th22: :: MORPH_01:22

for E being RealLinearSpace

for A, B, C being non empty binary-image of E st A c= B holds

A (-) C c= B (-) C

for A, B, C being non empty binary-image of E st A c= B holds

A (-) C c= B (-) C

proof end;

theorem :: MORPH_01:23

for E being RealLinearSpace

for A, B, C being non empty binary-image of E st A c= B holds

C (-) B c= C (-) A

for A, B, C being non empty binary-image of E st A c= B holds

C (-) B c= C (-) A

proof end;

theorem Th24: :: MORPH_01:24

for E being RealLinearSpace

for v being Element of E

for A, B being non empty binary-image of E holds

( (v + A) (-) B = A (-) (v + B) & (v + A) (-) B = v + (A (-) B) )

for v being Element of E

for A, B being non empty binary-image of E holds

( (v + A) (-) B = A (-) (v + B) & (v + A) (-) B = v + (A (-) B) )

proof end;

theorem Th25: :: MORPH_01:25

for E being RealLinearSpace

for A, B, C being non empty binary-image of E holds (A (-) B) (-) C = A (-) (B (+) C)

for A, B, C being non empty binary-image of E holds (A (-) B) (-) C = A (-) (B (+) C)

proof end;

definition

let E be RealLinearSpace;

let B be binary-image of E;

ex b_{1} being Function of (bool the carrier of E),(bool the carrier of E) st

for A being binary-image of E holds b_{1} . A = A (+) B

for b_{1}, b_{2} being Function of (bool the carrier of E),(bool the carrier of E) st ( for A being binary-image of E holds b_{1} . A = A (+) B ) & ( for A being binary-image of E holds b_{2} . A = A (+) B ) holds

b_{1} = b_{2}

end;
let B be binary-image of E;

func dilation B -> Function of (bool the carrier of E),(bool the carrier of E) means :Def2: :: MORPH_01:def 2

for A being binary-image of E holds it . A = A (+) B;

existence for A being binary-image of E holds it . A = A (+) B;

ex b

for A being binary-image of E holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines dilation MORPH_01:def 2 :

for E being RealLinearSpace

for B being binary-image of E

for b_{3} being Function of (bool the carrier of E),(bool the carrier of E) holds

( b_{3} = dilation B iff for A being binary-image of E holds b_{3} . A = A (+) B );

for E being RealLinearSpace

for B being binary-image of E

for b

( b

definition

let E be RealLinearSpace;

let B be binary-image of E;

ex b_{1} being Function of (bool the carrier of E),(bool the carrier of E) st

for A being binary-image of E holds b_{1} . A = A (-) B

for b_{1}, b_{2} being Function of (bool the carrier of E),(bool the carrier of E) st ( for A being binary-image of E holds b_{1} . A = A (-) B ) & ( for A being binary-image of E holds b_{2} . A = A (-) B ) holds

b_{1} = b_{2}

end;
let B be binary-image of E;

func erosion B -> Function of (bool the carrier of E),(bool the carrier of E) means :Def3: :: MORPH_01:def 3

for A being binary-image of E holds it . A = A (-) B;

existence for A being binary-image of E holds it . A = A (-) B;

ex b

for A being binary-image of E holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines erosion MORPH_01:def 3 :

for E being RealLinearSpace

for B being binary-image of E

for b_{3} being Function of (bool the carrier of E),(bool the carrier of E) holds

( b_{3} = erosion B iff for A being binary-image of E holds b_{3} . A = A (-) B );

for E being RealLinearSpace

for B being binary-image of E

for b

( b

theorem :: MORPH_01:26

for E being RealLinearSpace

for F being binary-image-family of E

for B being non empty binary-image of E holds (dilation B) . (union F) = union { ((dilation B) . X) where X is binary-image of E : X in F }

for F being binary-image-family of E

for B being non empty binary-image of E holds (dilation B) . (union F) = union { ((dilation B) . X) where X is binary-image of E : X in F }

proof end;

theorem :: MORPH_01:27

for E being RealLinearSpace

for A, B, C being non empty binary-image of E st A c= B holds

(dilation C) . A c= (dilation C) . B

for A, B, C being non empty binary-image of E st A c= B holds

(dilation C) . A c= (dilation C) . B

proof end;

theorem :: MORPH_01:28

for E being RealLinearSpace

for v being Element of E

for A, C being non empty binary-image of E holds (dilation C) . (v + A) = v + ((dilation C) . A)

for v being Element of E

for A, C being non empty binary-image of E holds (dilation C) . (v + A) = v + ((dilation C) . A)

proof end;

theorem :: MORPH_01:29

for E being RealLinearSpace

for F being binary-image-family of E

for B being non empty binary-image of E holds (erosion B) . (meet F) = meet { ((erosion B) . X) where X is binary-image of E : X in F }

for F being binary-image-family of E

for B being non empty binary-image of E holds (erosion B) . (meet F) = meet { ((erosion B) . X) where X is binary-image of E : X in F }

proof end;

theorem :: MORPH_01:30

for E being RealLinearSpace

for A, B, C being non empty binary-image of E st A c= B holds

(erosion C) . A c= (erosion C) . B

for A, B, C being non empty binary-image of E st A c= B holds

(erosion C) . A c= (erosion C) . B

proof end;

theorem :: MORPH_01:31

for E being RealLinearSpace

for v being Element of E

for A, C being non empty binary-image of E holds (erosion C) . (v + A) = v + ((erosion C) . A)

for v being Element of E

for A, C being non empty binary-image of E holds (erosion C) . (v + A) = v + ((erosion C) . A)

proof end;

theorem :: MORPH_01:32

for E being RealLinearSpace

for A, C being non empty binary-image of E holds

( (dilation C) . ( the carrier of E \ A) = the carrier of E \ ((erosion C) . A) & (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A) )

for A, C being non empty binary-image of E holds

( (dilation C) . ( the carrier of E \ A) = the carrier of E \ ((erosion C) . A) & (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A) )

proof end;

theorem :: MORPH_01:33

for E being RealLinearSpace

for A, B, C being non empty binary-image of E holds

( (dilation C) . ((dilation B) . A) = (dilation ((dilation C) . B)) . A & (erosion C) . ((erosion B) . A) = (erosion ((dilation C) . B)) . A )

for A, B, C being non empty binary-image of E holds

( (dilation C) . ((dilation B) . A) = (dilation ((dilation C) . B)) . A & (erosion C) . ((erosion B) . A) = (erosion ((dilation C) . B)) . A )

proof end;