 :

(

2

)

):

(

1

).

Suppose

h

f

i

a

2

/

atoms

B

[ f

0

B

g

for some

a

2

atoms

A

. Then there exist two atoms

p

=

/

q

such that

h

f

i

a

w

p

^h

f

i

a

w

q

. Consequently

p

u h

f

i

a

=

/ 0

B

;

a

uh

f

¡

1

i

p

=

/ 0

A

;

a

v h

f

¡

1

i

p

;

h

f

f

¡

1

i

p

=

h

f

ih

f

¡

1

i

p

w h

f

i

a

w

q

(by proposition

15.14

because

B

is separable by

proposition

3.22

);

h

f

f

¡

1

i

p

v

p

and

h

f

f

¡

1

i

p

=

/ 0

B

. So it cannot be

f

f

¡

1

v

id

FCD

(

B

)

.

Theorem 15.105.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over a boolean lattice. A pointfree

funcoid

f

2

FCD

(

A

;

B

)

is monovalued i

8

I ; J

2

Z

1

:

h

f

¡

1

i

(

I

u

Z

1

J

) =

h

f

¡

1

i

I

u h

f

¡

1

i

J:

Proof.

A

and

B

are complete lattices (corollary

4.107

).

(

B

;

Z

1

)

is a ltrator with separable core by the theorem

4.112

.

(

B

;

Z

1

)

is nitely meet-closed by the theorem

4.97

.

A

and

B

are starrish by corollary

4.114

.

A

is separable by obvious

4.136

.

We are under conditions of the theorem

15.25

.

)

.

Obvious (taking into account that

(

B

;

Z

1

)

is nitely meet-closed).

(

.

h

f

¡

1

i

(

I u J

) =

d

hh

f

¡

1

ii

up

(

B

;

Z

1

)

(

I u J

) =

d

hh

f

¡

1

iif

I

u

Z

1

J

j

I

2

up

I

; J

2

up

J g

=

d

fh

f

¡

1

i

(

I

u

Z

1

J

)

j

I

2

up

I

; J

2

up

J g

=

d

fh

f

¡

1

i

I

u h

f

¡

1

i

J

j

I

2

up

I

; J

2

up

J g

=

d

fh

f

¡

1

i

I

j

I

2

up

I g u

d

fh

f

¡

1

i

J

j

J

2

up

J g

=

h

f

¡

1

iI u

A

h

f

¡

1

iJ

(used theorem

15.25

,

theorem

4.110

theorem

15.15

).

15.14 Elements closed regarding a pointfree funcoid

Let

A

be a poset. Let

f

2

FCD

(

A

;

A

)

.

Denition 15.106.

Let's call

closed

regarding a pointfree funcoid

f

such element

a

2

A

that

h

f

i

a

v

a

.

Proposition 15.107.

If

i

and

j

are closed (regarding a pointfree funcoid

f

2

FCD

(

A

;

A

)

),

S

is a

set of closed elements (regarding

f

), then

1.

i

t

j

is a closed element, if

A

is a separable starrish join-semilattice;

2.

d

S

is a closed element if

A

is a separable complete lattice.

Proof.

h

f

i

(

i

t

j

) =

h

f

i

i

t h

f

i

j

v

i

t

j

(theorem

15.15

),

h

f

i

d

S

v

d

hh

f

ii

S

v

d

S

(used separability

of

A

twice). Consequently the elements

i

t

j

and

d

S

are closed.

Proposition 15.108.

If

S

is a set of elements closed regarding a complete pointfree funcoid

f

with separable destination which is a complete lattice, then the element

F

S

is also closed regarding

our funcoid.

Proof.

h

f

i

F

S

=

F

hh

f

ii

S

v

F

S

.

15.15 Connectedness regarding a pointfree funcoid

Let

A

be a poset with least element. Let

2

FCD

(

A

;

A

)

.

[TODO: No necessity for least element.]

Denition 15.109.

An element

a

2

A

is called

connected

regarding a pointfree funcoid

over

A

when

8

x; y

2

A

n f

0

A

g

: (

x

t

y

=

a

)

x

[

]

y

)

:

196

Pointfree funcoids