Let

f

is a lower bound for

n

Q

Strd

(

F

)

A

|

A

S

o

. Thus for every

A

S

we have

L

GR

f

implies

i

dom

A

:

A

i

L

i

. Then, by properties of generalized filter bases,

i

dom

A

:

a

i

L

i

that

is

L

GR

Q

Strd

(

F

)

a

.

So

f

Q

Strd

(

F

)

a

.

Theorem 98.

Let

F

is a family of sets of filters on distributive lattices with least elements. Let

a

Q

F

,

S

P

Q

F

is a generalized filter base,

d

S

=

a

,

f

is a staroid of the form

Q

F

. Then

Y

Strd

(

F

)

a

f

⇔ ∀

A

S

:

Y

Strd

(

A

)

A

f .

Proof.

It follows from the previous theorem by properties of generalized filter bases.

9.1 On products of staroids

Definition 99.

Q

(

D

)

F

=

{

uncurry

z

|

z

Q

F

}

(

reindexation product

) for every indexed family

F

of relations.

Definition 100.

Reindexation product

of an indexed family

F

of anchored relations is defined by

the formulas:

form

Y

(

D

)

F

=

uncurry

(

form

F

)

and

GR

Y

(

D

)

F

=

Y

(

D

)

(

GR

F

)

.

Obvious 101.

1. form

Q

(

D

)

F

=

{

((

i

;

j

); (

form

F

i

)

j

)

|

i

dom

F , j

arity

F

i

}

;

2. GR

Q

(

D

)

F

=

{{

((

i

;

j

); (

zi

)

j

)

|

i

dom

F , j

arity

F

i

} |

z

Q

(

GR

F

)

}

.

Proposition 102.

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

{

uncurry

z

|

z

Q

(

GR

F

)

} ∈

P

Q

{

((

i

;

j

); (

form

F

i

)

j

)

|

i

dom

F , j

arity

F

i

}

;

{

uncurry

z

|

z

Q

(

GR

F

)

} ⊆

Q

{

((

i

;

j

); (

form

F

i

)

j

)

|

i

dom

F , j

arity

F

i

}

{{

((

i

;

j

); (

zi

)

j

)

|

i

dom

F , j

arity

F

i

} |

z

Q

(

GR

F

)

} ⊆

Q

{

((

i

;

j

); (

form

F

i

)

j

)

|

i

dom

F ,

j

arity

F

i

}

;

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

.

Remark 103.

I suspect that the above proof can be simplified.

Obvious 104.

arity

Q

(

D

)

F

=

`

i

dom

F

arity

F

i

=

{

(

i

;

j

)

|

i

dom

F , j

arity

F

i

}

.

Definition 105.

f

×

(

D

)

g

=

Q

(

D

)

J

f

;

g

K

.

Lemma 106.

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

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

)

a

(

i

;

j

)

. Thus

(

curry

b

)

i

zi

; curry

b

Q

F

because every

F

i

is an upper set and so

b

Q

(

D

)

F

.

Proposition 107.

Let

F

is an indexed family of anchored relations and every

(

form

F

)

i

is a join-

semilattice.

1.

Q

(

D

)

F

is a pre-staroid if every

F

i

is a pre-staroid.

Infinite product of elements and filters

13