17.14. ON PRODUCTS AND PROJECTIONS

271

Proof.

Pr

k

GR

Strd

Y

x

=

Pr

k

L

`

i

dom

x

form

x

i

i

dom

x

:

x

i

6

L

i

=

(used the fact that

x

i

are proper filters)

l

form

x

k

x

k

6

l

=

?x

k

.

Proposition

1395

.

Pr

Strd

k

Q

Strd

x

=

x

k

if

x

is an indexed family of proper

filters, and

k

dom

x

.

Proof.

Strd

Pr

k

Strd

Y

x

=

val

Strd

Y

x

!

k

(

λi

(dom

x

)

\ {

k

}

:

>

(form

x

)

i

) =

X

form

Q

Strd

x

k

(

λi

(dom

x

)

\ {

k

}

:

>

(form

x

)

i

)

∪ {

(

k

;

X

)

} ∈

GR

Q

Strd

x

=

X

Base

x

k

(

i

(dom

x

)

\ {

k

}

:

>

(form

x

)

i

6

x

i

)

X

6

x

k

=

X

Base

x

k

X

6

x

k

=

∂x

k

.

Consequently Pr

Strd

k

Q

Strd

x

=

x

k

.

17.14.2. Cross-composition product of pointfree funcoids.

Definition

1396

.

Zero

pointfree funcoid from a poset

A

to to a poset

B

is such

a pointfree funcoid

A

B

that

h

f

i

x

is a least element of

B

for every

x

A

.

FiXme

:

Zero function is the same as the minimum funcoid, isn’t it?

Proposition

1397

.

A pointfree funcoid

f

is zero iff [

f

]=

.

Proof.

Direct implication is obvious.

Let now [

f

]=

. Then

h

f

i

x

y

for every

x

Src

f

,

y

Dst

f

and thus

h

f

i

x

h

f

i

x

. It is possible only when

h

f

i

x

=

Dst

f

.

Corollary

1398

.

A pointfree funcoid is zero iff its reverse is zero.

Proposition

1399

.

Values

x

i

(for every

i

dom

x

) can be restored from the

value of

Q

(

C

)

x

provided that

x

is an indexed family of non-zero pointfree funcoids

if Src

f

i

(for every

i

n

) is an atomic lattice and every Dst

f

i

is an atomic poset

with greatest element.

Proof.

D

Q

(

C

)

x

E

Q

Strd

p

=

Q

Strd

i

n

h

x

i

i

p

i

by theorem

1351

.

Since

x

i

is non-zero there exist

p

such that

h

x

i

i

p

i

is non-zero. Take

k

n

,

p

0

i

=

p

i

for

i

6

=

k

and

p

0

k

=

q

for an arbitrary value

q

; then (using the staroidal

projections from the previous subsection)

h

x

k

i

q

=

Strd

Pr

k

Strd

Y

i

n

h

x

i

i

p

0

i

=

Strd

Pr

k

*

(

C

)

Y

x

+

Strd

Y

p

0

.