6.11. COMPLETE FUNCOIDS

121

6

.

A

P

(Src

f

) :

h

f

i

A

=

F

n

h

f

i

{

a

}

a

A

o

.

Proof.

3

1

For every

S

PP

(Src

f

),

J

P

(Dst

f

)

Src

f

[

S

u

f

1

J

6

=

F

(Src

f

)

⇔ ∃

I

S

:

Src

f

u

f

1

J

6

=

F

(Src

f

)

,

consequently by proposition

482

we have that

f

1

J

is a principal filter.

1

2

For every

S

P

F

(Src

f

),

J

P

(Dst

f

) we have that

f

1

J

is a prin-

cipal filter, consequently

G

S

u

f

1

J

6

=

F

(Src

f

)

⇔ ∃I ∈

S

:

I u

f

1

J

6

=

F

(Src

f

)

.

From this follows

2

.

6

5

.

h

f

i

[

S

=

G

h

f

i

{

a

}

a

S

S

=

G [

n

h

f

i

{

a

}

a

A

o

A

S

=

G

F

n

h

f

i

{

a

}

a

A

o

A

S

=

G

h

f

i

A

A

S

=

G

h

f

i

S.

2

4

Using theorem

482

,

Dst

f

J

6 h

f

i

G

S

G

S

[

f

]

Dst

f

J

∃I ∈

S

:

I

[

f

]

Dst

f

J

∃I ∈

S

:

Dst

f

J

6 h

f

iI ⇔

Dst

f

J

6

G

hh

f

ii

S.

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

671

.

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

=

F

n

h

f

i

{

α

}

α

X

o

for every

X

P

(Src

f

).

Obviously it is really a complete funcoid.