6.4. LATTICES OF FUNCOIDS

106

1

.

X

hG

R

i

Y

Dst

f

Y

u

DG

R

E

X

6

=

F

(Dst

f

)

Dst

f

Y

u

G

h

f

i

X

f

R

f

R

:

Dst

f

Y

u h

f

i

X

6

=

F

(Dst

f

)

f

R

:

X

[

f

]

Y

(used proposition

461

).

In the next theorem, compared to the previous one, the class of infinite joins is

replaced with lesser class of finite joins and simultaneously class of sets is changed

to more wide class of filters.

Theorem

605

.

For every

f, g

FCD

(

A

;

B

) and

X ∈

F

(

A

) (for every sets

A

,

B

)

1

.

h

f

t

g

iX

=

h

f

iX t h

g

iX

;

2

. [

f

t

g

] = [

f

]

[

g

].

Proof.

1

Let

α

X

def

=

h

f

iX t h

g

iX

;

β

Y

def

=

f

1

Y t

g

1

Y

for every

X ∈

F

(

A

),

Y ∈

F

(

B

). Then

Y u

α

X 6

=

F

(

B

)

Y u h

f

iX 6

=

F

(

B

)

∨ Y u h

g

iX 6

=

F

(

B

)

X u

f

1

Y 6

=

F

(

A

)

∨ X u

g

1

Y 6

=

F

(

A

)

X u

β

Y 6

=

F

(

A

)

.

So

h

= (

A

;

B

;

α

;

β

) is a funcoid. Obviously

h

w

f

and

h

w

g

. If

p

w

f

and

p

w

g

for some funcoid

p

then

h

p

iX w h

f

iX t h

g

iX

=

h

h

iX

that is

p

w

h

. So

f

t

g

=

h

.

2

For every

X ∈

F

(

A

),

Y ∈

F

(

B

) we have

X

[

f

t

g

]

Y ⇔

Y u h

f

t

g

iX 6

=

F

(

B

)

Y u

(

h

f

iX t h

g

iX

)

6

=

F

(

B

)

Y u h

f

iX 6

=

F

(

B

)

∨ Y u h

g

iX 6

=

F

(

B

)

X

[

f

]

Y ∨ X

[

g

]

Y

.

Definition

606

.

GR

f

def

=

n

F

P

(Src

f

×

Dst

f

)

FCD

(Src

f

;Dst

f

)

F

w

f

o

.

Definition

607

.

xyGR

f

=

n

(Src

f

;Dst

f

;

F

)

F

GR

f

o

.

Remark

608

.

xyGR

f

is a set of

Rel

-morphisms.