 15.3. POINTFREE FUNCOID AS CONTINUATION

203

So

h

f

i

x

=

d

Dst

f

hh

f

ii

up

(Src

f

;

Z

0

)

x

because Dst

f

is separable (obvious

403

and

the fact that

Z

1

is a boolean lattice).

Theorem

1082

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices.

1

. A function

α

B

Z

0

conforming to the formulas (for every

I, J

Z

0

)

α

Z

0

=

B

,

α

(

I

t

J

) =

αI

t

αJ

can be continued to the function

h

f

i

for a unique

f

FCD

(

A

;

B

);

h

f

iX

=

B

l

h

α

i

up

(

A

;

Z

0

)

X

(14)

for every

X ∈

A

.

2

. A relation

δ

P

(

Z

0

×

Z

1

) conforming to the formulas (for every

I, J, K

Z

0

and

I

0

, J

0

, K

0

Z

1

)

¬

(

Z

0

δ I

0

)

,

I

t

J δ K

0

I δ K

0

J δ K

0

,

¬

(

I δ

Z

1

)

,

K δ I

0

t

J

0

K δ I

0

K δ J

0

(15)

can be continued to the relation [

f

] for a unique

f

FCD

(

A

;

B

);

X

[

f

]

Y ⇔ ∀

X

up

(

A

;

Z

0

)

X

, Y

up

(

B

;

Z

1

)

Y

:

X δ Y

(16)

for every

X ∈

A

,

Y ∈

B

.

Proof.

Existence of no more than one such pointfree funcoids and formulas

(

14

and (

16

follow from two previous theorems.

2

.

Y

Z

1

XδY

is obviously a free star for every

X

Z

0

. By properties of filters

on boolean lattices, there exist a unique filter

αX

such that

(

αX

) =

Y

Z

1

XδY

for

every

X

Z

0

. Thus

α

B

Z

0

. Similarly it can be defined

β

A

Z

1

by the formula

(

βY

) =

Y

Z

1

XδY

. Let’s continue the functions

α

and

β

to

α

0

B

A

and

β

0

A

B

by the formulas

α

0

X

=

B

l

h

α

i

up

(

A

;

Z

0

)

X

and

β

0

Y

=

A

l

h

β

i

up

(

B

;

Z

1

)

Y

and

δ

to

δ

0

P

(

A

×

B

) by the formula

X

δ

0

Y ⇔ ∀

X

up

(

A

;

Z

0

)

X

, Y

up

(

B

;

Z

1

)

Y

:

X

δ

Y

.

Y u

α

0

X 6

=

B

⇔ Y u

d

h

α

i

up

(

A

;

Z

0

)

X 6

=

B

d

hYui

h

α

i

up

(

A

;

Z

0

)

X 6

=

B

.

Let’s prove that

W

=

hYui

h

α

i

up

(

A

;

Z

0

)

X

is a generalized filter base: To prove it is enough to show that

h

α

i

up

(

A

;

Z

0

)

X

is a

generalized filter base.

If

A

,

B ∈ h

α

i

up

(

A

;

Z

0

)

X

then exist

X

1

, X

2

up

(

A

;

Z

0

)

X

such that

A

=

αX

1

and

B

=

αX

2

. Then

α

(

X

1

u

Z

0

X

2

)

∈ h

α

i

up

(

A

;

Z

0

)

X

. So

h

α

i

up

(

A

;

Z

0

)

X

is a

generalized filter base and thus

W

is a generalized filter base.

By properties of generalized filter bases,

d

hYui

h

α

i

up

(

A

;

Z

0

)

X 6

=

B

is equiv-

alent to

X

up

(

A

;

Z

0

)

X

:

Y u

αX

6

=

B

,

what is equivalent to

X

up

(

A

;

Z

0

)

X

, Y

up

(

B

;

Z

1

)

Y

:

Y

u

B

αX

6

=

B

X

up

(

A

;

Z

0

)

X

, Y

up

(

B

;

Z

1

)

Y

:

Y

(

αX

)

X

up

(

A

;

Z

0

)

X

, Y

up

(

B

;

Z

1

)

Y

:

X δ Y.