Proof.

By theorem

3.21

.

Remark 6.87.

For more ways to characterize (atomic) separability of the lattice of funcoids see

subsections Separation subsets and full stars and Atomically separable lattices.

Corollary 6.88.

The lattice

FCD

(

A

;

B

)

is an atomistic lattice.

Proof.

Let

f

2

FCD

(

A

;

B

)

. Suppose contrary to the statement to be proved that

F

atoms

f

@

f

.

Then there exists

a

2

atoms

f

such that

a

u

F

atoms

f

= 0

FCD

(

A

;

B

)

what is impossible.

Proposition 6.89.

atoms

(

f

t

g

) =

atoms

f

[

atoms

g

for every funcoids

f ; g

2

FCD

(

A

;

B

)

(for

every sets

A

,

B

).

Proof.

a

FCD

b

/

f

t

g

,

a

[

f

t

g

]

b

,

a

[

f

]

b

_

a

[

g

]

b

,

a

FCD

b

/

f

_

a

FCD

b

/

g

for every atomic

lters

a

and

b

.

Theorem 6.90.

For every

f ; g; h

2

FCD

(

A

;

B

)

,

R

2

P

FCD

(

A

;

B

)

(for every sets

A

and

B

)

1.

f

u

(

g

t

h

) = (

f

u

g

)

t

(

f

u

h

)

;

2.

f

t

d

R

=

d

h

f

t i

R

.

Proof.

We will take into account that the lattice of funcoids is an atomistic lattice.

1. atoms

(

f

u

(

g

t

h

)) =

atoms

f

\

atoms

(

g

t

h

) =

atoms

f

\

(

atoms

g

[

atoms

h

) =

(

atoms

f

\

atoms

g

)

[

(

atoms

f

\

atoms

h

) =

atoms

(

f

u

g

)

[

atoms

(

f

u

h

) =

atoms

((

f

u

g

)

t

(

f

u

h

))

.

2. atoms

(

f

t

d

R

) =

atoms

f

[

atoms

d

R

=

atoms

f

[

T

h

atoms

i

R

=

T

h

(

atoms

f

)

[

ih

atoms

i

R

=

T

h

atoms

ih

f

t i

R

=

atoms

d

h

f

t i

R

. (Used the following equality.)

h

(

atoms

f

)

[ ih

atoms

i

R

=

f

(

atoms

f

)

[

A

j

A

2 h

atoms

i

R

g

=

f

(

atoms

f

)

[

A

j 9

C

2

R

:

A

=

atoms

C

g

=

f

(

atoms

f

)

[

(

atoms

C

)

j

C

2

R

g

=

f

atoms

(

f

t

C

)

j

C

2

R

g

=

f

atoms

B

j 9

C

2

R

:

B

=

f

t

C

g

=

f

atoms

B

j

B

2 h

f

t i

R

g

=

h

atoms

ih

f

t i

R:

Note that distributivity of the lattice of funcoids is proved through using atoms of this lattice.

I have never seen such method of proving distributivity.

Corollary 6.91.

The lattice

FCD

(

A

;

B

)

is co-brouwerian (for every sets

A

,

B

).

Conjecture 6.92.

Distributivity of the lattice

FCD

(

A

;

B

)

of funcoids (for arbitrary sets

A

and

B

) is not provable in ZF (without axiom of choice).

The next proposition is one more (among the theorem

6.44

generalization for funcoids of

composition of relations.

Proposition 6.93.

For every composable funcoids

f

,

g

atoms

(

g

f

) =

(

x

FCD

z

j

x

2

atoms

F

(

Src

f

)

; z

2

atoms

F

(

Dst

g

)

;

9

y

2

atoms

F

(

Dst

f

)

: (

x

FCD

y

2

atoms

f

^

y

FCD

z

2

atoms

g

)

)

:

Proof.

x

FCD

z

/

g

f

,

x

[

g

f

]

z

, 9

y

2

atoms

F

(

Dst

f

)

: (

x

FCD

y

/

f

^

y

FCD

z

/

g

)

(it was used

the theorem

6.44

).

Corollary 6.94.

g

f

=

F

f

G

F

j

F

2

atoms

f ; G

2

atoms

g

g

for every composable funcoids

f

,

g

.

110

Funcoids