 By properties of generalized lter bases,

d

hY u ih

i

up

(

A

;

Z

0

)

X

=

/ 0

B

is equivalent to

8

X

2

up

(

A

;

Z

0

)

X

:

Y u

X

=

/ 0

B

;

what is equivalent to

8

X

2

up

(

A

;

Z

0

)

X

; Y

2

up

(

B

;

Z

1

)

Y

:

Y

u

B

X

=

/ 0

B

, 8

X

2

up

(

A

;

Z

0

)

X

;

Y

2

up

(

B

;

Z

1

)

Y

:

Y

2

@

(

X

)

, 8

X

2

up

(

A

;

Z

0

)

X

; Y

2

up

(

B

;

Z

1

)

Y

:

X  Y

. Combining the equivalencies

we get

Y u

0

X

=

/ 0

B

,X

0

Y

. Analogously

X u

0

Y

=

/ 0

A

,X

0

Y

. So

Y u

0

X

=

/ 0

B

,X u

0

Y

=

/ 0

A

,

that is

(

A

;

B

;

0

;

0

)

is a pointfree funcoid. From the formula

Y u

0

X

=

/ 0

B

, X

0

Y

it follows that

[(

A

;

B

;

0

;

0

)]

is a continuation of

.

1. Let dene the relation

2

P

(

Z

0

Z

1

)

by the formula

X  Y

,

Y

u

B

X

=

/ 0

B

.

That

:

(0

Z

0

I

0

)

and

:

(

0

Z

1

)

is obvious. We have

K  I

0

t

Z

1

J

0

,

(

I

0

t

Z

1

J

0

)

u

B

K

=

/ 0

B

,

(

I

0

t

B

J

0

)

u

K

=

/ 0

B

,

(

I

0

u

B

K

)

t

(

J

0

u

B

K

) =

/ 0

B

,

I

0

u

B

K

=

/ 0

B

_

J

0

u

B

K

=

/ 0

B

,

K  I

0

_

K  J

0

and

I

t

Z

0

J  K

0

,

K

0

u

B

(

I

t

Z

0

J

) =

/ 0

B

,

K

0

u

B

(

I

t

J

) =

/ 0

B

,

(

K

0

u

B

I

)

t

(

K

0

u

B

J

) =

/ 0

B

,

K

0

u

B

I

=

/ 0

B

_

K

0

u

B

J

=

/ 0

B

,

I  K

0

_

J  K

0

.

That is the formulas (

15.2

are true.

Accordingly the above

can be continued to the relation

[

f

]

for some

f

2

FCD

(

A

;

B

)

.

8

X

2

Z

0

; Y

2

Z

1

: (

Y

u

B

h

f

i

X

=

/ 0

B

,

X

[

f

]

Y

,

Y

u

B

X

=

/ 0

B

)

, consequently

8

X

2

Z

0

:

X

=

h

f

i

X

because our ltrator is with separable core. So

h

f

i

is a continuation of

.

Proposition 15.27.

Let

(

Src

f

;

Z

0

)

be a primary ltrator over a bounded distributive lattice and

(

Dst

f

;

Z

1

)

is a primary ltrator over a boolean lattice. If

S

is a generalized lter base on Src

f

then

h

f

i

d

Src

f

S

=

d

Dst

f

hh

f

ii

S

for every pointfree funcoid

f

.

Proof.

First the meets

d

Src

f

S

and

d

Dst

f

hh

f

ii

S

exist by corollary

4.107

.

(

Src

f

;

Z

0

)

is a nitely meet-closed ltrator by proposition

4.97

and with separable core by

theorem

4.112

thus we can apply theorem

15.25

(up

x

=

/

;

is obvious).

h

f

i

d

Src

f

S

v h

f

i

X

for every

X

2

S

because Dst

f

is separable by obvious

4.136

and thus

h

f

i

d

Src

f

S

v

d

Dst

f

hh

f

ii

S

.

Taking into account properties of generalized lter bases:

h

f

i

l

Src

f

S

=

l

Dst

f

hh

f

ii

up

l

S

=

l

Dst

f

hh

f

iif

X

j 9P 2

S

:

X

2

up

P g

=

l

Dst

f

fh

f

i

X

j 9P 2

S

:

X

2

up

P g w

(because Dst

f

is a separable poset)

l

Dst

f

fh

f

iP j P 2

S

g

=

l

Dst

f

hh

f

ii

S:

15.4 The order of pointfree funcoids

Denition 15.28.

The order of pointfree funcoids

FCD

(

A

;

B

)

is dened by the formula:

f

v

g

, 8

x

2

A

:

h

f

i

x

v h

g

i

x

^ 8

y

2

B

:

h

f

¡

1

i

y

v h

g

¡

1

i

y:

Proposition 15.29.

It is really a partial order on the set

FCD

(

A

;

B

)

.

Proof.

Reexivity.

Obvious.

15.4 The order of pointfree funcoids

181