 6.3. FUNCOID AS CONTINUATION

103

1

Let define the relation

δ

P

(

P

A

×

P

B

) by the formula

X δ Y

⇔↑

B

u

αX

6

=

F

(

B

)

.

That

¬

(

I δ

) and

¬

(

δ I

) is obvious. We have

I

J δ K

B

K

u

α

(

I

J

)

6

=

F

(

B

)

B

K

u

(

αI

t

αJ

)

6

=

F

(

B

)

B

K

u

αI

6

=

F

(

B

)

∨ ↑

B

K

u

αJ

6

=

F

(

B

)

I δ K

J δ K

and

K δ I

J

B

(

I

J

)

u

αK

6

=

F

(

B

)

(

B

I

t ↑

B

J

)

u

αK

6

=

F

(

B

)

B

I

u

αK

6

=

F

(

B

)

∨ ↑

B

J

u

αK

6

=

F

(

B

)

K δ I

K δ J.

That is the formulas (

5

are true.

Accordingly to the above there exists a funcoid

f

such that

X

[

f

]

Y ⇔ ∀

X

∈ X

, Y

∈ Y

:

X δ Y.

For every

X

P

A

,

Y

P

B

we have:

B

Y

u h

f

i ↑

A

X

6

=

F

(

B

)

⇔↑

A

X

[

f

]

B

Y

X δ Y

⇔↑

B

Y

u

αX

6

=

F

(

B

)

,

consequently

X

P

A

:

αX

=

h

f

i ↑

A

X

=

h

f

i

X

.

Note that by the last theorem to every proximity

δ

corresponds a unique fun-

coid. So funcoids are a generalization of (quasi-)proximity structures. Reverse

funcoids can be considered as a generalization of conjugate quasi-proximity.

Definition

596

.

Any (multivalued) function

F

:

A

B

corresponds to

a funcoid

FCD

(

A

;

B

)

F

FCD

(

A

;

B

), where by definition

FCD

(

A

;

B

)

F

X

=

d

B

h

F

i

X

for every

X ∈

F

(

A

).

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

does not contradict to former stuff. (Take

α

=

B

◦h

F

i

.)

Definition

597

.

FCD

f

= (Src

f

; Dst

f

;

FCD

(Src

f

;Dst

f

)

GR

f

) for every

Rel

-

morphism

f

.

Definition

598

.

Funcoids corresponding to a binary relation (= multivalued

function) are called

principal funcoids

.

We may equate principal funcoids with corresponding binary relations by the

method of appendix B in [

29

]. This is useful for describing relationships of funcoids

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

funcoids (see below).

Theorem

599

.

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

.