background image

Proof.

Taking into account the previous section, we have:

A t

F

l

F

S

=

A \

l

F

S

=

A \

K

0

u

Z

:::

u

Z

K

n

j

K

i

2

[

S

where

i

= 0

; :::; n

for

n

2

N

 

=

K

0

u

Z

:::

u

Z

K

n

j

K

0

u

Z

:::

u

Z

K

n

2 A

; K

i

2

[

S

where

i

= 0

; :::; n

for

n

2

N

 

=

K

0

u

Z

:::

u

Z

K

n

j

K

i

2 A ^

K

i

2

[

S

where

i

= 0

; :::; n

for

n

2

N

 

=

K

0

u

Z

:::

u

Z

K

n

j

K

i

2 A \

[

S

where

i

= 0

; :::; n

for

n

2

N

 

=

K

0

u

Z

:::

u

Z

K

n

j

K

i

2

[

hA \ i

S

where

i

= 0

; :::; n

for

n

2

N

 

=

K

0

u

Z

:::

u

Z

K

n

j

K

i

2

[

fA \ X j X 2

S

g

where

i

= 0

; :::; n

for

n

2

N

 

=

K

0

u

Z

:::

u

Z

K

n

j

K

i

2

[

fA t

F

X j X 2

S

g

where

i

= 0

; :::; n

for

n

2

N

 

=

l

F

fA t

F

X j X 2

S

g

=

l

F

hA t

F

i

S:

Corollary 4.114.

If

Z

is a distributive lattice with greatest element, then

F

is also a distributive

lattice.

Corollary 4.115.

If

Z

is a distributive lattice with greatest element, then

F

is a co-brouwerian

lattice.

4.3.12 Filters over Boolean Lattices

Theorem 4.116.

If

Z

is a boolean lattice then

a

n

F

B

=

a

u

F

B

for every

a

2

F

,

B

2

P

(where the

complement is taken on

P

).

Proof.

F

is a distributive lattice by corollary

4.114

Our ltrator is nitely meet-closed by the

theorem

4.44

and with join-closed core by the theorem

4.25

It is also up and down aligned.

So we can apply the proposition

4.74

.

4.3.12.1 Distributivity for an Element of Boolean Core

Lemma 4.117.

Let

F

be the poset of lters over a boolean lattice

Z

.

Then

A

u

F

is a lower adjoint of

A

t

F

for every

A

2

P

.

Proof.

Lemma

4.75

.

Theorem 4.118.

Let

F

be the poset of lters over a boolean lattice

Z

. Then

A

u

F

F

F

S

=

F

F

h

A

u

F

i

S

for every

A

2

P

and every set

S

2

P

F

.

Proof.

Direct consequence of the lemma.

4.3.13 Generalized Filter Base

Denition 4.119.

Generalized lter base

is a lter base on the set

F

.

Denition 4.120.

If

S

is a generalized lter base and

A

=

d

F

S

, then we call

S

a generalized

lter base of a lter

A

.

Theorem 4.121.

If

Z

is a distributive lattice

[TODO: Can be generalized for any meet-semilat-

tice?]

and

S

is a generalized lter base of a lter

F

then for any

K

2

Z

K

2 F , 9L 2

S

:

K

2 L

:

4.3 Filters on a poset

67