6.6. DOMAIN AND RANGE OF A FUNCOID

109

1

. im

FCD

(

A

;

B

)

f

=

B

im

f

;

2

. dom

FCD

(

A

;

B

)

f

=

A

dom

f

.

Proposition

623

.

h

f

iX

=

h

f

i

(

X u

dom

f

) for every funcoid

f

,

X ∈

F

(Src

f

).

Proof.

For every

Y ∈

F

(Dst

f

) we have

Y u h

f

i

(

X u

dom

f

)

6

=

F

(Dst

f

)

X u

dom

f

u

f

1

Y 6

=

F

(Src

f

)

X u

im

f

1

u

f

1

Y 6

=

F

(Src

f

)

X u

f

1

Y 6

=

F

(Src

f

)

Y u h

f

iX 6

=

F

(Dst

f

)

.

Thus

h

f

i

(

X u

dom

f

) =

h

f

iX

because the lattice of filters is separable.

Proposition

624

.

h

f

iX

= im(

f

|

X

) for every funcoid

f

,

X ∈

F

(Src

f

).

Proof.

im(

f

|

X

) =

D

f

id

FCD

X

E

>

F

(Src

f

)

=

h

f

i

D

id

FCD

X

E

>

F

(Src

f

)

=

h

f

i

(

X u >

F

(Src

f

)

) =

h

f

iX

.

Proposition

625

.

X u

dom

f

6

=

F

(Src

f

)

⇔ h

f

iX 6

=

F

(Dst

f

)

for every funcoid

f

and

X ∈

F

(Src

f

).

Proof.

X u

dom

f

6

=

F

(Src

f

)

X u

f

1

>

F

(Dst

f

)

6

=

F

(Src

f

)

>

F

(Dst

f

)

u h

f

iX 6

=

F

(Dst

f

)

h

f

iX 6

=

F

(Dst

f

)

.

Corollary

626

.

dom

f

=

F

n

a

atoms

F

(Src

f

)

h

f

i

a

6

=

F

(Dst

f

)

o

.

Proof.

This follows from the fact that

F

(Src

f

) is an atomistic lattice.

Proposition

627

.

dom(

f

|

A

) =

A u

dom

f

for every funcoid

f

and

A ∈

F

(Src

f

).

Proof.

dom(

f

|

A

) =

im(id

FCD

A

f

1

) =

D

id

FCD

A

E

f

1

>

F

(Dst

f

)

=

A u

f

1

>

F

(Dst

f

)

=

A u

dom

f.