 Corollary 17.106.

If each

(

F

i

;

P

i

)

is a powerset ltrator and

A

2

Q

P

, then

Q

Strd

(

F

)

A

is a

principal staroid.

Proof.

Use the obvious fact above.

Theorem 17.107.

Let

F

be a family of sets of lters on distributive lattices with least elements.

Let

a

2

Q

F

,

S

2

P

Q

F

, and every Pr

i

S

be a generalized lter base,

d

S

=

a

. Then

Y

Strd

(

F

)

a

=

l

(

Y

Strd

(

F

)

A

j

A

2

S

)

:

Proof.

That

Q

Strd

(

F

)

a

is a lower bound for

nQ

Strd

(

F

)

A

j

A

2

S

o

is obvious.

Let

f

be a lower bound for

nQ

Strd

(

F

)

A

j

A

2

S

o

. Thus

8

A

2

S

:

GR

f

GR

Q

Strd

(

F

)

A

. Thus

for every

A

2

S

we have

L

2

GR

f

implies

8

i

2

dom

A

:

A

i

/

L

i

. Then, by properties of generalized

lter bases,

8

i

2

dom

A

:

a

i

/

L

i

that is

L

2

GR

Q

Strd

(

F

)

a

.

So

f

v

Q

Strd

(

F

)

a

.

Conjecture 17.108.

Let

F

be a family of sets of lters on distributive lattices with least elements.

Let

a

2

Q

F

,

S

2

P

Q

F

be a generalized lter base,

d

S

=

a

,

f

is a staroid of the form

Q

F

. Then

Y

Strd

(

F

)

a

/

f

, 8

A

2

S

:

Y

Strd

(

A

)

A

/

f :

17.9 On products of staroids

Denition 17.109.

Q

(

D

)

F

=

f

uncurry

z

j

z

2

Q

F

g

(

reindexation product

) for every indexed

family

F

of relations.

Denition 17.110.

Reindexation product

of an indexed family

F

of anchored relations is dened

by the formulas:

form

Y

(

D

)

F

=

uncurry

(

form

F

)

and GR

Y

(

D

)

F

=

Y

(

D

)

(

GR

F

)

:

Obvious 17.111.

1. form

Q

(

D

)

F

=

f

((

i

;

j

); (

form

F

i

)

j

)

j

i

2

dom

F ; j

2

arity

F

i

g

;

2. GR

Q

(

D

)

F

=

ff

((

i

;

j

); (

zi

)

j

)

j

i

2

dom

F ; j

2

arity

F

i

g j

z

2

Q

(

GR

F

)

g

.

Proposition 17.112.

Q

(

D

)

F

is an anchored relation if every

F

i

is an anchored relation.

Proof.

We need to prove GR

Q

(

D

)

F

2

P

Q

form

¡Q

(

D

)

F

that is

GR

Q

(

D

)

F

Q

form

¡Q

(

D

)

F

;

ff

((

i

;

j

); (

zi

)

j

)

j

i

2

dom

F ; j

2

arity

F

i

g j

z

2

Q

(

GR

F

)

Q

f

((

i

;

j

); (

form

F

i

)

j

)

j

i

2

dom

F ;

j

2

arity

F

i

g

;

8

z

2

Q

(

GR

F

)

; i

2

dom

F ; j

2

arity

F

i

: (

zi

)

j

2

(

form

F

i

)

j

.

Really,

zi

2

GR

F

i

Q

(

form

F

i

)

and thus

(

zi

)

j

2

(

form

F

i

)

j

.

Obvious 17.113.

arity

Q

(

D

)

F

=

`

i

2

dom

F

arity

F

i

=

f

(

i

;

j

)

j

i

2

dom

F ; j

2

arity

F

i

g

.

Denition 17.114.

f

(

D

)

g

=

Q

(

D

)

J

f

;

g

K

.

Lemma 17.115.

Q

(

D

)

F

is an upper set if every

F

i

is an upper set.

216

Multifuncoids and staroids