background image

19.5. DOMAIN AND RANGE OF A POINTFREE FUNCOID

292

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

pFCD

(

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

.

19.5. Domain and range of a pointfree funcoid

Definition

1530

.

Let

A

be a poset. The

identity pointfree funcoid

1

pFCD

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

1531

.

Let

a

A

. The

restricted identity pointfree funcoid

id

pFCD

(

A

)

a

= (

A

,

A

, a

u

A

, a

u

A

).

Proposition

1532

.

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

1533

.

(id

pFCD

(

A

)

a

)

1

= id

pFCD

(

A

)

a

.

Obvious

1534

.

x

h

id

pFCD

(

A

)

a

i

y

a

6

A

x

u

A

y

for every

x, y

A

.

Definition

1535

.

I will define

restricting

of a pointfree funcoid

f

to an element

a

Src

f

by the formula

f

|

a

def

=

f

id

pFCD

(Src

f

)

a

.

Definition

1536

.

Let

f

be a pointfree funcoid whose source is a set with

greatest element.

Image

of

f

will be defined by the formula im

f

=

h

f

i>

.

Proposition

1537

.

im

f

w h

f

i

x

for every

x

Src

f

whenever Dst

f

is a

strongly separable poset with greatest element.

Proof.

h

f

i>

is greater than every

h

f

i

x

(where

x

Src

f

) by proposition

1500

.

Definition

1538

.

Domain

of a pointfree funcoid

f

is defined by the formula

dom

f

= im

f

1

.

Proposition

1539

.

h

f

i

dom

f

= im

f

if

f

is a pointfree funcoid and Src

f

is a

strongly separable poset with greatest element and Dst

f

is a separable poset with

greatest element.

Proof.

For every

y

Dst

f

y

6 h

f

i

dom

f

dom

f

6

f

1

y

f

1

> 6

f

1

y

(by strong separability of Src

f

)

f

1

y

is not least

⇔ > 6

f

1

y

y

6 h

f

i> ⇔

y

6

im

f.

So

h

f

i

dom

f

= im

f

by separability of Dst

f

.