19.4. THE ORDER OF POINTFREE FUNCOIDS

290

Proof.

Reflexivity. Obvious.

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

1522

.

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

pFCD

(

A

,

B

) where

A

and

B

are posets. We do not need to compare pointfree

funcoids with different sources or destinations.

Obvious

1523

.

f

v

g

[

f

]

[

g

] for every

f, g

pFCD

(

A

,

B

) for every posets

A

and

B

.

Theorem

1524

.

If

A

and

B

are separable posets then

f

v

g

[

f

]

[

g

].

Proof.

From the theorem

1498

.

Proposition

1525

.

If

A

and

B

have least elements, then

pFCD

(

A

,

B

) has least

element.

Proof.

It is (

A

,

B

,

A

× {⊥

B

}

,

B

× {⊥

A

}

).

Theorem

1526

.

If

A

and

B

are bounded posets, then

pFCD

(

A

,

B

) is bounded.

Proof.

That

pFCD

(

A

,

B

) has least element was proved above. I will demon-

strate that (

A

,

B

, α, β

) is the greatest element of

pFCD

(

A

,

B

) for

αX

=

(

B

if

X

=

A

>

B

if

X

6

=

A

;

βY

=

(

A

if

Y

=

B

>

A

if

Y

6

=

B

.

First prove

Y

6

αX

X

6

βY

.

If

>

B

=

B

then

Y

6

αX

Y

6 ⊥

B

0

X

6 ⊥

A

X

6

β

A

(proposition

1499

). The case

>

A

=

A

is similar. So we can assume

>

A

6

=

A

and

>

B

6

=

B

.

Consider all variants:

X

=

A

and

Y

=

B

.

Y

6

αX

0

X

6

βY

.

X

6

=

A

and

Y

6

=

B

.

αX

=

>

B

and

βY

=

>

A

;

Y

6

αX

Y

6 >

B

1

X

6 >

A

X

6

βY

(used that

>

A

6

=

A

and

>

B

6

=

B

).

X

=

A

and

Y

6

=

B

.

αX

=

B

(proposition

1499

and

βY

=

>

A

;

Y

6

αX

Y

6 ⊥

B

0

⇔ ⊥

A

6

βY

X

6

βY

.

X

=

A

and

Y

6

=

B

. Similar.

It’s easy to show that both

α

and

β

are the greatest possible components of a

pointfree funcoid taking into account proposition

1499

.

Theorem

1527

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices. Then for

R

P

pFCD

(

A

,

B

) and

X

Z

0

,

Y

Z

1

we have:

1

.

X

[

d

R

]

Y

⇔ ∃

f

R

:

X

[

f

]

Y

;

2

.

h

d

R

i

X

=

d

f

R

h

f

i

X

.

Proof.