 15.14. ELEMENTS CLOSED REGARDING A POINTFREE FUNCOID

224

every

a, b

atoms

B

. This is possible only (corollary

1112

and the fact

that

B

is atomic) when

f

f

1

v

id

FCD

(

B

)

.

¬

2

⇒ ¬

1

Suppose

h

f

i

a /

atoms

B

∪{⊥

B

}

for some

a

atoms

A

. Then there

exist two atoms

p

6

=

q

such that

h

f

i

a

w

p

∧ h

f

i

a

w

q

. Consequently

p

u h

f

i

a

6

= 0

B

;

a

u

f

1

p

6

=

A

;

a

v

f

1

p

;

f

f

1

p

=

h

f

i

f

1

p

w

h

f

i

a

w

q

(by proposition

1070

because

B

is separable by proposition

181

);

f

f

1

p

6v

p

and

f

f

1

p

6

=

B

. So it cannot be

f

f

1

v

id

FCD

(

B

)

.

Theorem

1161

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over a boolean

lattice. A pointfree funcoid

f

FCD

(

A

;

B

) is monovalued iff

I, J

Z

1

:

f

1

(

I

u

Z

1

J

) =

f

1

I

u

f

1

J.

Proof.

A

and

B

are complete lattices (corollary

374

).

(

B

;

Z

1

) is a filtrator with separable core by the theorem

379

.

(

B

;

Z

1

) is finitely meet-closed by the theorem

364

.

A

and

B

are starrish by corollary

381

.

A

is separable by obvious

403

.

We are under conditions of the theorem

1081

.

. Obvious (taking into account that (

B

;

Z

1

) is finitely meet-closed).

.

f

1

(

I u J

) =

l

f

1

up

(

B

;

Z

1

)

(

I u J

) =

l

f

1

I

u

Z

1

J

I

up

I

, J

up

J

=

l

(

f

1

(

I

u

Z

1

J

)

I

up

I

, J

up

J

)

=

l

f

1

I

u

f

1

J

I

up

I

, J

up

J

)

=

l

f

1

I

I

up

I

)

u

l

(

f

1

J

J

up

J

)

=

f

1

I u

A

f

1

J

(used theorem

1081

theorem

377

theorem

1071

).

15.14. Elements closed regarding a pointfree funcoid

Let

A

be a poset. Let

f

FCD

(

A

;

A

).

Definition

1162

.

Let’s call

closed

regarding a pointfree funcoid

f

such element

a

A

that

h

f

i

a

v

a

.

Proposition

1163

.

If

i

and

j

are closed (regarding a pointfree funcoid

f

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

1071

),

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.