 and we have (

6.10

obviously.

(

.

Let (

6.10

hold. Then

G

(

) =

F

atoms

G

(

)

and thus

f

=

G

f"

Src

f

f

FCD

b

j

2

Src

f ; b

2

atoms

G

(

)

g

and so

f

is complete.

Theorem 6.115.

1. For a complete funcoid

f

there exists exactly one function

F

2

F

(

Dst

f

)

Src

f

such that

f

=

G

f"

Src

f

f

FCD

F

(

)

j

2

Src

f

g

:

2. For a co-complete funcoid

f

there exists exactly one function

F

2

F

(

Src

f

)

Dst

f

such that

f

=

G

f

F

(

)

FCD

"

Dst

f

f

g j

2

Dst

f

g

:

Proof.

We will prove only the rst as the second is similar. Let

f

=

G

f"

Src

f

f

FCD

F

(

)

j

2

Src

f

g

=

G

f"

Src

f

f

FCD

G

(

)

j

2

Src

f

g

for some

F ; G

2

F

(

Dst

f

)

Src

f

. We need to prove

F

=

G

. Let

2

Src

f

.

h

f

i

f

g

=

G

fh"

Src

f

f

FCD

F

(

)

i

f

g j

2

Src

f

g

=

F

(

)

:

Similarly

h

f

i

f

g

=

G

(

)

. So

F

(

) =

G

(

)

.

6.12 Funcoids corresponding to pretopologies

Let

be a pretopology on a set

U

and cl the preclosure corresponding to it (see theorem

5.12

).

Both induce a funcoid, I will show that these two funcoids are reverse of each other:

Theorem 6.116.

Let

f

be a complete funcoid dened by the formula

h

f

i

f

x

g

= (

x

)

for every

x

2

U

, let

g

be a co-complete funcoid dened by the formula

h

g

i

X

=

"

U

cl

(

X

)

for every

X

2

P

U

.

Then

g

=

f

¡

1

.

Remark 6.117.

It is obvious that funcoids

f

and

g

exist.

Proof.

X

[

g

]

Y

, "

U

Y

/

h

g

i"

U

X

,

Y

/

cl

(

X

)

, 9

y

2

Y

: (

y

)

/

"

U

X

, 9

y

2

Y

:

h

f

i

f

y

/

"

U

X

,

(proposition

4.194

and properties of complete funcoids)

,h

f

i

Y

/

"

U

X

,

Y

[

f

]

X

.

So

g

=

f

¡

1

.

6.13 Completion of funcoids

Theorem 6.118.

Cor

f

=

Cor

0

f

for an element

f

of a ltrator of funcoids.

Proof.

By theorems

4.34

and

6.108

.

Denition 6.119.

Completion

of a funcoid

f

2

FCD

(

A

;

B

)

is the complete funcoid Compl

f

2

FCD

(

A

;

B

)

dened by the formula

h

Compl

f

i

f

g

=

h

f

i

f

g

for

2

Src

f

.

Denition 6.120.

Co-completion

of a funcoid

f

is dened by the formula

CoCompl

f

= (

Compl

f

¡

1

)

¡

1

:

Obvious 6.121.

Compl

f

v

f

and CoCompl

f

v

f

.

114

Funcoids