 Proof.

By theorem

4.165

.

Proposition 4.228.

(

P

U

)/

is a boolean lattice.

Proof.

By corollary

4.166

.

Proposition 4.229.

For a lattice

F

of lters on a set and

a; b

2

F

the following expressions are

always equal:

1.

a

n

b

=

d

f

z

2

F

j

a

v

b

t

z

g

(quasidierence of

a

and

b

);

2.

a

#

b

=

F

f

z

2

F

j

z

v

a

^

z

u

b

= 0

g

(second quasidierence of

a

and

b

);

3.

F

(

atoms

a

n

atoms

b

)

.

Proof.

Theorem

4.167

.

Conjecture 4.230.

a

n

b

=

a

#

b

for arbitrary lters

a

,

b

on powersets is not provable in ZF

(without axiom of choice).

4.4.1 Fréchet Filter

The consideration below is about lters on a set

U

, but this can be generalized for lters on complete

atomic boolean algebras due complete atomic boolean algebras are isomorphic to algebras of sets
on some set

U

.

Denition 4.231.

=

f

U

n

X

j

X

is a nite subset of

U

g

is called either

Fréchet lter

or

conite

lter

.

It is trivial that Fréchet lter is a lter.

Proposition 4.232.

Cor

= 0

P

;

T

=

;

.

Proof.

This can be deduced from the formula

8

2

U

9

X

2

:

2

/

X

.

Theorem 4.233.

max

fX 2

F

j

Cor

X

= 0

P

g

=

max

fX 2

F

j

T

X

=

;g

.

Proof.

Due the last proposition, it is enough to show that Cor

X

= 0

P

) X v

for every lter

X

.

Let Cor

X

= 0

P

for some lter

X

. Let

X

2

. We need to prove that

X

2 X

.

X

=

U

n f

0

; :::;

n

g

.

U

n f

i

g 2 X

because otherwise

i

2 "

¡

1

Cor

X

. So

X

2 X

.

Theorem 4.234.

=

F

F

f

x

j

x

is a non-trivial ultralter

g

.

Proof.

It follows from the facts that Cor

x

= 0

P

for every non-trivial ultralter

x

, that

F

is an

atomistic lattice, and the previous theorem.

Theorem 4.235.

Cor is the lower adjoint of

t

F

¡

.

Proof.

Because both Cor and

t

F

¡

are monotone, it is enough (theorem

2.98

to prove (for

every lters

X

and

Y

)

X v

t

F

Cor

X

and Cor

(

t

F

Y

)

v Y

:

Cor

(

t

F

Y

) =

Cor

t

P

Cor

Y

= 0

P

t

P

Cor

Y

=

Cor

Y v Y

.

t

F

Cor

X w

Edg

X t

F

Cor

X

=

X

.

Corollary 4.236.

Cor

X

=

X n

for every lter on a set.

Proof.

By theorem

2.115

.

Corollary 4.237.

Cor

F

F

S

=

F

F

h

Cor

i

S

for any set

S

of lters on a powerset.

4.4 Filters on a Set

81