 7.3. FUNCOID AS CONTINUATION

151

Using the last theorem it is easy to show that this definition is monovalued and

does not contradict to former stuff. (Take

α

=

↑ ◦h

F

i

.)

Proposition

831

.

FCD

f

X

=

h

f

i

X

for a

Rel

-morphism

f

and

X

T

Src

f

.

Proof.

FCD

f

X

= min

h↑i

h

f

i

up

X

=

↑ h

f

i

X

=

h

f

i

X

.

Corollary

832

.

FCD

f

= [

f

]

for every

Rel

-morphism

f

.

Proof.

X

FCD

f

Y

Y

6

FCD

f

X

Y

6 h

f

i

X

X

[

f

]

Y

for

X

T

Src

f

,

Y

T

Dst

f

.

Definition

833

.

FCD

(

A,B

)

f

=

FCD

(

A, B, f

) for every binary relation

f

be-

tween sets

A

and

B

.

Definition

834

.

Funcoids corresponding to a binary relation (= multivalued

function) are called

principal funcoids

.

Proposition

835

.

FCD

g

◦ ↑

FCD

f

=

FCD

(

g

f

) for composable morphisms

f

,

g

of category

Rel

.

Proof.

For every

X

T

Src

f

FCD

g

◦ ↑

FCD

f

X

=

FCD

g

FCD

f

X

=

h

g

i

h

f

i

X

=

h

g

f

i

X

=

FCD

(

g

f

)

X.

We may equate principal funcoids with corresponding binary relations by the

method of appendix

A

This is useful for describing relationships of funcoids and

binary relations, such as for the formulas of continuous functions and continuous

funcoids (see below).

Thus (

FCD

(

A, B

)

,

Rel

(

A, B

)) is a filtrator. I call it

filtrator of funcoids

.

Theorem

836

.

If

S

is a generalized filter base on Src

f

then

h

f

i

d

S

=

d

hh

f

ii

S

for every funcoid

f

.

Proof.

h

f

i

d

S

v h

f

i

X

for every

X

S

and thus

h

f

i

d

S

v

d

hh

f

ii

S

.

By properties of generalized filter bases:

h

f

i

l

S

=

l

h

f

i

up

l

S

=

l

h

f

i

X

∃P ∈

S

:

X

up

P

=

l

h

f

i

X

∃P ∈

S

:

X

up

P

w

l

P∈

S

h

f

iP

=

l

hh

f

ii

S.

Proposition

837

.

X

[

f

]

d

S

⇔ ∃Y ∈

S

:

X

[

f

]

Y

if

f

is a funcoid and

S

is a

generalized filter base on Dst

f

.