background image

15.7. SPECIFYING FUNCOIDS BY FUNCTIONS OR RELATIONS ON ATOMIC FILTERS211

Let’s prove the reverse of (

18

):

l

DG

◦h

α

i

atoms

A

E

up

(

A

;

Z

0

)

a

=

l

DG

◦h

α

i

E

atoms

A

up

(

A

;

Z

0

)

a

v

l

DG

◦h

α

i

E

atoms

A

{{

a

}}

=

l

nG

◦h

α

i

{

a

}

o

=

l

nG

h

α

i

{

a

}

o

=

l

nG

{

αa

}

o

=

l

{

αa

}

=

αa.

Finally,

αa

=

l

DG

◦h

α

i

atoms

A

E

up

(

A

;

Z

0

)

a

=

l

h

α

0

i

up

(

A

;

Z

0

)

a

=

h

f

i

a,

so

h

f

i

is a continuation of

α

.

2

Consider the relation

δ

0

P

(

Z

0

×

Z

1

) defined by the formula (for every

X

Z

0

,

Y

Z

1

)

X δ

0

Y

⇔ ∃

x

atoms

A

X, y

atoms

B

Y

:

x δ y.

Obviously

¬

(

X δ

0

Z

1

) and

¬

(

Z

0

δ

0

Y

).

I

t

J δ

0

Y

x

atoms

A

(

I

t

J

)

, y

atoms

B

Y

:

x δ y

x

atoms

A

I

atoms

A

J, y

atoms

B

Y

:

x δ y

x

atoms

A

I, y

atoms

B

Y

:

x δ y

∨ ∃

x

atoms

A

J, y

atoms

B

Y

:

x δ y

I δ

0

Y

J δ

0

Y

;

similarly

X δ

0

I

t

J

X δ

0

I

X δ

0

J

. Let’s continue

δ

0

till a funcoid

f

(by the

theorem

1082

):

X

[

f

]

Y ⇔ ∀

X

up

(

A

;

Z

0

)

X

, Y

up

(

B

;

Z

1

)

Y

:

X δ

0

Y.

The reverse of (

20

implication is trivial, so

X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

x

atoms

A

X, y

atoms

B

Y

:

x δ y

a δ b.

X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

x

atoms

A

X, y

atoms

B

Y

:

x δ y

X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

:

X δ

0

Y

a

[

f

]

b.

So

a δ b

a

[

f

]

b

, that is [

f

] is a continuation of

δ

.

Theorem

1115

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices. If

R

P

FCD

(

A

;

B

) and

x

atoms

A

,

y

atoms

B

, then

1

.

h

d

R

i

x

=

d

n

h

f

i

x

f

R

o

;

2

.

x

[

d

R

]

y

⇔ ∀

f

R

:

x

[

f

]

y

.

Proof.