 7.9. SPECIFYING FUNCOIDS BY FUNCTIONS OR RELATIONS ON ATOMIC FILTERS 160

Proposition

871

.

FCD

is a functor from

Rel

to

FCD

.

Proof.

FCD

(

g

f

) =

FCD

g

◦ ↑

FCD

f

was proved above.

FCD

1

Rel

A

= 1

FCD

A

is

obvious.

7.9. Specifying funcoids by functions or relations on atomic filters

Theorem

872

.

For every funcoid

f

and

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

)

1

.

h

f

iX

=

d

hh

f

ii

atoms

X

;

2

.

X

[

f

]

Y ⇔ ∃

x

atoms

X

, y

atoms

Y

:

x

[

f

]

y

.

Proof.

1

.

Y u h

f

iX 6

=

⊥ ⇔

X u

f

1

Y 6

=

⊥ ⇔

x

atoms

X

:

x

u

f

1

Y 6

=

⊥ ⇔

x

atoms

X

:

Y u h

f

i

x

6

=

.

h

f

iX

=

d

h

i

hh

f

ii

atoms

X

=

d

hh

f

ii

atoms

X

.

So

h

f

iX

=

d

hh

f

ii

atoms

X

by corollary

565

.

2

If

X

[

f

]

Y

, then

Y u h

f

iX 6

=

, consequently there exists

y

atoms

Y

such

that

y

u h

f

iX 6

=

,

X

[

f

]

y

. Repeating this second time we get that there exists

x

atoms

X

such that

x

[

f

]

y

. From this it follows

x

atoms

X

, y

atoms

Y

:

x

[

f

]

y.

The reverse is obvious.

Corollary

873

.

Let

f

be a funcoid.

The value of

f

can be restored from the value of

h

f

i|

atoms

F

(Src

f

)

.

The

value

of

f

can

be

restored

from

the

value

of

[

f

]

|

atoms

F

(Src

f

)

×

atoms

F

(Dst

f

)

.

Theorem

874

.

Let

A

and

B

be sets.

1

. A function

α

F

(

B

)

atoms

F

(

A

)

such that (for every

a

atoms

F

(

A

)

)

αa

v

l

D

l

◦h

α

i

atoms

◦ ↑

E

up

a

(10)

can be continued to the function

h

f

i

for a unique

f

FCD

(

A, B

);

h

f

iX

=

l

h

α

i

atoms

X

(11)

for every

X ∈

F

(

A

).

2

. A relation

δ

P

(atoms

F

(

A

)

×

atoms

F

(

B

)

) such that (for every

a

atoms

F

(

A

)

,

b

atoms

F

(

B

)

)

X

up

a, Y

up

b

x

atoms

X, y

atoms

Y

:

x δ y

a δ b

(12)

can be continued to the relation [

f

] for a unique

f

FCD

(

A, B

);

X

[

f

]

Y ⇔ ∃

x

atoms

X

, y

atoms

Y

:

x δ y

(13)

for every

X ∈

F

(

A

),

Y ∈

F

(

B

).

Proof.

Existence of no more than one such funcoids and formulas (

11

and

(

13

follow from the previous theorem.