background image

15.5. DOMAIN AND RANGE OF A POINTFREE FUNCOID

208

Definition

1103

.

Domain

of a pointfree funcoid

f

is defined by the formula

dom

f

= im

f

1

.

Proposition

1104

.

h

f

i

dom

f

= im

f

if

f

is a pointfree funcoid and Src

f

has

greatest element

>

and Dst

f

is a separable poset.

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

f

1

y

6

=

⊥ ⇔

1

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

.

Proposition

1105

.

h

f

i

x

=

h

f

i

(

x

u

dom

f

) whenever dom

f

is defined, for

every

x

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.

Proof.

For every

y

Dst

f

we have

y

6 h

f

i

(

x

u

dom

f

)

x

u

dom

f

u

f

1

y

6

=

Src

f

x

u

im

f

1

u

f

1

y

6

=

Src

f

x

u

f

1

y

6

=

Src

f

y

6 h

f

i

x.

Thus

h

f

i

x

=

h

f

i

(

x

u

dom

f

) by separability of Dst

f

.

Proposition

1106

.

x

6

dom

f

(

h

f

i

x

is not least) for every pointfree fun-

coid

f

and

x

Src

f

if Dst

f

has greatest element

>

and Src

f

is a separable

poset.

Proof.

x

6

dom

f

x

6

f

1

>

Dst

f

>

Dst

f

6

h

f

i

x

(

h

f

i

x

is not least).

Corollary

1107

.

dom

f

=

F

n

a

atoms

Src

f

h

f

i

a

6

=

Dst

f

o

for every pointfree funcoid

f

whose destination is a bounded poset and source is a separable atomistic meet-

semilattice.

Proof.

For every

a

atoms

Src

f

we have

a

6

dom

f

a

6

f

1

>

Dst

f

⇔ >

Dst

f

6 h

f

i

a

⇔ h

f

i

a

6

=

Dst

f

.

So dom

f

=

F

n

a

atoms

Src

f

a

6

dom

f

o

=

F

n

a

atoms

Src

f

h

f

i

a

6

=

Dst

f

o

.

Proposition

1108

.

dom(

f

|

a

) =

a

u

dom

f

for every pointfree funcoid

f

and

a

Src

f

where Src

f

is a separable meet-semilattice and Dst

f

has greatest element.

Proof.

dom(

f

|

a

) = im(id

FCD

(Src

f

)

a

f

1

) =

D

id

FCD

(Src

f

)

a

E

f

1

>

Dst

f

=

a

u

f

1

>

Dst

f

=

a

u

dom

f.

Proposition

1109

.

For every composable pointfree funcoids

f

and

g

where

the posets Src

f

and Dst

f

= Src

g

have greatest elements and Dst

f

and Dst

g

are

separable:

1

. If im

f

w

dom

g

then im(

g

f

) = im

g

.

2

. If im

f

v

dom

g

then dom(

g

f

) = dom

g

.

Proof.

1

im(

g

f

) =

h

g

f

i>

Src

f

=

h

g

ih

f

i>

Src

f

=

h

g

i

im

f

=

h

g

i

dom

g

=

h

g

i>

Src

g

= im

g

.