 Proof.

Backward implication is easy.

Let

=

'

j

P

A

. Then

preserves bottom element and binary joins. Thus there exists a funcoid

f

such that

h

f

i

=

.

It remains to prove that

h

f

i

=

'

.

Really,

h

f

iX

=

d

hh

f

i

i

X

=

d

h

i

X

=

d

h

'

i

X

=

'

d

X

=

'

X

for every

X 2

F

(

A

)

.

Corollary 6.

Funcoids

f

from

A

to

B

bijectively correspond by the formula

h

f

i

=

'

to functions

'

:

F

(

A

)

!

F

(

B

)

preserving nite joins and ltered meets.

2 Representing funcoids as binary relations

Denition 7.

The binary relation

~

2

P

(

F

(

Src

)

F

(

Dst

))

for a funcoid

is dened by the

formula

A

~

B ,B w h

iA

.

Denition 8.

The binary relation

2

P

(

P

Src

P

Dst

)

for a funcoid

is dened by the

formula

B

,

B

w h

i

A

,

B

2

up

h

i

A:

Proposition 9.

Funcoid

can be restored from

1. the value of

~

;

2. the value of

.

Proof.

1. The value of

h

i

can be restored from

~

.

2. The value of

h

i

can be restored from

.

Theorem 10.

Let

and

be composable funcoids. Then:

1.

~

~

= (

)

~

;

2.

= (

)

.

Proof.

1.

A

[

~

~

]

C , 9B

: (

A

~

B ^B

~

C

)

, 9B 2

F

(

Dst

): (

B w h

iA ^ C w h

iB

)

, C w h

ih

iA,

C w h

iA , A

[(

)

~

]

C

.

2.

A

[

]

C

, 9

B

: (

B

^

C

)

, 9

B

: (

B

2

up

h

i

A

^

C

2

up

h

i

B

)

, 9

B

2

up

h

i

A

:

C

2

up

h

i

B

.

A

[(

)

]

C

,

C

2

up

h

i

B

,

C

2

up

h

ih

i

B

.

It remains to prove

9

B

2

up

h

i

A

:

C

2

up

h

i

B

,

C

2

up

h

ih

i

A:

9

B

2

up

h

i

A

:

C

2

up

h

i

B

)

C

2

up

h

ih

i

A

is obvious.

Let

C

2

up

h

ih

i

A

. Then

C

2

up

d

hh

ii

up

h

i

A

; so by properties of generalized lter

bases,

9

P

2 hh

ii

up

h

i

A

:

C

2

up

P

;

9

B

2

up

h

i

A

:

C

2

up

h

i

B

.

Remark 11.

The above theorem is interesting by the fact that composition of funcoids is repre-

sented as relational composition of binary relations.

Bibliography



Victor Porton.

Algebraic General Topology. Volume 1

. 2014.

2