background image

19.7. MORE ON COMPOSITION OF POINTFREE FUNCOIDS

297

Theorem

1549

.

Let

f

and

g

be pointfree funcoids and

A

= Dst

f

= Src

g

be

an atomic poset. Then for every

X ∈

Src

f

and

Z ∈

Dst

g

X

[

g

f

]

Z ⇔ ∃

y

atoms

A

: (

X

[

f

]

y

y

[

g

]

Z

)

.

Proof.

y

atoms

A

: (

X

[

f

]

y

y

[

g

]

Z

)

y

atoms

A

: (

Z 6 h

g

i

y

y

6 h

f

iX

)

y

atoms

A

: (

y

6

g

1

Z ∧

y

6 h

f

iX

)

g

1

Z 6 h

f

iX ⇔

X

[

g

f

]

Z

.

Theorem

1550

.

Let

A

,

B

,

C

be separable starrish join-semilattices and

B

is

atomic. Then:

1

.

f

(

g

t

h

) =

f

g

t

f

h

for

g, h

pFCD

(

A

,

B

) and

f

pFCD

(

B

,

C

).

2

. (

g

t

h

)

f

=

g

f

t

h

f

for

f

pFCD

(

A

,

B

) and

g, h

pFCD

(

B

,

C

).

Proof.

I will prove only the first equality because the other is analogous.

We can apply theorem

1526

.

For every

X ∈

A

,

Y ∈

C

X

[

f

(

g

t

h

)]

Z ⇔

y

atoms

B

: (

X

[

g

t

h

]

y

y

[

f

]

Z

)

y

atoms

B

: ((

X

[

g

]

y

∨ X

[

h

]

y

)

y

[

f

]

Z

)

y

atoms

B

: ((

X

[

g

]

y

y

[

f

]

Z

)

(

X

[

h

]

y

y

[

f

]

Z

))

y

atoms

B

: (

X

[

g

]

y

y

[

f

]

Z

)

∨ ∃

y

atoms

B

: (

X

[

h

]

y

y

[

f

]

Z

)

X

[

f

g

]

Z ∨ X

[

f

h

]

Z ⇔

X

[

f

g

t

f

h

]

Z

.

Thus

f

(

g

t

h

) =

f

g

t

f

h

by theorem

1495

.

Theorem

1551

.

Let

A

,

B

,

C

be posets of filters over some boolean lattices,

f

pFCD

(

A

,

B

),

g

pFCD

(

B

,

C

),

h

pFCD

(

A

,

C

). Then

g

f

6

h

g

6

h

f

1

.

Proof.

g

f

6

h

a

atoms

A

, c

atoms

C

:

a

[(

g

f

)

u

h

]

c

a

atoms

A

, c

atoms

C

: (

a

[

g

f

]

c

a

[

h

]

c

)

a

atoms

A

, b

atoms

B

, c

atoms

C

: (

a

[

f

]

b

b

[

g

]

c

a

[

h

]

c

)

b

atoms

B

, c

atoms

C

: (

b

[

g

]

c

b

h

f

1

c

)

b

atoms

B

, c

atoms

C

:

b

g

u

(

h

f

1

)

c

g

6

h

f

1

.