background image

15.1. DEFINITION

200

Obvious

1066

.

x

[

f

]

y

y

6 h

f

i

x

x

6

f

1

y

for every pointfree funcoid

f

and

x

Src

f

,

y

Dst

f

.

Obvious

1067

.

f

1

=[

f

]

1

for every pointfree funcoid

f

.

Theorem

1068

.

Let

A

and

B

be posets. Then:

1

. If

A

is separable, for given value of

h

f

i

there exists no more than one

f

FCD

(

A

;

B

).

2

. If

A

and

B

are separable, for given value of [

f

] there exists no more than

one

f

FCD

(

A

;

B

).

Proof.

Let

f, g

FCD

(

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

B

we have

h

f

i

x

=

h

g

i

x

that is

h

f

i

=

h

g

i

. Similarly we

have

f

1

=

g

1

. Thus

f

=

g

.

Proposition

1069

.

If Src

f

and Dst

f

have least elements, then

h

f

i⊥

Src

f

=

Dst

f

for every pointfree funcoid

f

.

FiXme

: Previously I required separability of

Dst

f

. It turned out to be a superfluous condition. Remove it also in consequences

of this proposition.

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

1070

.

If Dst

f

is a separable meet-semilattice then

h

f

i

is a mono-

tone function (for a pointfree funcoid

f

).

FiXme

: Added condition to be a meet-

semilattice, add it also in all consequences.

FiXme

: Check whether existence of least

element of Dst

f

is required (in theorem

173

).

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

(used theorem

173

and that it is a separable meet-semilattice).

Theorem

1071

.

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

.