17.9. ON PRODUCTS OF STAROIDS

249

Proof.

GR

Strd

(

A

)

Y

A

=

GR

Strd

(

A

)

Y

A

=

L

Q

A

i

dom

A

:

A

i

6

L

i

=

L

Q

A

i

dom

A

:

A

i

6

L

i

Z

=

L

Q

Z

i

dom

A

:

A

i

6

L

i

=

GR

Strd

(

Z

)

Y

A.

Corollary

1303

.

If each (

F

i

;

P

i

) is a powerset filtrator and

A

Q

P

, then

Q

Strd

(

F

)

A

is a principal staroid.

Proof.

Use the “obvious” fact above.

Theorem

1304

.

Let

F

be a family of sets of filters on distributive lattices with

least elements. Let

a

Q

F

,

S

P

Q

F

, and every Pr

i

S

be a generalized filter

base,

d

S

=

a

. Then

Strd

(

F

)

Y

a

=

l

(

Q

Strd

(

F

)

A

A

S

)

.

Proof.

That

Q

Strd

(

F

)

a

is a lower bound for

Q

Strd

(

F

)

A

A

S

is obvious.

Let

f

be a lower bound for

Q

Strd

(

F

)

A

A

S

. Thus

A

S

: GR

f

GR

Q

Strd

(

F

)

A

.

Thus for every

A

S

we have

L

GR

f

implies

i

dom

A

:

A

i

6

L

i

. Then, by

properties of generalized filter bases,

i

dom

A

:

a

i

6

L

i

that is

L

GR

Q

Strd

(

F

)

a

.

So

f

v

Q

Strd

(

F

)

a

.

Conjecture

1305

.

Let

F

be a family of sets of filters on distributive lattices

with least elements. Let

a

Q

F

,

S

P

Q

F

be a generalized filter base,

d

S

=

a

,

f

is a staroid of the form

Q

F

. Then

Strd

(

F

)

Y

a

6

f

⇔ ∀

A

S

:

Strd

(

A

)

Y

A

6

f.

17.9. On products of staroids

Definition

1306

.

Q

(

D

)

F

=

uncurry

z

z

Q

F

(

reindexation product

) for every in-

dexed family

F

of relations.

Definition

1307

.

Reindexation product

of an indexed family

F

of anchored

relations is defined by the formulas:

form

(

D

)

Y

F

= uncurry(form

F

) and GR

(

D

)

Y

F

=

(

D

)

Y

(GR

F

)

.

Obvious

1308

.