background image

2.

x

[

f

t

g

]

y

,

y

/

h

f

t

g

i

x

,

y

/

h

f

i

x

t h

g

i

x

,

y

/

h

f

i

x

_

y

/

h

g

i

x

,

x

[

f

]

y

_

x

[

g

]

y

for every

x

2

A

,

y

2

B

.

Theorem 15.36.

Let

f

be a pointfree funcoid from a separable poset

A

to a separable poset

B

.

If

h

f

i

is an injection, then

h

f

i

is an order embedding

A

!

B

.

Proof.

Suppose

x

w

y

but

h

f

i

x

wh

f

i

y

.

Then by separability of

B

there exist

z

/

h

f

i

y

such that

z

 h

f

i

x

.

Thus

h

f

¡

1

i

z

x

and

h

f

¡

1

i

z

/

y

what is impossible for

x

w

y

.

Corollary 15.37.

Let

f

be a pointfree funcoid from a separable poset

A

to a separable poset

B

.

If

h

f

i

is a bijection

A

!

B

, then

h

f

i

is an order isomorphism

A

!

B

.

15.5 Domain and range of a pointfree funcoid

Denition 15.38.

Let

A

be a poset. The

identity pointfree funcoid

id

FCD

(

A

)

= (

A

;

A

;

id

A

;

id

A

)

.

It is trivial that identity funcoid is really a pointfree funcoid.
Let now

A

be a meet-semilattice.

Denition 15.39.

Let

a

2

A

. The

restricted identity pointfree funcoid

id

a

FCD

(

A

)

= (

A

;

A

;

a

u

A

;

a

u

A

)

.

Proposition 15.40.

The restricted pointfree funcoid is a pointfree funcoid.

Proof.

We need to prove that

(

a

u

A

x

)

/

A

y

,

(

a

u

A

y

)

/

A

x

what is obvious.

Obvious 15.41.

id

a

FCD

(

A

)

¡

1

=

id

a

FCD

(

A

)

.

Obvious 15.42.

x

h

id

a

FCD

(

A

)

i

y

,

a

/

A

x

u

A

y

for every

x; y

2

A

.

Denition 15.43.

I will dene

restricting

of a pointfree funcoid

f

to an element

a

2

Src

f

by the

formula

f

j

a

=

def

f

id

a

FCD

(

Src

f

)

.

Denition 15.44.

Image

of

f

will be dened by the formula im

f

=

F

hh

f

ii

Src

f

.

Obvious 15.45.

im

f

w

fx

for every

x

2

Src

f

whenever im

f

is dened.

Proposition 15.46.

im

f

=

h

f

i

1

if Src

f

has greatest element

1

and Dst

f

is a separable poset.

Proof.

h

f

i

1

is greater than every

h

f

i

x

(where

x

2

Src

f

) by proposition

15.14

and thus

h

f

i

1 =

max

hh

f

ii

Src

f

=

im

f :

Denition 15.47.

Domain

of a pointfree funcoid

f

is dened by the formula dom

f

=

im

f

¡

1

.

Proposition 15.48.

h

f

i

dom

f

=

im

f

if

f

is a pointfree funcoid and Src

f

has greatest element

1

and Dst

f

is a separable poset.

Proof.

y

/

h

f

i

dom

f

,

dom

f

/

h

f

¡

1

i

y

, h

f

¡

1

i

1

/

h

f

¡

1

i

y

, h

f

¡

1

i

y

=

/ 0

,

1

/

h

f

¡

1

i

y

,

y

/

h

f

i

1

,

y

/

im

f

for every

y

2

Dst

f

.

So

h

f

i

dom

f

=

im

f

by separability of Dst

f

.

Proposition 15.49.

h

f

i

x

=

h

f

i

(

x

u

dom

f

)

whenever dom

f

is dened, for every

x

2

Src

f

for

a pointfree funcoid

f

whose source is a meet-semilattice with least element and destination is a

separable poset with least element.

15.5 Domain and range of a pointfree funcoid

183