 17.3. DEFINITION OF STAROIDS

238

To prove it is enough to show

a

i

\

b

i

=

d

z

i

z

Q

A

,a

v

b

t

z

that is

a

i

\

b

i

=

d

n

z

A

i

a

i

v

b

i

t

z

o

(for the reverse implication take

z

j

=

a

i

for

j

6

=

i

) what is true by

definition.

Proposition

1235

.

If every

A

i

is a distributive lattice with least element, then

a

#

b

=

λi

dom

A

:

a

i

#

b

i

for every

a, b

Q

A

whenever every

a

i

#

b

i

is defined.

Proof.

We need to prove that

λi

dom

A

:

a

i

#

b

i

=

F

z

Q

A

z

v

a

z

b

.

To prove it is enough to show

a

i

#

b

i

=

F

z

i

z

Q

A

,z

v

a

z

b

that is

a

i

#

b

i

=

F

n

z

A

i

z

v

a

i

∧∀

j

dom

A

:

z

j

b

j

o

that is

a

i

#

b

i

=

F

n

z

A

i

z

v

a

i

z

b

i

o

(take

z

j

=

for

j

6

=

i

)

what is true by definition.

Proposition

1236

.

Let every

A

i

be a poset with least element and

a

i

is

defined. Then

a

=

λi

dom

A

:

a

i

.

Proof.

We need to prove that

λi

dom

A

:

a

i

=

F

c

A

c

a

. To prove this it is

enough to show that

a

i

=

F

c

i

c

Q

A

,c

a

that is

a

i

=

F

c

i

c

Q

A

,

j

dom

A

:

c

j

a

j

that is

a

i

=

F

c

i

c

Q

A

,c

i

a

i

(take

c

j

= 0 for

j

6

=

i

) that is

a

i

=

F

n

c

A

i

c

a

i

o

what

is true by definition.

Corollary

1237

.

Let every

A

i

be a poset with greatest element and

a

+

i

is

defined. Then

a

+

=

λi

dom

A

:

a

+

i

.

Proof.

By duality.

17.3. Definition of staroids

Let

n

be a set. As an example,

n

may be an ordinal,

n

may be a natural

number, considered as a set by the formula

n

=

{

0

, . . . , n

1

}

. Let

A

=

A

i

n

be a

family of posets indexed by the set

n

.

Definition

1238

.

I will call an

anchored relation

a pair

f

= (form

f

; GR

f

)

of a family form(

f

) of sets indexed by the some index set and a relation GR(

f

)

P

Q

form(

f

). I call GR(

f

) the

graph

of the anchored relation

f

. I denote Anch(

A

)

the set of anchored relations of the form

A

.

Definition

1239

.

An anchored relation

on powersets

is an anchored relation

f

such that every (form

f

)

i

is a powerset.

I will denote arity

f

= dom form

f

.

Definition

1240

.

Every set of anchored relations of the same form constitutes

a poset by the formula

f

v

g

GR

f

GR

g

.

Definition

1241

.

An anchored relation is an

anchored relation between posets

when every (form

f

)

i

is a poset.

Definition

1242

.

Let

f

be an anchored relation. For every

i

arity

f

and

L

Q

((form

f

)

|

(arity

f

)

\{

i

}

)

(val

f

)

i

L

=

X

(form

f

)

i

L

∪ {

(

i

;

X

}

)

GR

f

(“val” is an abbreviation of the word “value”.)