 6.2. BASIC DEFINITIONS

98

(where

h

p

i

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

determined 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 these will be defined domain and image of a funcoid

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

6.2. Basic definitions

Definition

568

.

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

)

.

Further we will assume that all funcoids in consideration are small without

mentioning it explicitly.

FiXme

: It is superfluous.

Definition

569

.

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

570

.

h

(

A

;

B

;

α

;

β

)

i

def

=

α

for a funcoid (

A

;

B

;

α

;

β

).

Definition

571

.

The

reverse

funcoid (

A

;

B

;

α

;

β

)

1

= (

B

;

A

;

β

;

α

) for a fun-

coid (

A

;

B

;

α

;

β

).

Note

572

.

The reverse funcoid is

not

an inverse in the sense of group theory

or category theory.

Proposition

573

.

If

f

is a funcoid then

f

1

is also a funcoid.

Proof.

It follows from symmetry in the definition of funcoid.

Obvious

574

.

(

f

1

)

1

=

f

for a funcoid

f

.

Definition

575

.

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

576

.

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

577

.

f

1

=[

f

]

1

for a funcoid

f

.

Theorem

578

.

Let

A

,

B

be sets.

1

. For given value of

h

f

i ∈

F

(

B

)

F

(

A

)

there exists no more than one funcoid

f

FCD

(

A

;

B

).

2

. For given value of [

f

]

P

(

F

(

A

)

×

F

(

B

)) there exists no more than one

funcoid

f

FCD

(

A

;

B

).