background image

19.15. CONNECTEDNESS REGARDING A POINTFREE FUNCOID

308

.

f

1

(

I u J

) =

l

f

1

up

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

1509

corollary

518

theorem

1498

).

Proposition

1593

.

Let

A

be an atomistic meet-semilattice with least element,

B

be an atomistic bounded meet-semilattice. Then if

f

,

g

are pointfree funcoids

from

A

to

B

,

f

v

g

and

g

is monovalued then

g

|

dom

f

=

f

.

Proof.

Obviously

g

|

dom

f

w

f

. Suppose for contrary that

g

|

dom

f

@

f

. Then

there exists an atom

a

atoms dom

f

such that

h

g

|

dom

f

i

a

6

=

h

f

i

a

that is

h

g

i

a

@

h

f

i

a

what is impossible.

19.14. Elements closed regarding a pointfree funcoid

Let

A

be a poset. Let

f

pFCD

(

A

,

A

).

Definition

1594

.

Let’s call

closed

regarding a pointfree funcoid

f

such element

a

A

that

h

f

i

a

v

a

.

Proposition

1595

.

If

i

and

j

are closed (regarding a pointfree funcoid

f

pFCD

(

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 strongly separable complete lattice.

Proof.

h

f

i

(

i

t

j

) =

h

f

i

i

t h

f

i

j

v

i

t

j

(theorem

1498

),

h

f

i

d

S

v

d

hh

f

ii

S

v

d

S

(used strong separability of

A

twice). Consequently the elements

i

t

j

and

d

S

are closed.

Proposition

1596

.

If

S

is a set of elements closed regarding a complete point-

free funcoid

f

with strongly separable destination which is a complete lattice, then

the element

d

S

is also closed regarding our funcoid.

Proof.

h

f

i

d

S

=

d

hh

f

ii

S

v

d

S

.

19.15. Connectedness regarding a pointfree funcoid

Let

A

be a poset with least element. Let

µ

pFCD

(

A

,

A

).

Definition

1597

.

An element

a

A

is called

connected

regarding a pointfree

funcoid

µ

over

A

when

x, y

A

\ {⊥

A

}

: (

x

t

y

=

a

x

[

µ

]

y

)

.