 15.4. THE ORDER OF POINTFREE FUNCOIDS

205

Taking into account properties of generalized filter bases:

h

f

i

Src

f

l

S

=

Dst

f

l

hh

f

ii

up

l

S

=

Dst

f

l

hh

f

ii

X

∃P ∈

S

:

X

up

P

=

Dst

f

l

h

f

i

X

∃P ∈

S

:

X

up

P

w

(because Dst

f

is a separable poset)

Dst

f

l

h

f

iP

P ∈

S

=

Dst

f

l

hh

f

ii

S.

15.4. The order of pointfree funcoids

Definition

1084

.

The order of pointfree funcoids

FCD

(

A

;

B

) is defined by the

formula:

f

v

g

⇔ ∀

x

A

:

h

f

i

x

v h

g

i

x

∧ ∀

y

B

:

f

1

y

v

g

1

y.

Proposition

1085

.

It is really a partial order on the set

FCD

(

A

;

B

).

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

1086

.

It is enough to define 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 different sources or destinations.

Obvious

1087

.

f

v

g

[

f

]

[

g

] for every

f, g

FCD

(

A

;

B

) for every posets

A

and

B

.

Theorem

1088

.

If

A

and

B

are separable posets then

f

v

g

[

f

]

[

g

].

Proof.

From the theorem

1068

.

Theorem

1089

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices. Then for

R

P

FCD

(

A

;

B

) and

X

Z

0

,

Y

Z

1

we have:

1

.

X

[

F

R

]

Y

⇔ ∃

f

R

:

X

[

f

]

Y

;

2

.

h

F

R

i

X

=

n

h

f

i

X

f

R

o

.

Proof.