background image

15.11. COMPLETE POINTFREE FUNCOIDS

221

1

2

For every

S

P

A

,

J

Z

1

we have

f

1

J

Z

0

, consequently

S

P

A

, J

Z

1

:

 

A

G

S

6

f

1

J

⇒ ∃I ∈

S

:

I 6

f

1

J

!

.

From this follows

2

.

2

4

Let

h

f

i

F

Z

0

S

and

F

B

hh

f

ii

S

be defined. We have

h

f

i

F

A

S

=

h

f

i

F

Z

0

S

.

J

u

B

h

f

i

A

G

S

6

=

B

A

G

S

[

f

]

J

∃I ∈

S

:

I

[

f

]

J

∃I ∈

S

:

J

u

B

h

f

iI 6

=

B

J

u

B

B

G

hh

f

ii

S

6

=

B

(used theorem

320

). Thus

h

f

i

F

A

S

=

F

B

hh

f

ii

S

by star-separability of

(

B

;

Z

1

).

5

3

Let

h

f

i

F

Z

0

S

be defined.

Then

F

B

hh

f

ii

S

is also defined because

h

f

i

F

Z

0

S

=

F

B

hh

f

ii

S

. Then

Z

0

G

S

[

f

]

J

J

u

B

h

f

i

Z

0

G

S

6

=

B

J

u

B

B

G

hh

f

ii

S

6

=

B

what by theorem

320

is equivalent to

I

S

:

J

u

B

h

f

i

I

6

=

B

that is

I

S

:

I

[

f

]

J

.

2

3

,

4

5

By join-closedness of the core of (

A

;

Z

0

).

Theorem

1149

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices. If

R

is a set of co-complete pointfree funcoids in

FCD

(

A

;

B

) then

F

R

is a

co-complete pointfree funcoid.

Proof.

Let

R

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

X

Z

0

DG

R

E

X

=

B

G

h

f

i

X

f

R

=

Z

1

G

h

f

i

X

f

R

Z

1

(used the theorem

1089

and corollary

363

).

Let

A

and

B

be posets with least elements. I will denote

ComplFCD

(

A

;

B

) and

CoComplFCD

(

A

;

B

) the sets of complete and co-complete funcoids correspondingly

from a poset

A

to a poset

B

.

Proposition

1150

.

1

. Let

f

ComplFCD

(

A

;

B

) and

g

ComplFCD

(

B

;

C

) where

A

and

C

are

posets with least elements and

B

is a complete lattice. Then

g

f

ComplFCD

(

A

;

C

).

2

. Let

f

CoComplFCD

(

A

;

B

) and

g

CoComplFCD

(

B

;

C

) where

A

,

B

and

C

are posets with least elements and (

A

;

Z

0

), (

B

;

Z

1

), (

C

;

Z

2

) are filtrators.

Then

g

f

CoComplFCD

(

A

;

C

).

Proof.

1

Let

F

S

and

F

hh

g

f

ii

S

be defined. Then

FiXme

: Is

F

hh

f

ii

S

defined?

h

g

f

i

G

S

=

h

g

ih

f

i

G

S

=

h

g

i

G

hh

f

ii

S

=

G

hh

g

ii

hh

f

ii

S

=

G

hh

g

f

ii

S.