background image

5.24. SEPARABILITY CRITERIA

103

3

4

We have Cor

0

p

v

p

for every

p

A

because our filtrator is with join-closed

core (theorem

540

).

Obviously Cor

0

d

A

S

v

Cor

0

a

for every

a

S

.

If

x

v

Cor

0

a

for every

a

S

for some

x

Z

then

x

v

a

, thus

x

v

d

A

S

and

x

v

Cor

0

d

A

S

.

So Cor

0

d

A

S

=

d

Z

Cor

0

S

. Cor

0

d

A

T

=

d

Z

T

trivially follows

from this.

Theorem

600

.

The following is an implications tuple:

1

. (

A

,

Z

) is a powerset filtrator.

2

. (

A

,

Z

) is a primary filtrator over a complete atomistic distributive lattice.

3

. (

A

,

Z

) is a filtered down-aligned filtrator with binarily meet-closed core

Z

which is a complete atomistic lattice and

A

is a complete starrish lattice.

4

. Cor

0

(

a

t

A

b

) = Cor

0

a

t

Z

Cor

0

b

for every

a, b

A

.

Proof.

1

2

Obvious.

2

3

(

A

,

Z

) is filtered by theorem

531

It is with binarily meet-close core by

corollary

533

.

A

is starrish by corollary

528

.

A

is complete by corol-

lary

515

.

3

4

From theorem conditions it follows that Cor

0

(

a

t

A

b

) exists.

Cor

0

(

a

t

A

b

) =

d

Z

n

x

x

is an atom of

Z

,x

v

a

t

A

b

o

(used proposition

596

).

By theorem

555

we have

Cor

0

(

a

t

A

b

) =

Z

l

((atoms

A

(

a

t

A

b

))

Z

) =

Z

l

((atoms

A

a

atoms

A

b

)

Z

) =

Z

l

((atoms

A

a

Z

)

(atoms

A

b

Z

)) =

Z

l

(atoms

A

a

Z

)

t

Z

Z

l

(atoms

A

b

Z

)

(used the theorem

493

). Again using theorem

555

we get

Cor

0

(

a

t

A

b

) =

Z

l

x

x

is an atom of

Z

, x

v

a

t

Z

Z

l

x

x

is an atom of

Z

, x

v

b

=

Cor

0

a

t

Z

Cor

0

b

(again used proposition

596

).

See also theorem

167

above.

5.24. Separability criteria

Theorem

601

.

The following is an implications tuple:

1

. (

A

,

Z

) is a powerset filtrator.

2

. (

A

,

Z

) is a primary filtrator over a boolean lattice.