 5.26. DISTRIBUTIVITY FOR AN ELEMENT OF BOOLEAN CORE

105

2

. (

A

,

Z

) is a complete co-brouwerian atomistic down-aligned lattice filtrator

with binarily meet-closed and separable boolean core.

3

. The three expressions of pseudodifference of

a

and

b

in theorem

247

are

also equal to

d

n

a

u

B

B

up

b

o

.

Proof.

1

2

The filtrator of filters on a boolean lattice is:

complete by corollary

518

;

atomistic by theorem

581

;

co-brouwerian by corollary

531

;

with separable core by theorem

537

;

with binarily meet-closed core by corollary

536

.

2

3

.

d

n

z

F

z

v

a

z

u

b

=

o

v

d

n

a

u

B

B

up

b

o

because

z

z

F

z

v

a

z

u

b

=

z

v

a

z

u

b

=

⊥ ⇔

(separability)

z

v

a

∧ ∃

B

up

b

:

z

u

B

=

⊥ ⇔

(theorem

604

)

z

v

a

∧ ∃

B

up

b

:

z

v

B

B

up

b

:

z

v

a

z

v

B

⇔ ∃

B

up

b

:

z

v

a

u

B

z

v

l

a

u

B

B

up

b

.

But

a

u

B

n

z

F

z

v

a

z

u

b

=

o

because

a

u

B

u

b

=

a

u

B

u

b

v

a

u

B

u

A

B

=

a

u

B

u

Z

B

=

a

u ⊥

=

and thus

a

u

B

v

l

z

F

z

v

a

z

u

b

=

so

d

n

z

F

z

v

a

z

u

b

=

o

w

d

n

a

u

B

B

up

b

o

.

5.26. Distributivity for an Element of Boolean Core

Lemma

609

.

The following is an implications tuple:

1

. (

A

,

Z

) is a powerset filtrator.

2

. (

A

,

Z

) is a primary filtrator over a boolean lattice.

3

. (

A

,

Z

) is an up-aligned binarily join-closed and binarily meet-closed dis-

tributive lattice filtrator over a boolean lattice.

4

.

A

u

A

is a lower adjoint of

A

t

A

for every

A

Z

.

Proof.

1

2

Obvious.

2

3

It is binarily join closed by theorem

534

It is binarily meet-closed by

corollary

536

It is distributive by corollary

531

.

3

4

We will use the theorem

126

.

That

A

u

A

and

A

t

A

are monotone is obvious.

We need to prove (for every

x, y

A

) that

x

v

A

t

A

(

A

u

A

x

) and

A

u

A

(

A

t

A

y

)

v

y.

Really,

A

t

A

(

A

u

A

x

) = (

A

t

A

A

)

u

A

(

A

t

A

x

) =

(

A

t

Z

A

)

u

A

(

A

t

A

x

) =

> u

A

(

A

t

A

x

) =

A

t

A

x

w

x