background image

6.12. FUNCOIDS CORRESPONDING TO PRETOPOLOGIES

124

Theorem

681

.

1

. A funcoid

f

is complete iff there exists a function

G

: Src

f

F

(Dst

f

)

such that

f

=

G

Src

f

{

α

} ×

FCD

G

(

α

)

α

Src

f

.

(12)

2

. A funcoid

f

is co-complete iff there exists a function

G

: Dst

f

F

(Src

f

)

such that

f

=

G

G

(

α

)

×

FCD

Dst

f

{

α

}

α

Dst

f

.

Proof.

We will prove only the first as the second is symmetric.

. Let

f

be complete. Then take

G

(

α

) =

G

(

b

atoms

F

(Dst

f

)

Src

f

{

α

} ×

FCD

b

v

f

)

and we have (

12

obviously.

. Let (

12

hold. Then

G

(

α

) =

F

atoms

G

(

α

) and thus

f

=

G

Src

f

{

α

} ×

FCD

b

α

Src

f, b

atoms

G

(

α

)

and so

f

is complete.

Theorem

682

.

1

. For a complete funcoid

f

there exists exactly one function

F

F

(Dst

f

)

Src

f

such that

f

=

G

Src

f

{

α

} ×

FCD

F

(

α

)

α

Src

f

.

2

. For a co-complete funcoid

f

there exists exactly one function

F

F

(Src

f

)

Dst

f

such that

f

=

G

F

(

α

)

×

FCD

Dst

f

{

α

}

α

Dst

f

.

Proof.

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

f

=

G

Src

f

{

α

} ×

FCD

F

(

α

)

α

Src

f

=

G

Src

f

{

α

} ×

FCD

G

(

α

)

α

Src

f

for some

F, G

F

(Dst

f

)

Src

f

. We need to prove

F

=

G

. Let

β

Src

f

.

h

f

i

{

β

}

=

G

Src

f

{

α

} ×

FCD

F

(

α

)

{

β

}

α

Src

f

)

=

F

(

β

)

.

Similarly

h

f

i

{

β

}

=

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

543

).

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

other:

Theorem

683

.

Let

f

be a complete funcoid defined by the formula

h

f

i

{

x

}

=

∆(

x

) for every

x

U

, let g be a co-complete funcoid defined by the formula

h

g

i

X

=

U

cl(

X

) for every

X

P

U

. Then

g

=

f

1

.