 Transitivity.

It follows from transitivity of the order relations on

A

and

B

.

Antisymmetry.

It follows from antisymmetry of the order relations on

A

and

B

.

Remark 15.30.

It is enough to dene order of pointfree funcoids on every set

FCD

(

A

;

B

)

where

A

and

B

are posets. We do not need to compare pointfree funcoids with dierent sources or

destinations.

Obvious 15.31.

f

v

g

)

[

f

]

[

g

]

for every

f ; g

2

FCD

(

A

;

B

)

for every posets

A

and

B

.

Theorem 15.32.

If

A

and

B

are separable posets then

f

v

g

,

[

f

]

[

g

]

.

Proof.

From the theorem

15.12

.

Theorem 15.33.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over boolean lattices. Then for

R

2

P

FCD

(

A

;

B

)

and

X

2

Z

0

,

Y

2

Z

1

we have:

1.

X

[

F

R

]

Y

, 9

f

2

R

:

X

[

f

]

Y

;

2.

h

F

R

i

X

=

F

fh

f

i

X

j

f

2

R

g

.

Proof.

2.

X

=

def

F

fh

f

i

X

j

f

2

R

g

(by corollary

4.107

all joins on

B

exist). We have

0

A

= 0

B

;

(

I

t

Z

0

J

) =

G

fh

f

i

(

I

t

Z

0

J

)

j

f

2

R

g

=

G

fh

f

i

(

I

t

A

J

)

j

f

2

R

g

=

G

fh

f

i

I

t

B

h

f

i

J

j

f

2

R

g

=

G

fh

f

i

I

j

f

2

R

g t

B

G

fh

f

i

J

j

f

2

R

g

=

I

t

B

J

(used theorem

15.15

). By theorem

15.26

the function

can be continued to

h

h

i

for an

h

2

FCD

(

A

;

B

)

. Obviously

8

f

2

R

:

h

w

f :

(15.4)

And

h

is the least element of

FCD

(

A

;

B

)

for which the condition (

15.4

holds. So

h

=

F

R

.

1.

X

[

F

R

]

Y

,

Y

u

B

h

F

R

i

X

=

/ 0

B

,

Y

u

B

F

fh

f

i

X

j

f

2

R

g

=

/ 0

B

, 9

f

2

R

:

Y

u

B

h

f

i

X

=

/ 0

B

, 9

f

2

R

:

X

[

f

]

Y

(used theorem

4.118

).

Corollary 15.34.

If

(

A

;

Z

0

)

and

(

B

;

Z

1

)

are primary ltrators over boolean lattices then

FCD

(

A

;

B

)

is a complete lattice.

Proof.

Apply [

26

].

Theorem 15.35.

Let

A

and

B

be starrish join-semilattices. Then for

f ; g

2

FCD

(

A

;

B

)

:

1.

h

f

t

g

i

x

=

h

f

i

x

t h

g

i

x

for every

x

2

A

;

2.

[

f

t

g

]=[

f

]

[

[

g

]

.

Proof.

1. Let

X

=

def

h

f

i

x

t h

g

i

x

;

Y

=

def

h

f

¡

1

i

y

t h

g

¡

1

i

y

for every

x

2

A

,

y

2

B

. Then

y

/

x

,

y

/

h

f

i

x

_

y

/

h

g

i

x

,

x

/

h

f

¡

1

i

y

_

x

/

h

g

¡

1

i

y

,

x

/

h

f

¡

1

i

y

t h

g

¡

1

i

y

,

x

/

y:

So

h

= (

A

;

B

;

;

)

is a pointfree funcoid. Obviously

h

w

f

and

h

w

g

. If

p

w

f

and

p

w

g

for some

p

2

FCD

(

A

;

B

)

then

h

p

i

x

w h

f

i

x

t h

g

i

x

=

h

h

i

x

and

h

p

¡

1

i

y

w h

f

¡

1

i

y

t h

g

¡

1

i

y

=

h

h

¡

1

i

y

that is

p

w

h

.

So

f

t

g

=

h

.

182

Pointfree funcoids