7.5. LATTICES OF FUNCOIDS

153

2

.

A

(

ξ

ν

)

C

⇔ ∃

B

: (

A ν

B

B ξ

C

)

B

: (

B

up

h

ν

i

A

C

up

h

ξ

i

B

)

⇔ ∃

B

up

h

ν

i

A

:

C

up

h

ξ

i

B.

A

(

ξ

ν

)

C

C

up

h

ξ

ν

i

B

C

up

h

ξ

ih

ν

i

B

.

It remains to prove

B

up

h

ν

i

A

:

C

up

h

ξ

i

B

C

up

h

ξ

ih

ν

i

A.

B

up

h

ν

i

A

:

C

up

h

ξ

i

B

C

up

h

ξ

ih

ν

i

A

is obvious.

Let

C

up

h

ξ

ih

ν

i

A

. Then

C

up

d

hh

ξ

ii

up

h

ν

i

A

; so by properties of general-

ized filter bases,

P

∈ hh

ξ

ii

up

h

ν

i

A

:

C

up

P

;

B

up

h

ν

i

A

:

C

up

h

ξ

i

B

.

Remark

848

.

The above theorem is interesting by the fact that composition

of funcoids is represented as relational composition of binary relations.

7.5. Lattices of funcoids

Definition

849

.

f

v

g

def

= [

f

]

[

g

] for

f, g

FCD

(

A, B

) for every sets

A

,

B

.

Thus every

FCD

(

A, B

) is a poset. (It’s taken into account that [

f

]

6

= [

g

] when

f

6

=

g

.)

We will consider filtrators (

filtrators of funcoids

) whose base is

FCD

(

A, B

) and

whose core are principal funcoids from

A

to

B

.

Lemma

850

.

h

f

i

X

=

d

F

F

up

f

h

F

i

X

for every funcoid

f

and typed set

X

T

(Src

f

).

Proof.

Obviously

h

f

i

X

v

d

F

F

up

f

h

F

i

X

.

Let

B

up

h

f

i

X

. Let

F

B

=

X

×

B

t

X

× >

.

h

F

B

i

X

=

B

.

Let

P

T

(Src

f

). We have

⊥ 6

=

P

v

X

⇒ h

F

B

i

P

=

B

w h

f

i

P

and

P

6v

X

⇒ h

F

B

i

P

=

> w h

f

i

P.

Thus

h

F

B

i

P

w h

f

i

P

for every

P

and so

F

B

w

f

that is

F

B

up

f

.

Thus

B

up

h

f

i

X

:

B

up

d

F

F

up

f

h

F

i

X

because

B

up

h

F

B

i

X

.

So

d

F

up

f

h

F

i

X

v h

f

i

X

.

Theorem

851

.

h

f

iX

=

d

F

F

up

f

h

F

iX

for every funcoid

f

and

X ∈

F

(Src

f

).