background image

17.2. FUNCTION SPACES OF POSETS

236

Proof.

We will prove only the first as the second is dual.

up

a

=

c

Q

Z

c

w

a

=

c

Q

Z

i

dom

a

:

c

i

w

a

i

=

c

Q

Z

i

dom

a

:

c

i

up

a

i

=

Y

i

dom

a

up

a

i

.

Proposition

1227

.

If every (

A

i

;

Z

i

) is a filtered complete lattice filtrator, then

(

Q

A

;

Q

Z

) is a filtered complete lattice filtrator.

Proof.

That

Q

A

is a complete lattice is already proved above. We have for

every

a

Q

A

Q

A

l

up

a

=

λi

dom

A

:

l

x

i

x

up

a

=

λi

dom

A

:

l

x

x

up

a

i

=

λi

dom

A

:

l

up

a

i

=

λi

dom

A

:

a

i

=

a.

Proposition

1228

.

If every (

A

i

n

;

Z

i

n

) is a prefiltered complete lattice filtra-

tor with up

x

6

=

for every

x

A

i

(for every

i

n

), then (

Q

A

;

Q

Z

) is a prefiltered

complete lattice filtrator.

Proof.

Let

a, b

Q

A

and

a

6

=

b

. Then there exists

i

n

such that

a

i

6

=

b

i

and so up

a

i

6

= up

b

i

. Consequently

Q

i

dom

a

up

a

i

6

=

Q

i

dom

a

up

b

i

(taken into

account that up

x

6

=

for every

x

A

i

) that is up

a

6

= up

b

.

Proposition

1229

.

Let every (

A

i

n

;

Z

i

n

) be a semifiltered filtrator with

up

x

6

=

for every

x

A

i

(for every

i

n

). Then (

Q

A

;

Q

Z

) is a semifiltered

filtrator.

FiXme

: Semifiltered is the same as filtered, remove one of the two state-

ments (which one? they are not equivalent having different theorem conditions!)

Proof.

Let every (

A

i

;

Z

i

) be a semifiltered filtrator. Let up

a

up

b

for some

a, b

Q

A

. Then

Q

i

dom

a

up

a

i

Q

i

dom

a

up

b

i

and consequently (taking into

account that up

x

6

=

for every

x

A

i

) up

a

i

up

b

i

for every

i

n

. Then

i

n

:

a

i

v

b

i

that is

a

v

b

.

Proposition

1230

.

Let (

A

i

;

Z

i

) be filtrators and each

Z

i

be a complete lattice

with up

x

6

=

for every

x

A

i

(for every

i

n

). For

a

Q

A

:

1

. Cor

a

=

λi

dom

a

: Cor

a

i

;

2

. Cor

0

a

=

λi

dom

a

: Cor

0

a

i

.