 21.3. UPGRADING AND DOWNGRADING A SET REGARDING A FILTRATOR

322

Proof.

c

∈ {

0

,

1

}

n

: (

λi

n

:

L

c

(

i

)

i

)

GR

f

c

∈ {

0

,

1

}

n

1

:

(

{

(

n

1

, L

0

(

n

1))

} ∪

(

λi

n

1 :

L

c

(

i

)

i

))

GR

f

(

{

(

n

1

, L

1

(

n

1))

} ∪

(

λi

n

1 :

L

c

(

i

)

i

))

GR

f

!

c

∈ {

0

,

1

}

n

1

:

L

0

(

n

1)

(val

f

)

n

1

(

λi

n

1 :

L

c

(

i

)

i

)

L

1

(

n

1)

(val

f

)

n

1

(

λi

n

1 :

L

c

(

i

)

i

)

!

c

∈ {

0

,

1

}

n

1

K

(form

f

)

i

:

K

w

L

0

(

n

1)

K

w

L

1

(

n

1)

K

(val

f

)

n

1

(

λi

n

1 :

L

c

(

i

)

i

)

!

c

∈ {

0

,

1

}

n

1

K

(form

f

)

i

:

K

w

L

0

(

n

1)

K

w

L

1

(

n

1)

{

(

n

1

, K

)

} ∪

(

λi

n

1 :

L

c

(

i

)

i

)

GR

f

!

. . .

K

Y

form

f

: (

K

w

L

0

K

w

L

1

K

GR

f

)

.

Exercise

1647

.

Prove the simpler special case of the above theorem when the

form is a family of join-semilattices.

Theorem

1648

.

For finite arity the following are the same:

1

. prestaroids;

2

. staroids;

3

. completary staroids.

Proof.

f

is a finitary prestaroid

f

is a finitary completary staroid.

f

is a finitary completary staroid

f

is a finitary staroid.

f

is a finitary staroid

f

is a finitary prestaroid.

Definition

1649

.

We will denote the set of staroids of a form

A

as

Strd

(

A

).

21.3. Upgrading and downgrading a set regarding a filtrator

Let fix a filtrator (

A

,

Z

).

Definition

1650

.

f

=

f

Z

for every

f

P

A

(

f

).

Definition

1651

.

f

=

n

L

A

up

L

f

o

for every

f

P

Z

(

f

).

Obvious

1652

.

a

f

up

a

f

for every

f

P

Z

and

a

A

.

Proposition

1653

.

f

=

f

if

f

is an upper set for every

f

P

Z

.

Proof.

f

=

f

Z

=

n

L

Z

up

L

f

o

=

n

L

Z

L

f

o

=

f

Z

=

f

.

Let fix a family (

A

,

Z

) of

filtrators.

For a graph

f

of an anchored relation between posets define

f

and

f

taking the filtrator of (

Q

A

,

Q

Z

).

For a anchored relation between posets

f

define:

form

f

=

Z

and GR

f

=

GR

f

;

form

f

=

A

and GR

f

=

GR

f.

Below we will show that under certain conditions upgraded staroid is a staroid,

see theorem

1678

.