 19.8. FUNCOIDAL PRODUCT OF ELEMENTS

299

Corollary

1558

.

Let

A

,

B

be bounded separable meet-semilattices. For

every

f

pFCD

(

A

,

B

) and

A ∈

A

,

B ∈

B

we have

f

6 A ×

FCD

B ⇔ A

[

f

]

B

.

Proof.

Existence of

f

u

(

A ×

FCD

B

) follows from the above theorem.

f

6 A ×

FCD

B ⇔

f

u

(

A ×

FCD

B

)

6

=

pFCD

(

A

,

B

)

f

u

(

A ×

FCD

B

)

>

A

6

=

B

D

id

pFCD

(

B

)

B

f

id

pFCD

(

A

)

A

E

>

A

6

=

B

D

id

pFCD

(

B

)

B

E

h

f

i

D

id

pFCD

(

A

)

A

E

>

A

6

=

B

B u h

f

i

(

A u >

A

)

6

=

B

B u h

f

iA 6

=

B

A

[

f

]

B

.

Theorem

1559

.

Let

A

,

B

be bounded separable meet-semilattices. Then the

poset

pFCD

(

A

,

B

) is separable.

Proof.

Let

f, g

pFCD

(

A

,

B

) and

f

6

=

g

. By the theorem

1495

[

f

]

6

= [

g

].

That is there exist

x, y

A

such that

x

[

f

]

y

<

x

[

g

]

y

that is

f

u

(

x

×

FCD

y

)

6

=

pFCD

(

A

,

B

)

<

g

u

(

x

×

FCD

y

)

6

=

pFCD

(

A

,

B

)

. Thus

pFCD

(

A

,

B

) is separable.

Corollary

1560

.

Let

A

,

B

be atomic bounded separable meet-semilattices.

The poset

pFCD

(

A

,

B

) is:

1

. separable;

2

. strongly separable;

3

. atomically separable;

4

. conforming to Wallman’s disjunction property.

Proof.

By the theorem

230

.

Remark

1561

.

For more ways to characterize (atomic) separability of the

lattice of pointfree funcoids see subsections

Separation subsets and full stars

” and

Atomically Separable Lattices

.

Corollary

1562

.

Let (

A

,

Z

0

) and (

B

,

Z

1

) be primary filtrators over boolean

lattices. The poset

pFCD

(

A

,

B

) is an atomistic lattice.

Proof.

By the corollary

1525

pFCD

(

A

,

B

) is a complete lattice. We can use

theorem

228

.

Theorem

1563

.

Let

A

and

B

be posets of filters over boolean lattices. If

S

P

(

A

×

B

) then

l

(

A

,

B

)

S

(

A ×

FCD

B

) =

l

dom

S

×

FCD

l

im

S.

Proof.

If

x

atoms

A

then by the theorem

1547

*

l

(

A

,

B

)

S

(

A ×

FCD

B

)

+

x

=

l

A ×

FCD

B

x

(

A

,

B

)

S

)

.