background image

Proof.

"

FCD

f

(

x

;

y

)

g v

(

FCD

)

g

, "

FCD

f

(

x

;

y

)

/ (

FCD

)

g

, f

x

g

[(

FCD

)

g

]

f

y

g , "

RLD

f

(

x

;

y

)

/

g

, "

RLD

f

(

x

;

y

)

g v

g

.

Theorem 8.40.

Cor

(

FCD

)

g

= (

FCD

)

Cor

g

for every reloid

g

.

Proof.

Cor

(

FCD

)

g

=

F

f"

FCD

f

(

x

;

y

)

g j "

FCD

f

(

x

;

y

)

g v

(

FCD

)

g

g

=

F

f"

FCD

f

(

x

;

y

)

g j "

RLD

f

(

x

;

y

)

g v

g

g

=

F

f

(

FCD

)

"

RLD

f

(

x

;

y

)

g j "

RLD

f

(

x

;

y

)

g v

g

g

= (

FCD

)

F

f"

RLD

f

(

x

;

y

)

g j "

RLD

f

(

x

;

y

)

g v

g

g

=

(

FCD

)

Cor

g

.

Conjecture 8.41.

For every funcoid

g

1. Cor

(

RLD

)

in

g

= (

RLD

)

in

Cor

g

;

2. Cor

(

RLD

)

out

g

= (

RLD

)

out

Cor

g

.

8.4 Funcoidal reloids

Denition 8.42.

I call

funcoidal

such a reloid

that

RLD

/

) 9X

0

2

F

(

Base

(

X

))

n f

0

g

;

Y

0

2

F

(

Base

(

Y

))

n f

0

g

: (

X

0

v X ^ Y

0

v Y ^ X

0

RLD

Y

0

v

)

for every

X 2

F

(

Src

)

,

Y 2

F

(

Dst

)

.

Proposition 8.43.

A reloid

is funcoidal i

x

RLD

y

/

)

x

RLD

y

v

for every ultralters

x

and

y

on respective sets.

Proof.

)

.

x

RLD

y

/

) 9X

0

2

atoms

x;

Y

0

2

atoms

y

:

X

0

RLD

Y

0

v

)

x

RLD

y

v

.

(

.

RLD

/

) 9

x

2

atoms

X

; y

2

atoms

Y

:

x

RLD

y

/

) 9

x

2

atoms

X

; y

2

atoms

Y

:

x

RLD

y

v

) 9X

0

2

F

(

Base

(

X

))

n f

0

g

;

Y

0

2

F

(

Base

(

Y

))

n f

0

g

: (

X

0

v X ^ Y

0

v Y ^

X

0

RLD

Y

0

v

)

.

Proposition 8.44.

(

RLD

)

in

(

FCD

)

f

=

a

RLD

b

j

a

2

atoms

F

(

Src

)

; b

2

atoms

F

(

Dst

)

; a

RLD

b

/

f

 

.

Proof.

(

RLD

)

in

(

FCD

)

f

=

a

RLD

b

j

a

2

atoms

F

(

Src

f

)

; b

2

atoms

F

(

Dst

f

)

; a

FCD

b

v

(

FCD

)

f

 

=

a

RLD

b

j

a

2

atoms

F

(

Src

f

)

; b

2

atoms

F

(

Dst

f

)

; a

[(

FCD

)

f

]

b

 

=

a

RLD

b

j

a

2

atoms

F

(

Src

f

)

;

b

2

atoms

F

(

Src

f

)

; a

RLD

b

/

f

 

.

Denition 8.45.

I call

(

RLD

)

in

(

FCD

)

f

funcoidization

of a reloid

f

.

Lemma 8.46.

(

RLD

)

in

(

FCD

)

f

is funcoidal for every reloid

f

.

Proof.

x

RLD

y

/ (

RLD

)

in

(

FCD

)

f

)

x

RLD

y

v

(

RLD

)

in

(

FCD

)

f

.

Theorem 8.47.

(

RLD

)

in

is a bijection from

FCD

(

A

;

B

)

to the set of funcoidal reloids from

A

to

B

.

Proof.

Let

f

2

FCD

(

A

;

B

)

. Prove that

(

RLD

)

in

f

is funcoidal.

Really

(

RLD

)

in

f

= (

RLD

)

in

(

FCD

)(

RLD

)

in

f

and thus we can use the lemma stating that it is

funcoidal.

It remains to prove

(

RLD

)

in

(

FCD

)

f

=

f

for a funcoidal reloid

f

. (

(

FCD

)(

RLD

)

in

g

=

g

for every

funcoid

g

is already proved above.)

(

RLD

)

in

(

FCD

)

f

=

x

RLD

y

j

x

2

atoms

F

(

Src

)

; y

2

atoms

F

(

Dst

)

; x

RLD

y

/

f

 

=

p

2

atoms

(

x

RLD

y

)

j

x

2

atoms

F

(

Src

)

; y

2

atoms

F

(

Dst

)

; x

RLD

y

/

f

 

=

p

2

atoms

(

x

RLD

y

)

j

x

2

atoms

F

(

Src

)

; y

2

atoms

F

(

Dst

)

; x

RLD

y

v

f

 

=

F

atoms

f

=

f

.

Corollary 8.48.

Funcoidal reloids are convex.

Proof.

Every

(

RLD

)

in

f

is obviously convex.

8.4 Funcoidal reloids

137