6.13. COMPLETION OF FUNCOIDS

126

Proof.

CoCompl

f

v

f

thus

h

CoCompl

f

i

X

v h

f

i

X

but

h

CoCompl

f

i

X

is a principal filter thus

h

CoCompl

f

i

X

v

Cor

h

f

i

X

.

Let

αX

= Cor

h

f

i

X

. Then

α

=

F

(Dst

f

)

and

α

(

X

Y

) = Cor

h

f

i

(

X

Y

) = Cor(

h

f

i

X

th

f

i

Y

) = Cor

h

f

i

X

t

Cor

h

f

i

Y

=

αX

t

αY

(used theorem

490

). Thus

α

can be continued till

h

g

i

for some funcoid

g

. This

funcoid is co-complete.

Evidently

g

is the greatest co-complete element of

FCD

(Src

f

; Dst

f

) which is

lower than

f

.

Thus

g

= CoCompl

f

and Cor

h

f

i

X

=

αX

=

h

g

i

X

=

h

CoCompl

f

i

X

.

Theorem

692

.

ComplFCD

(

A

;

B

) is an atomistic lattice.

Proof.

Let

f

ComplFCD

(

A

;

B

).

h

f

i

X

=

G

h

f

i

{

x

}

x

X

=

G

f

|

Src

f

{

x

}

{

x

}

x

X

)

=

G

f

|

Src

f

{

x

}

X

x

X

)

,

thus

f

=

F

n

f

|

Src

f

{

x

}

x

X

o

. It is trivial that every

f

|

Src

f

{

x

}

is a join of atoms of

ComplFCD

(

A

;

B

).

Theorem

693

.

A funcoid is complete iff it is a join (on the lattice

FCD

(

A

;

B

))

of atomic complete funcoids.

Proof.

It follows from the theorem

673

and the previous theorem.

Corollary

694

.

ComplFCD

(

A

;

B

) is join-closed.

Theorem

695

.

Compl

F

R

=

F

h

Compl

i

R

for every

R

P

FCD

(

A

;

B

) (for

every sets

A

,

B

).

Proof.

For every set

X

D

Compl

G

R

E

X

=

G

h

F

R

i

{

α

}

α

X

=

G

F

n

h

f

i

{

α

}

f

R

o

α

X

=

G

F

n

h

f

i

{

α

}

α

X

o

f

R

=

G

h

Compl

f

i

X

f

R

=

DG

h

Compl

i

R

E

X.

Corollary

696

.