 9.4. FUNCOIDAL RELOIDS

207

9.4. Funcoidal reloids

Definition

1110

.

I call

funcoidal

such a reloid

ν

that

X ×

RLD

Y 6

ν

∃X

0

F

(Base(

X

))

\{⊥}

,

Y

0

F

(Base(

Y

))

\{⊥}

: (

X

0

v X ∧Y

0

v Y∧X

0

×

RLD

Y

0

v

ν

)

for every

X ∈

F

(Src

ν

),

Y ∈

F

(Dst

ν

).

Remark

1111

.

See theorem

1116

below for how they are bijectively related

with funcoids (and thus named funcoidal).

Proposition

1112

.

A reloid

ν

is funcoidal iff

x

×

RLD

y

6

ν

x

×

RLD

y

v

ν

for every atomic filter objects

x

and

y

on respective sets.

Proof.

.

x

×

RLD

y

6

ν

⇒ ∃X

0

atoms

x,

Y

0

atoms

y

:

X

0

×

RLD

Y

0

v

ν

x

×

RLD

y

v

ν

.

.

X ×

RLD

Y 6

ν

x

atoms

X

, y

atoms

Y

:

x

×

RLD

y

6

ν

x

atoms

X

, y

atoms

Y

:

x

×

RLD

y

v

ν

∃X

0

F

(Base(

X

))

\{⊥}

,

Y

0

F

(Base(

Y

))

\{⊥}

: (

X

0

v X ∧Y

0

v Y∧X

0

×

RLD

Y

0

v

ν

)

.

Proposition

1113

.

(

RLD

)

in

(

FCD

)

f

=

d

n

a

×

RLD

b

a

atoms

F

(Src

ν

)

,b

atoms

F

(Dst

ν

)

,a

×

RLD

b

6

f

o

.

Proof.

(

RLD

)

in

(

FCD

)

f

=

l

a

×

RLD

b

a

atoms

F

(Src

ν

)

, b

atoms

F

(Dst

ν

)

, a

×

FCD

b

v

(

FCD

)

f

=

l

a

×

RLD

b

a

atoms

F

(Src

ν

)

, b

atoms

F

(Dst

ν

)

, a

[(

FCD

)

f

]

b

=

l

a

×

RLD

b

a

atoms

F

(Src

ν

)

, b

atoms

F

(Dst

ν

)

, a

×

RLD

b

6

f

.

Definition

1114

.

I call (

RLD

)

in

(

FCD

)

f

funcoidization

of a reloid

f

.

Lemma

1115

.

(

RLD

)

in

(

FCD

)

f

is funcoidal for every reloid

f

.

Proof.

x

×

RLD

y

6

(

RLD

)

in

(

FCD

)

f

x

×

RLD

y

v

(

RLD

)

in

(

FCD

)

f

for atomic

filters

x

and

y

.

Theorem

1116

.

(

RLD

)

in

is a bijection from

FCD

(

A, B

) to the set of funcoidal

reloids from

A

to

B

. The reverse bijection is given by (

FCD

).

Proof.

Let

f

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.