7.7. DOMAIN AND RANGE OF A FUNCOID

158

Proof.

For every

Y ∈

F

(Dst

f

) we have

Y u h

f

i

(

X u

dom

f

)

6

=

⊥ ⇔

X u

dom

f

u

f

1

Y 6

=

⊥ ⇔

X u

im

f

1

u

f

1

Y 6

=

⊥ ⇔

X u

f

1

Y 6

=

⊥ ⇔

Y u h

f

iX 6

=

.

Thus

h

f

i

(

X u

dom

f

) =

h

f

iX

because the lattice of filters is separable.

Proposition

865

.

h

f

iX

= im(

f

|

X

) for every funcoid

f

,

X ∈

F

(Src

f

).

Proof.

im(

f

|

X

) =

D

f

id

FCD

X

E

>

=

h

f

i

D

id

FCD

X

E

>

=

h

f

i

(

X u >

) =

h

f

iX

.

Proposition

866

.

X u

dom

f

6

=

⊥ ⇔ h

f

iX 6

=

for every funcoid

f

and

X ∈

F

(Src

f

).

Proof.

X u

dom

f

6

=

⊥ ⇔

X u

f

1

>

F

(Dst

f

)

6

=

⊥ ⇔

> u h

f

iX 6

=

⊥ ⇔

h

f

iX 6

=

.

Corollary

867

.

dom

f

=

d

n

a

atoms

F

(Src

f

)

h

f

i

a

6

=

o

.

Proof.

This follows from the fact that

F

(Src

f

) is an atomistic lattice.

Proposition

868

.

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

>

=

A u

f

1

>

=

A u

dom

f.

Theorem

869

.

im

f

=

d

F

h

im

i

up

f

and dom

f

=

d

F

h

dom

i

up

f

for every

funcoid

f

.