background image

2.

(

g

FCD

(

B

;

C

)

h

)

f

=

g

f

FCD

(

A

;

C

)

h

f

for

f

FCD

(

A

;

B

)

and

g, h

FCD

(

B

;

C

)

.

Proof.

I will prove only the first equality because the other is analogous.

For every

X ∈

A

,

Y ∈

C

X

f

(

g

FCD

(

A

;

B

)

h

)

Z ⇔ ∃

y

atoms

B

: (

X

g

FCD

(

A

;

B

)

h

y

y

[

f

]

Z

)

⇔ ∃

y

atoms

B

: ((

X

[

g

]

y

∨ X

[

h

]

y

)

y

[

f

]

Z

)

⇔ ∃

y

atoms

B

: ((

X

[

g

]

y

y

[

f

]

Z

)

(

X

[

h

]

y

y

[

f

]

Z

))

⇔ ∃

y

atoms

B

: (

X

[

g

]

y

y

[

f

]

Z

)

∨ ∃

y

atoms

B

: (

X

[

h

]

y

y

[

f

]

Z

)

⇔ X

[

f

g

]

Z ∨ X

[

f

h

]

Z

⇔ X

f

g

FCD

(

A

;

C

)

f

h

Z

.

3.6 Domain and range of a pointfree funcoid

Definition 38.

Let

A

is a poset. The

identity pointfree funcoid

I

FCD

(

A

)

= (

A

;

A

; (=)

|

A

; (=)

|

A

)

.

It is trivial that identity funcoid is really a pointfree funcoid.
Let now

A

is a meet-semilattice.

Definition 39.

Let

a

A

. The

restricted identity pointfree funcoid

I

a

FCD

(

A

)

= (

A

;

A

;

a

A

;

a

A

)

.

Proposition 40.

The restricted pointfree funcoid is a pointfree funcoid.

Proof.

We need to prove that

(

a

A

x

)

A

y

(

a

A

y

)

A

x

what is obvious.

Obvious 41.

I

A

FCD

(

A

)

1

=

I

A

FCD

(

A

)

.

Obvious 42.

x

h

I

A

FCD

(

A

)

i

y

a

A

x

A

y

for every

x, y

A

.

Definition 43.

I will define

restricting

of a pointfree funcoid

f

to an element

a

Src

f

by the

formula

f

|

a

=

def

f

I

a

FCD

(

Src

f

)

.

Definition 44.

Let

f

is a pointfree funcoid whose source has greatest element

1

.

Image

of

f

will be defined by the formula im

f

=

h

f

i

1

.

Definition 45.

Domain

of a pointfree funcoid

f

is defined by the formula dom

f

=

im

f

1

(when

f

has a poset with greatest element as its destination).

Proposition 46.

h

f

i

x

=

h

f

i

(

x

Src

f

dom

f

)

for every pointfree funcoid

f

whose destination is a

separable poset with greatest element and source is a meet-semilattice and

x

Src

f

.

Proof.

For every

y

Dst

f

we have

y

Dst

f

h

f

i

(

x

Src

f

dom

f

)

0

Dst

f

x

Src

f

dom

f

Src

f

h

f

1

i

y

0

Src

f

x

Src

f

im

f

1

Src

f

h

f

1

i

y

0

Src

f

x

Src

f

h

f

1

i

y

0

Src

f

y

Dst

f

h

f

i

x

. Thus

h

f

i

x

=

h

f

i

(

x

Src

f

dom

f

)

by separability of Dst

f

.

Proposition 47.

x

Src

f

dom

f

(

h

f

i

x

is not least

)

for every pointfree funcoid

f

whose

destination is a poset with greatest element and

x

Src

f

.

Proof.

x

Src

f

dom

f

x

Src

f

h

f

1

i

1

1

Dst

f

Dst

f

h

f

i

x

(

h

f

i

x

is not least

)

.

Corollary 48.

dom

f

=

S

Src

f

{

a

atoms

Src

f

| h

f

i

a

0

Dst

f

}

for every pointfree funcoid

f

whose

destination is a bounded poset and source is an atomistic meet-semilattice.

Proof.

For every

a

atoms

Src

f

we have

a

Src

f

dom

f

a

Src

f

im

f

1

a

Src

f

h

f

1

i

1

Dst

f

1

Dst

f

h

f

i

a

⇔ h

f

i

a

0

Dst

f

. So

8

Section 3