 8

X

2

P

A; Y

2

P

B

:

¡

"

B

Y

u h

f

i"

A

X

=

/ 0

F

(

B

)

, "

A

X

[

f

]

"

B

Y

,

X  Y

, "

B

Y

u

X

=

/ 0

F

(

B

)

,

consequently

8

X

2

P

A

:

X

=

h

f

i"

A

X

=

h

f

i

X

.

Note that by the last theorem to every proximity

corresponds a unique funcoid. So funcoids

are a generalization of (quasi-)proximity structures. Reverse funcoids can be considered as a gen-
eralization of conjugate quasi-proximity.

Denition 6.29.

Any (multivalued) function

F

:

A

!

B

corresponds to a funcoid

"

FCD

(

A

;

B

)

F

2

FCD

(

A

;

B

)

, where by denition

"

FCD

(

A

;

B

)

F

X

=

d

h"

B

ihh

F

iiX

for every

X 2

F

(

A

)

.

Using the last theorem it is easy to show that this denition is monovalued and does not

contradict to former stu. (Take

=

"

B

h

F

i

.)

Denition 6.30.

"

FCD

f

=

def

¡

Src

f

;

Dst

f

;

"

FCD

(

Src

f

;

Dst

f

)

GR

f

for every Rel-morphism

f

.

Denition 6.31.

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 6.32.

If

S

is a generalized lter 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

2

S

and thus

h

f

i

d

S

v

d

hh

f

ii

S

.

By properties of generalized lter bases:

h

f

i

d

S

=

d

hh

f

i

i

d

S

=

d

hh

f

i

if

X

j 9P 2

S

:

X

2 P g

=

d

fh

f

i

X

j 9P 2

S

:

X

2 P g w

d

fh

f

iP j P 2

S

g

=

d

hh

f

ii

S:

6.4 Lattices of funcoids

Denition 6.33.

f

v

g

=

def

[

f

]

[

g

]

for

f ; g

2

FCD

.

Thus every

FCD

(

A

;

B

)

is a poset. (It's taken into account that

[

f

]=

/ [

g

]

when

f

=

/

g

.)

We will consider ltrators (

ltrators of funcoids

) whose base is

FCD

(

A

;

B

)

and whose core are

principal funcoids from

A

to

B

.

Lemma 6.34.

h

f

i

X

=

d

fh

F

i

X

j

F

2

up

f

g

for every funcoid

f

and set

X

2

P

(

Src

f

)

.

Proof.

Obviously

h

f

i

X

v

d

fh

F

i

X

j

F

2

up

f

g

.

Let

B

2 h

f

i

X

. Let

F

B

=

X

B

[

((

Src

f

)

n

X

)

Dst

f

.

h

F

B

i

X

=

B

.

Let

P

2

P

(

Src

f

)

. We have

;

=

/

P

X

) "

Dst

f

h

F

B

i

P

=

"

Dst

f

B

w h

f

i

P

and

;

=

/

P

*

X

) "

Dst

f

h

F

B

i

P

=

"

Dst

f

Dst

f

w h

f

i

P

. Thus

"

Dst

f

h

F

B

i

P

w h

f

i

P

for every

P

and

so

"

FCD

(

Src

f

;

Dst

f

)

F

B

w

f

that is

F

B

2

up

f

.

Thus

8

B

2 h

f

i

X

:

B

2

d

fh

F

i

X

j

F

2

up

f

g

because

B

2

"

FCD

(

Src

f

;

Dst

f

)

F

B

X

.

So

d

fh

F

i

X

j

F

2

up

f

g v h

f

i

X

.

Theorem 6.35.

h

f

iX

=

d

fh

F

iX j

F

2

up

f

g

for every funcoid

f

and

X 2

F

(

Src

f

)

.

Proof.

d

fh

F

iX j

F

2

up

f

g

=

d

f

d

hh

F

i

iX j

F

2

up

f

g

=

d

f

d

fh

F

i

X

j

X

2 X g j

F

2

up

f

g

=

d

f

d

fh

F

i

X

j

F

2

up

f

g j

X

2 X g

=

d

fh

f

i

X

j

X

2 X g

=

h

f

iX

(the lemma used).

Conjecture 6.36.

Every ltrator of funcoids is:

[TODO: Solved. See rewrite-plan.pdf]

1. with separable core;

100

Funcoids