background image

15.2. COMPOSITION OF POINTFREE FUNCOIDS

201

Proof.

?

h

f

i

(

i

t

j

) =

y

Dst

f

y

6 h

f

i

(

i

t

j

)

=

y

Dst

f

i

t

j

6 h

f

1

i

y

=

y

Dst

f

i

6 h

f

1

i

y

j

6 h

f

1

i

y

=

y

Dst

f

y

6 h

f

i

i

y

6 h

f

i

j

=

y

Dst

f

y

6 h

f

i

i

t h

f

i

j

=

?

(

h

f

i

i

t h

f

i

j

)

.

Thus

h

f

i

(

i

t

j

) =

h

f

i

i

t h

f

i

j

by separability.

Proposition

1072

.

Let

f

be a pointfree funcoid. Then:

1

.

k

[

f

]

i

t

j

k

[

f

]

i

k

[

f

]

j

for every

i, j

Dst

f

,

k

Src

f

if Dst

f

is a

starrish join-semilattice.

2

.

i

t

j

[

f

]

k

i

[

f

]

k

j

[

f

]

k

for every

i, j

Src

f

,

k

Dst

f

if Src

f

is a

starrish join-semilattice.

Proof.

1

.

k

[

f

]

i

t

j

i

t

j

6 h

f

i

k

i

6 h

f

i

k

j

6 h

f

i

k

k

[

f

]

i

k

[

f

]

j

.

2

Similar.

15.2. Composition of pointfree funcoids

Definition

1073

.

Composition

of pointfree funcoids is defined by the formula

(

B

;

C

;

α

2

;

β

2

)

(

A

;

B

;

α

1

;

β

1

) = (

A

;

C

;

α

2

α

1

;

β

1

β

2

)

.

Definition

1074

.

I will call funcoids

f

and

g

composable

when Dst

f

= Src

g

.

Proposition

1075

.

If

f

,

g

are composable pointfree funcoids then

g

f

is

pointfree funcoid.

Proof.

Let

f

= (

A

;

B

;

α

1

;

β

1

),

g

= (

B

;

C

;

α

2

;

β

2

). For every

x, y

A

we have

y

6

(

α

2

α

1

)

x

y

6

α

2

α

1

x

α

1

x

6

β

2

y

x

6

β

1

β

2

y

x

6

(

β

1

β

2

)

y.

So (

A

;

C

;

α

2

α

1

;

β

1

β

2

) is a pointfree funcoid.

Obvious

1076

.

h

g

f

i

=

h

g

i ◦ h

f

i

for every composable pointfree funcoids

f

and

g

.

Theorem

1077

.

(

g

f

)

1

=

f

1

g

1

for every composable pointfree funcoids

f

and

g

.

Proof.

(

g

f

)

1

=

f

1

g

1

=

f

1

g

1

;

((

g

f

)

1

)

1

=

h

g

f

i

=

(

f

1

g

1

)

1

.