background image

19.1. DEFINITION

284

1

. If

A

is separable, for given value of

h

f

i

there exists no more than one

f

pFCD

(

A

,

B

).

2

. If

A

and

B

are separable, for given value of [

f

] there exists no more than

one

f

pFCD

(

A

,

B

).

Proof.

Let

f, g

pFCD

(

A

,

B

).

1

Let

h

f

i

=

h

g

i

. Then for every

x

A

,

y

B

we have

x

6

f

1

y

y

6 h

f

i

x

y

6 h

g

i

x

x

6

g

1

y

and thus by separability of

A

we have

f

1

y

=

g

1

y

that is

f

1

=

g

1

and

so

f

=

g

.

2

Let [

f

]=[

g

]. Then for every

x

A

,

y

B

we have

x

6

f

1

y

x

[

f

]

y

x

[

g

]

y

x

6

g

1

y

and thus by separability of

A

we have

f

1

y

=

g

1

y

that is

f

1

=

g

1

.

Similarly we have

h

f

i

=

h

g

i

. Thus

f

=

g

.

Proposition

1496

.

If Src

f

and Dst

f

have least elements, then

h

f

i⊥

Src

f

=

Dst

f

for every pointfree funcoid

f

.

Proof.

y

6 h

f

i⊥

Src

f

⇔ ⊥

Src

f

6

f

1

y

0 for every

y

Dst

f

. Thus

h

f

i⊥

Src

f

 h

f

i⊥

Src

f

. So

h

f

i⊥

Src

f

=

Dst

f

.

Proposition

1497

.

If Dst

f

is strongly separable then

h

f

i

is a monotone func-

tion (for a pointfree funcoid

f

).

Proof.

a

v

b

x

Dst

f

: (

a

6

f

1

x

b

6

f

1

x

)

x

Dst

f

: (

x

6 h

f

i

a

x

6 h

f

i

b

)

?

h

f

i

a

?

h

f

i

b

h

f

i

a

v h

f

i

b.

Theorem

1498

.

Let

f

be a pointfree funcoid from a starrish join-semilattice

Src

f

to a separable starrish join-semilattice Dst

f

. Then

h

f

i

(

i

t

j

) =

h

f

i

i

t h

f

i

j

for every

i, j

Src

f

.

Proof.

?

h

f

i

(

i

t

j

) =

y

Dst

f

y

6 h

f

i

(

i

t

j

)

=

y

Dst

f

i

t

j

6 h

f

1

i

y

=

y

Dst

f

i

6 h

f

1

i

y

j

6 h

f

1

i

y

=

y

Dst

f

y

6 h

f

i

i

y

6 h

f

i

j

=

y

Dst

f

y

6 h

f

i

i

t h

f

i

j

=

?

(

h

f

i

i

t h

f

i

j

)

.