background image

17.9. ON PRODUCTS OF STAROIDS

250

1

. form

Q

(

D

)

F

=

n

((

i

;

j

);(form

F

i

)

j

)

i

dom

F,j

arity

F

i

o

;

2

. GR

Q

(

D

)

F

=

 

((

i

;

j

);(

zi

)

j

)

i

dom

F,j

arity

Fi

 

z

Q

(GR

F

)

.

Proposition

1309

.

Q

(

D

)

F

is an anchored relation if every

F

i

is an anchored

relation.

Proof.

We need to prove GR

Q

(

D

)

F

P

Q

form

Q

(

D

)

F

that is

GR

Q

(

D

)

F

Q

form

Q

(

D

)

F

;

 

((

i

;

j

);(

zi

)

j

)

i

dom

F,j

arity

Fi

 

z

Q

(GR

F

)

Q

n

((

i

;

j

);(form

F

i

)

j

)

i

dom

F,j

arity

F

i

o

;

z

Q

(GR

F

)

, i

dom

F, j

arity

F

i

: (

zi

)

j

(form

F

i

)

j

.

Really,

zi

GR

F

i

Q

(form

F

i

) and thus (

zi

)

j

(form

F

i

)

j

.

Obvious

1310

.

arity

Q

(

D

)

F

=

`

i

dom

F

arity

F

i

=

n

(

i

;

j

)

i

dom

F,j

arity

F

i

o

.

Definition

1311

.

f

×

(

D

)

g

=

Q

(

D

)

J

f

;

g

K

.

Lemma

1312

.

Q

(

D

)

F

is an upper set if every

F

i

is an upper set.

Proof.

We need to prove that

Q

(

D

)

F

is an upper set. Let

a

Q

(

D

)

F

and

an anchored relation

b

w

a

of the same form as

a

. We have

a

= uncurry

z

for some

z

Q

F

that is

a

(

i

;

j

) = (

zi

)

j

for all

i

dom

F

and

j

dom

F

i

where

zi

F

i

.

Also

b

(

i

;

j

)

w

a

(

i

;

j

). Thus (curry

b

)

i

w

zi

; curry

b

Q

F

because every

F

i

is an

upper set and so

b

Q

(

D

)

F

.

Proposition

1313

.

Let

F

be an indexed family of anchored relations and

every (form

F

)

i

is a join-semilattice.

1

.

Q

(

D

)

F

is a prestaroid if every

F

i

is a prestaroid.

2

.

Q

(

D

)

F

is a staroid if every

F

i

is a staroid.

3

.

Q

(

D

)

F

is a completary staroid if every

F

i

is a completary staroid.

Proof.

1

Let

q

arity

Q

(

D

)

F

that is

q

= (

i

;

j

) where

i

dom

F

,

j

arity

F

i

; let

L

Y

form

(

D

)

Y

F

|

arity

Q

(

D

)

F

\{

q

}