 7.2. BASIC DEFINITIONS

145

For every binary relation

p

on a set

f

there exists unique funcoid

f

such that

X

P

f

:

h

f

i ↑

X

=

↑ h

p

i

X

(where

h

p

i

is defined in the introduction), recall that a funcoid is uniquely deter-

mined by the values of its first component on sets. I will call such funcoids

principal

.

So funcoids are a generalization of binary relations.

Composition of binary relations (i.e. of principal funcoids) complies with the

formulas:

h

g

f

i

=

h

g

i

◦ h

f

i

and

(

g

f

)

1

=

f

1

g

1

.

By similar formulas we can define composition of every two funcoids. Funcoids with

this composition form a category (

the category of funcoids

).

Also funcoids can be reversed (like reversal of

X

and

Y

in a binary relation)

by the formula (

α, β

)

1

= (

β, α

). In the particular case if

µ

is a proximity we have

µ

1

=

µ

because proximities are symmetric.

Funcoids behave similarly to (multivalued) functions but acting on filters in-

stead of acting on sets. Below there will be defined domain and image of a funcoid

(the domain and the image of a funcoid are filters).

7.2. Basic definitions

Definition

800

.

Let us call a

funcoid

from a set

A

to a set

B

(

A, B, α, β

) where

α

F

(

B

)

F

(

A

)

,

α

F

(

A

)

F

(

B

)

such that

∀X ∈

F

(

A

)

,

Y ∈

F

(

B

) : (

Y 6

α

X ⇔ X 6

β

Y

)

.

Definition

801

.

Source

and

destination

of every funcoid (

A, B, α, β

) are de-

fined as:

Src(

A, B, α, β

) =

A

and Dst(

A, B, α, β

) =

B.

I will denote

FCD

(

A, B

) the set of funcoids from

A

to

B

.

I will denote

FCD

the set of all funcoids (for small sets).

Definition

802

.

I will call an

endofuncoid

a funcoid whose source is the same

as it’s destination.

Definition

803

.

h

(

A, B, α, β

)

i

def

=

α

for a funcoid (

A, B, α, β

).

Definition

804

.

The

reverse

funcoid (

A, B, α, β

)

1

= (

B, A, β, α

) for a fun-

coid (

A, B, α, β

).

Note

805

.

The reverse funcoid is

not

an inverse in the sense of group theory

or category theory.

Proposition

806

.

If

f

is a funcoid then

f

1

is also a funcoid.

Proof.

It follows from symmetry in the definition of funcoid.

Obvious

807

.

(

f

1

)

1

=

f

for a funcoid

f

.

Definition

808

.

The relation [

f

]

P

(

F

(Src

f

)

×

F

(Dst

f

)) is defined (for

every funcoid

f

and

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

) by the formula

X

[

f

]

Y ⇔ Y 6

h

f

iX

.

Obvious

809

.

X

[

f

]

Y ⇔ Y 6 h

f

iX ⇔ X 6

f

1

Y

for every funcoid

f

and

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

).

Obvious

810

.

f

1

=[

f

]

1

for a funcoid

f

.

Theorem

811

.

Let

A

,

B

be sets.