background image

2. From the lemma.

3. We need to prove

L

0

t

L

1

2

GR

Y

(

D

)

F

, 9

c

2 f

0

;

1

g

arity

Q

(

D

)

F

:

 

i

2

arity

Y

(

D

)

F

:

L

c

(

i

)

i

!

2

GR

Y

(

D

)

F

for every

L

0

; L

1

2

Q

form

Q

(

D

)

F

that is

L

0

; L

1

2

Q

uncurry

(

form

F

)

.

Really

L

0

t

L

1

2

GR

Q

(

D

)

F

,

L

0

t

L

1

2 f

uncurry

z

j

z

2

Q

(

GR

F

)

g

.

9

c

2 f

0

;

1

g

arity

Q

(

D

)

F

:

 i

2

arity

Q

(

D

)

F

:

L

c

(

i

)

i

:

L

c

(

i

)

i

2

GR

Q

(

D

)

F

, 9

c

2 f

0

;

1

g

arity

Q

(

D

)

F

:

 i

2

arity

Q

(

D

)

F

:

L

c

(

i

)

i

2 f

uncurry

z

j

z

2

Q

(

GR

F

)

g , 9

c

2 f

0

;

1

g

arity

Q

(

D

)

F

:

curry

 i

2

arity

Q

(

D

)

F

:

L

c

(

i

)

i

2

Q

(

GR

F

)

, 9

c

2 f

0

;

1

g

arity

Q

(

D

)

F

:

curry

(

i

;

j

)

2

arity

Q

(

D

)

F

:

L

c

(

i

;

j

)

(

i

;

j

)

2

Q

(

GR

F

)

, 9

c

2 f

0

;

1

g

arity

Q

(

D

)

F

:

(

i

2

dom

F

: (

j

2

dom

F

i

:

L

c

(

i

;

j

)

(

i

;

j

)))

2

Q

(

GR

F

)

, 9

c

2 f

0

;

1

g

arity

Q

(

D

)

F

8

i

2

dom

F

:

(

 j

2

dom

F

i

:

L

c

(

i

;

j

)

(

i

;

j

))

2

GR

F

i

, 8

i

2

dom

F

9

c

2 f

0

;

1

g

dom

F

i

: (

 j

2

dom

F

i

:

L

c

(

j

)

(

i

;

j

))

2

GR

F

i

, 8

i

2

dom

F

9

c

2 f

0

;

1

g

dom

F

i

: (

j

2

dom

F

i

: (

curry

(

L

c

(

j

)

)

i

)

j

)

2

GR

F

i

,

8

i

2

dom

F

:

curry

(

L

0

)

i

t

curry

(

L

1

)

i

2

GR

F

i

,

L

0

t

L

1

2 f

uncurry

z

j

z

2

Q

(

GR

F

)

g ,

L

0

t

L

1

2

GR

Q

(

D

)

F

.

For staroids it is dened

ordinated product

Q

(

ord

)

as dened in the section Ordinated product

above.

Obvious 17.117.

If

f

and

g

are anchored relations and there exists a bijection

'

from arity

g

to

arity

f

such that

f

F

'

j

F

2

GR

f

g

=

GR

g

, then:

1.

f

is a prestaroid i

g

is a prestaroid.

2.

f

is a staroid i

g

is a staroid.

3.

f

is a completary staroid i

g

is a completary staroid.

Corollary 17.118.

Let

F

be an indexed family of anchored relations and every

(

form

F

)

i

be a

join-semilattice.

1.

Q

(

ord

)

F

is a prestaroid if every

F

i

is a prestaroid.

2.

Q

(

ord

)

F

is a staroid if every

F

i

is a staroid.

3.

Q

(

ord

)

F

is a completary staroid if every

F

i

is a completary staroid.

Proof.

Use the fact that GR

Q

(

ord

)

F

=

n

F

(

L

(

dom

F

))

¡

1

j

F

2

GR

Q

(

D

)

f

o

.

Denition 17.119.

f

(

ord

)

g

=

Q

(

ord

)

J

f

;

g

K

.

Remark 17.120.

If

f

and

g

are binary funcoids, then

f

(

ord

)

g

is ternary.

Proposition 17.121.

Q

Strd

a

=

Q

Strd

a

if each

a

i

2

A

i

(for

i

2

n

where

n

is some index set)

where each

(

A

i

2

n

;

Z

i

2

n

)

is a down aligned ltrator with separable core.

[TODO: Duplicate with a

proposition in innite produict of poset elements section.]

Proof.

GR

Q

Strd

a

=

L

2

Q

A

j

up

L

Z

\

Q

Strd

a

 

=

L

2

Q

A

j

up

L

Q

Strd

a

 

=

L

2

Q

A

j 8

K

2

up

L

:

K

2

Q

Strd

a

 

=

f

L

2

Q

A

j 8

K

2

up

L; i

2

n

:

K

i

/

a

i

g

=

f

L

2

Q

A

j 8

i

2

n;

K

2

up

L

:

K

i

/

a

i

g

=

f

L

2

Q

A

j 8

i

2

n

:

L

i

/

a

i

g

=

GR

Q

Strd

a

(taken into account that our ltrator

is with separable core).

218

Multifuncoids and staroids