background image

15.7. SPECIFYING FUNCOIDS BY FUNCTIONS OR RELATIONS ON ATOMIC FILTERS210

Proof.

Apply the theorem twice.

Corollary

1113

.

If

A

is a separable atomic poset and

B

is a separable poset

then

f

FCD

(

A

;

B

) is determined by the values of

h

f

i

X

for

X

atoms

A

.

Proof.

y

6 h

f

i

x

x

6

f

1

y

⇔ ∃

X

atoms

x

:

X

6

f

1

y

⇔ ∃

X

atoms

x

:

y

6 h

f

i

X.

Thus by separability of

B

we have

h

f

i

is determined by

h

f

i

X

for

X

atoms

x

.

By separability of

A

we infer that

f

can be restored from

h

f

i

(theorem

1068

).

Theorem

1114

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices.

1

. A function

α

B

atoms

A

such that (for every

a

atoms

A

)

αa

v

l

DG

◦h

α

i

atoms

A

E

up

(

A

;

Z

0

)

a

(18)

can be continued to the function

h

f

i

for a unique

f

FCD

(

A

;

B

);

h

f

iX

=

G

h

α

i

atoms

A

X

(19)

for every

X ∈

A

.

2

. A relation

δ

P

(atoms

A

×

atoms

B

) such that (for every

a

atoms

A

,

b

atoms

B

)

X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

x

atoms

A

X, y

atoms

B

Y

:

x δ y

a δ b

(20)

can be continued to the relation [

f

] for a unique

f

FCD

(

A

;

B

);

X

[

f

]

Y ⇔ ∃

x

atoms

X

, y

atoms

Y

:

x δ y

(21)

for every

X ∈

A

,

Y ∈

B

.

Proof.

Existence of no more than one such funcoids and formulas (

19

and

(

21

follow from the theorem

632

and corollary

1080

and the fact that our filtrators

are with separable core.

1

Consider the function

α

0

B

Z

0

defined by the formula (for every

X

Z

0

)

α

0

X

=

G

h

α

i

atoms

A

X.

Obviously

α

0

0

Z

0

= 0

B

. For every

I, J

Z

0

α

0

(

I

t

J

) =

G

h

α

i

atoms

A

(

I

t

J

) =

G

h

α

i

(atoms

A

I

atoms

A

J

) =

G

(

h

α

i

atoms

A

I

∪ h

α

i

atoms

A

J

) =

G

h

α

i

atoms

A

I

t

G

h

α

i

atoms

A

J

=

α

0

I

t

α

0

J.

Let continue

α

0

till a pointfree funcoid

f

(by the theorem

1082

):

h

f

iX

=

d

h

α

0

i

up

(

A

;

Z

0

)

X

.