 16.6. SOME ADDITIONAL PROPERTIES

265

Proof.

For every filter

X

F

(Src

f

) we have

h

(

FCD

)(

RLD

)

in

f

iX

=

d

F

F

up(

RLD

)

in

f

h

F

iX

=

d

F

F

up

Γ(Src

f,

Dst

f

)

f

h

F

iX

.

Obviously

d

F

F

up

Γ(Src

f,

Dst

f

)

f

h

F

iX w h

f

iX

. So (

FCD

)(

RLD

)

in

f

w

f

.

Let

Y

up

h

f

iX

. Then (proposition above) there exists

A

up

X

such that

Y

up

h

f

i

A

.

Thus

A

×

Y

t

A

×> ∈

up

f

. So

h

(

FCD

)(

RLD

)

in

f

iX

=

d

F

F

up

Γ(Src

f,

Dst

f

)

f

h

F

iX v

A

×

Y

t

A

× >

X

=

Y

.

So

Y

up

h

(

FCD

)(

RLD

)

in

f

iX

that is

h

f

iX

w

h

(

FCD

)(

RLD

)

in

f

iX

that is

f

w

(

FCD

)(

RLD

)

in

f

.

16.6. Some additional properties

Proposition

1397

.

For every funcoid

f

FCD

(

A, B

) (for sets

A

,

B

):

1

. dom

f

=

d

F

(

A

)

h

dom

i

up

Γ(

A,B

)

f

;

2

. im

f

=

d

F

(

B

)

h

im

i

up

Γ(

A,B

)

f

.

Proof.

Take

n

X

×

Y

X

P

A,Y

P

B,X

×

Y

f

o

up

Γ(

A,B

)

f

. I leave the rest reasoning

as an exercise.

Theorem

1398

.

For every reloid

f

and

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

):

1

.

X

[(

FCD

)

f

]

Y ⇔ ∀

F

up

Γ(Src

f,

Dst

f

)

f

:

X

[

F

]

Y

;

2

.

h

(

FCD

)

f

iX

=

d

F

F

up

Γ(Src

f,

Dst

f

)

f

h

F

iX

.

Proof.

1

.

F

up

Γ(Src

f,

Dst

f

)

f

:

X

[

F

]

Y ⇔

F

up

Γ(Src

f,

Dst

f

)

f

: (

X ×

FCD

Y

)

u

F

6

=

⊥ ⇔

(*)

(

X ×

FCD

Y

)

u

FCD

l

up

Γ(Src

f,

Dst

f

)

f

6

=

⊥ ⇔

X

"

FCD

l

up

Γ(Src

f,

Dst

f

)

f

#

Y ⇔ X

[(

FCD

)

f

]

Y

.

(*) by properties of generalized filter bases, taking into account that funcoids

are isomorphic to filters.

2

.

d

F

F

up

Γ(Src

f,

Dst

f

)

f

h

F

i

a

=

D

d

FCD

up

Γ(Src

f,

Dst

f

)

f

E

a

=

h

(

FCD

)

f

i

a

for every

ultrafilter

a

.

It remains to prove that the function

ϕ

=

λ

X ∈

F

(Src

f

) :

F

l

F

up

Γ(Src

f,

Dst

f

)

f

h

F

iX

is a component of a funcoid (from what follows that

ϕ

=

h

(

FCD

)

f

i

). To prove this,

it’s enough to show that it preserves finite joins and filtered meets.