
Proof. Backward implication is easy.
Let = 'j
PA
. Then preserves bottom element and binary joins. Thus there exists a funcoid f
such that hf i
∗
= .
It remains to prove that hf i = '.
Really, hf iX =
d
hhf 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 hf i = ' to functions
': F(A) ! F(B) preserving finite joins and filtered meets.
2 Representing funcoids as binary relations
Definition 7. The binary relation ξ
~
2 P(F(Src ξ) × F(Dst ξ)) for a funcoid ξ is defined by the
formula A ξ
~
B ,B w hξ iA.
Definition 8. The binary relation ξ
∗
2 P(P Src ξ × P Dst ξ) for a funcoid ξ is defined by the
formula
A ξ
∗
B ,B w hξiA , B 2 up hξiA:
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 whξiB) ,C whξ ihνiA,
C w hξ ◦ ν iA , A [(ξ ◦ ν)
~
] C.
2. A [ξ
∗
◦ ν
∗
] C , 9B: (A ν
∗
B ^B ξ
∗
C ) , 9B: (B 2 up hν iA ^ C 2 up hξiB) , 9B 2 up hν iA:
C 2 up hξiB.
A [(ξ ◦ ν)
∗
] C , C 2 up hξ ◦ ν iB , C 2 up hξ ihν iB.
It remains to prove
9B 2 up hν iA: C 2 up hξiB , C 2 up hξ ihνiA:
9B 2 up hν iA: C 2 up hξiB ) C 2 up hξihν iA is obvious.
Let C 2 up hξ ihν iA. Then C 2 up
d
hhξ ii
∗
up hν iA; so by properties of generalized filter
bases, 9P 2 hhξii
∗
up hν iA: C 2 up P ; 9B 2 up hν iA: C 2 up hξ iB.
Remark 11. The above theorem is interesting by the fact that composition of funcoids is repre-
sented as relational composition of binary relations.
Bibliography
[1] Victor Porton. Algebraic General Topology. Volume 1. 2014.
2