background image

15.15. CONNECTEDNESS REGARDING A POINTFREE FUNCOID

225

Proposition

1164

.

If

S

is a set of elements closed regarding a complete point-

free 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

µ

FCD

(

A

;

A

).

FiXme

: No necessity

for least element.

Definition

1165

.

An element

a

A

is called

connected

regarding a pointfree

funcoid

µ

over

A

when

x, y

A

\ {⊥

A

}

: (

x

t

y

=

a

x

[

µ

]

y

)

.

Proposition

1166

.

Let (

A

;

Z

) be a co-separable filtrator with join-closed core.

An

A

Z

is connected regarding a funcoid

µ

iff

X, Y

Z

\ {⊥

Z

}

: (

X

t

Z

Y

=

A

X

[

µ

]

Y

)

.

Proof.

. Obvious.

. Follows from co-separability.

Obvious

1167

.

For

A

being a set of filters over a boolean lattice, an element

a

A

is connected regarding a pointfree funcoid

µ

iff it is connected regarding the

funcoid

µ

u

(

a

×

FCD

a

).