background image

19.5. DOMAIN AND RANGE OF A POINTFREE FUNCOID

293

Proposition

1537

.

h

f

i

x

=

h

f

i

(

x

u

dom

f

) for every

x

Src

f

for a pointfree

funcoid

f

whose source is a bounded separable meet-semilattice and destination is

a bounded separable poset.

Proof.

Src

f

is strongly separable by theorem

222

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

(by strong separability of 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

1538

.

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

>

.

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).

Proposition

1539

.

dom

f

=

d

n

a

atoms

Src

f

h

f

i

a

6

=

Dst

f

o

for every pointfree funcoid

f

whose destination is a bounded strongly separable poset and source is an atomistic

poset.

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

=

d

n

a

atoms

Src

f

a

6

dom

f

o

=

d

n

a

atoms

Src

f

h

f

i

a

6

=

Dst

f

o

.

Proposition

1540

.

dom(

f

|

a

) =

a

u

dom

f

for every pointfree funcoid

f

and

a

Src

f

where Src

f

is a meet-semilattice and Dst

f

has greatest element.

Proof.

dom(

f

|

a

) = im(id

pFCD

(Src

f

)

a

f

1

) =

D

id

pFCD

(Src

f

)

a

E

f

1

>

Dst

f

=

a

u

f

1

>

Dst

f

=

a

u

dom

f.

Proposition

1541

.

For every composable pointfree funcoids

f

and

g

1

. If im

f

w

dom

g

then im(

g

f

) = im

g

, provided that the posets Src

f

,

Dst

f

= Src

g

and Dst

g

have greatest elements and Src

g

and Dst

g

are

strongly separable.

2

. If im

f

v

dom

g

then dom(

g

f

) = dom

g

, provided that the posets Dst

g

,

Dst

f

= Src

g

and Src

f

have greatest elements and Dst

f

and Src

f

are

strongly separable.

Proof.

1

im(

g

f

) =

h

g

f

i>

Src

f

=

h

g

ih

f

i>

Src

f

v

im

g

by strong separability of

Dst

g

; im(

g

f

) =

h

g

f

i>

Src

f

=

h

g

i

im

f

w h

g

i

dom

g

= im

g

by strong separability

of Dst

g

and proposition

1536

.

2

dom(

g

f

) = im(

f

1

g

1

) what by the proved is equal to im

f

1

that is

dom

f

.