background image

Proposition 6.50.

The restricted identity funcoid is a funcoid.

Proof.

We need to prove that

(

A u X

)

u Y

=

/ 0

F

(

A

)

,

(

A u Y

)

u X

=

/ 0

F

(

A

)

what is obvious.

Obvious 6.51.

1.

¡

id

FCD

(

A

)

¡

1

=

id

FCD

(

A

)

;

2.

(

id

A

FCD

)

¡

1

=

id

A

FCD

.

Obvious 6.52.

For every

X

;

Y 2

F

(

A

)

1.

X

id

FCD

(

A

)

Y , X u Y

=

/ 0

F

(

A

)

;

2.

X

[

id

A

FCD

]

Y , A u X u Y

=

/ 0

F

(

A

)

.

Denition 6.53.

I will dene

restricting

of a funcoid

f

to a lter

A 2

F

(

Src

f

)

by the formula

f

j

A

=

f

id

A

FCD

:

Denition 6.54.

Image

of a funcoid

f

will be dened by the formula im

f

=

h

f

i

1

F

(

Src

f

)

.

Domain

of a funcoid

f

is dened by the formula dom

f

=

im

f

¡

1

.

Obvious 6.55.

For every binary relation

f

between sets

A

and

B

1. im

"

FCD

(

A

;

B

)

f

=

"

B

im

f

;

2. dom

"

FCD

(

A

;

B

)

f

=

"

A

dom

f

.

Proposition 6.56.

h

f

iX

=

h

f

i

(

X u

dom

f

)

for every funcoid

f

,

X 2

F

(

Src

f

)

.

Proof.

For every

Y 2

F

(

Dst

f

)

we have

Y u h

f

i

(

X u

dom

f

) =

/ 0

F

(

Dst

f

)

, X u

dom

f

u h

f

¡

1

iY

=

/

0

F

(

Src

f

)

, X u

im

f

¡

1

u h

f

¡

1

iY

=

/ 0

F

(

Src

f

)

, X u h

f

¡

1

iY

=

/ 0

F

(

Src

f

)

, Y u h

f

iX

=

/ 0

F

(

dst

f

)

. Thus

h

f

i

(

X u

dom

f

) =

h

f

iX

because the lattice of lters is separable.

Proposition 6.57.

h

f

iX

=

im

(

f

j

X

)

for every funcoid

f

,

X 2

F

(

Src

f

)

.

Proof.

im

(

f

j

X

) =

h

f

id

X

FCD

i

1

F

(

Src

f

)

=

h

f

ih

id

X

FCD

i

1

F

(

Src

f

)

=

h

f

i

¡

X u

1

F

(

Src

f

)

=

h

f

iX

.

Proposition 6.58.

X u

dom

f

=

/ 0

F

(

Src

f

)

, h

f

iX

=

/ 0

F

(

Dst

f

)

for every funcoid

f

and

X 2

F

(

Src

f

)

.

Proof.

X u

dom

f

=

/ 0

F

(

Src

f

)

, X u h

f

¡

1

i

1

F

(

Dst

f

)

=

/ 0

F

(

Src

f

)

,

1

F

(

Dst

f

)

u h

f

iX

=

/ 0

F

(

Dst

f

)

,

h

f

iX

=

/ 0

F

(

Dst

f

)

.

Corollary 6.59.

dom

f

=

a

2

atoms

F

(

Src

f

)

j h

f

i

a

=

/ 0

F

(

Dst

f

)

 

.

Proof.

This follows from the fact that

F

(

Src

f

)

is an atomistic lattice.

Proposition 6.60.

dom

(

f

j

A

) =

A u

dom

f

for every funcoid

f

and

A 2

F

(

Src

f

)

.

Proof.

dom

(

f

j

A

) =

im

(

id

A

FCD

f

¡

1

) =

h

id

A

FCD

ih

f

¡

1

i

1

F

(

Dst

f

)

=

A u h

f

¡

1

i

1

F

(

Dst

f

)

=

A u

dom

f

.

Theorem 6.61.

im

f

=

d

h

im

i

up

f

and dom

f

=

d

h

dom

i

up

f

for every funcoid

f

.

Proof.

im

f

=

h

f

i

1

F

(

Src

f

)

=

d

h

F

i

1

F

(

Src

f

)

j

F

2

up

f

 

=

d

f

im

F

j

F

2

up

f

g

=

d

h

im

i

up

f

.

The second formula follows from symmetry.

Proposition 6.62.

For every composable funcoids

f

,

g

:

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

f

.

6.6 Domain and range of a funcoid

103