 7.12. COMPLETE FUNCOIDS

171

2

3

,

4

5

,

5

3

,

5

6

Obvious.

The following proposition shows that complete funcoids are a direct general-

ization of pretopological spaces.

Proposition

920

.

To specify a complete funcoid

f

it is enough to specify

h

f

i

on one-element sets, values of

h

f

i

on one element sets can be specified arbitrarily.

Proof.

From the above theorem is clear that knowing

h

f

i

on one-element

sets

h

f

i

can be found on every set and then the value of

h

f

i

can be inferred for

every filter.

Choosing arbitrarily the values of

h

f

i

on one-element sets we can define a

complete funcoid the following way:

h

f

i

X

=

d

α

atoms

X

h

f

i

α

for every

X

T

(Src

f

). Obviously it is really a complete funcoid.

Theorem

921

.

A funcoid is principal iff it is both complete and co-complete.

Proof.

. Obvious.

. Let

f

be both a complete and co-complete funcoid. Consider the relation

g

defined by that

↑ h

g

i

α

=

h

f

i

α

for one-element sets

α

(

g

is correctly

defined because

f

corresponds to a generalized closure). Because

f

is a

complete funcoid

f

is the funcoid corresponding to

g

.

Theorem

922

.

If

R

P

FCD

(

A, B

) is a set of (co-)complete funcoids then

d

R

is a (co-)complete funcoid (for every sets

A

and

B

).

Proof.

It is enough to prove for co-complete funcoids. Let

R

P

FCD

(

A, B

)

be a set of co-complete funcoids. Then for every

X

T

(Src

f

)

D

l

R

E

X

=

l

f

R

h

f

i

X

is a principal filter (used theorem

852

).

Corollary

923

.

If

R

is a set of binary relations between sets

A

and

B

then

d

FCD

(

A,B

)

R

=

FCD

(

A,B

)

S

R

.

Proof.

From two last theorems.

Lemma

924

.

Every funcoid is representable as meet (on the lattice of funcoids)

of binary relations of the form

X

×

Y

t

X

× >

T

(

B

)

(where

X

,

Y

are typed sets).

Proof.

Let

f

FCD

(

A, B

),

X

T

A

,

Y

up

h

f

i

X

,

g

(

X, Y

)

def

=

X

×

Y

t

X

×

>

T

(

B

)

. Then

g

(

X, Y

) =

X

×

FCD

Y

t

X

×

FCD

>

F

(

B

)

. For every

K

T

A

h

g

(

X, Y

)

i

K

=

X

×

FCD

Y

K

t

D

X

×

FCD

>

F

(

B

)

E

K

=

F

(

B

)

if

K

=

T

A

Y

if

T

A

6

=

K

v

X

>

F

(

B

)

if

K

6v

X

w h

f

i

K

;

so

g

(

X, Y

)

w

f

. For every

X

T

A

l

Y

up

h

f

i

X

h

g

(

X, Y

)

i

X

=

F

l

Y

up

h

f

i

X

Y

=

h

f

i

X

;