background image

5.11. CORE PART

87

2

1

It is enough to prove that

a

v

A, B

a

v

A

u

Z

B

for every

A, B

A

.

Really:

a

v

A, B

A, B

up

a

A

u

Z

B

up

a

a

v

A

u

Z

B.

Corollary

533

.

The following is an implications tuple:

1

. (

A

,

Z

) is a powerset filtrator.

2

. (

A

,

Z

) is a primary filtrator over a meet semilattice.

3

. (

A

,

Z

) is with binarily meet-closed core.

Proof.

1

2

Obvious.

2

3

From the theorem.

5.10.1. Separability of Core for Primary Filtrators.

Theorem

534

.

The following is an implications tuple:

1

. (

A

,

Z

) is a powerset filtrator.

2

. (

A

,

Z

) is a primary filtrator over a meet semilattice with least element.

3

. (

A

,

Z

) is with separable core.

Proof.

1

2

Obvious.

2

3

Let

A

B

where

A

,

B ∈

A

.

up(

A u

A

B

) =

[

up(

A

u

Z

B

)

A

up

A

, B

up

B

.

So

⊥ ∈

up(

A u

A

B

)

A

up

A

, B

up

B

:

⊥ ∈

up(

A

u

Z

B

)

A

up

A

, B

up

B

:

A

u

Z

B

=

⊥ ⇔

A

up

A

, B

up

B

:

A

u

A

B

=

A

(used proposition

533

).

5.11. Core Part

Let (

A

,

Z

) be a filtrator.

Definition

535

.

The

core part

of an element

a

A

is Cor

a

=

d

Z

up

a

.

Definition

536

.

The

dual core part

of an element

a

A

is Cor

0

a

=

d

Z

down

a

.

Obvious

537

.

Cor

0

is dual of Cor.

Obvious

538

.

Cor

a

= Cor

0

a

=

a

for every element

a

of the core of a filtrator.

Theorem

539

.

The following is an implications tuple:

1

.

a

is a filter on a set.

2

.

a

is a filter on a complete lattice.

3

.

a

is an element of a filtered filtrator and Cor

a

exists.

4

. Cor

a

v

a

and Cor

a

down

a

.

Proof.