background image

15.5. DOMAIN AND RANGE OF A POINTFREE FUNCOID

207

So

h

= (

A

;

B

;

α

;

β

) is a pointfree funcoid. Obviously

h

w

f

and

h

w

g

. If

p

w

f

and

p

w

g

for some

p

FCD

(

A

;

B

) then

h

p

i

x

w h

f

i

x

t h

g

i

x

=

h

h

i

x

and

p

1

y

w

f

1

y

t

g

1

y

=

h

1

y

that is

p

w

h

. So

f

t

g

=

h

.

2

.

x

[

f

t

g

]

y

y

6 h

f

t

g

i

x

y

6 h

f

i

x

t h

g

i

x

y

6 h

f

i

x

y

6 h

g

i

x

x

[

f

]

y

x

[

g

]

y

for every

x

A

,

y

B

.

Theorem

1092

.

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

6w h

f

i

y

.

Then by separability of

B

there exist

z

6 h

f

i

y

such that

z

 h

f

i

x

.

Thus

f

1

z

x

and

f

1

z

6

y

what is impossible for

x

w

y

.

Corollary

1093

.

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

Definition

1094

.

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.

Definition

1095

.

Let

a

A

. The

restricted identity pointfree funcoid

id

FCD

(

A

)

a

= (

A

;

A

;

a

u

A

;

a

u

A

).

Proposition

1096

.

The restricted pointfree funcoid is a pointfree funcoid.

Proof.

We need to prove that (

a

u

A

x

)

6

A

y

(

a

u

A

y

)

6

A

x

what is

obvious.

Obvious

1097

.

(id

FCD

(

A

)

a

)

1

= id

FCD

(

A

)

a

.

Obvious

1098

.

x

h

id

FCD

(

A

)

a

i

y

a

6

A

x

u

A

y

for every

x, y

A

.

Definition

1099

.

I will define

restricting

of a pointfree funcoid

f

to an element

a

Src

f

by the formula

f

|

a

def

=

f

id

FCD

(Src

f

)

a

.

Definition

1100

.

Image

of

f

will be defined by the formula im

f

=

F

hh

f

ii

Src

f

.

Obvious

1101

.

im

f

w

f x

for every

x

Src

f

whenever im

f

is defined.

Proposition

1102

.

im

f

=

h

f

i>

if Src

f

has greatest element

>

and Dst

f

is

a separable poset.

Proof.

h

f

i>

is greater than every

h

f

i

x

(where

x

Src

f

) by proposition

1070

and thus

h

f

i>

= max

hh

f

ii

Src

f

= im

f.