background image

15.10. ATOMIC POINTFREE FUNCOIDS

218

Proof.

(

a

×

FCD

b

)

u

(

f

t

g

)

6

=

∅ ⇔

a

[

f

t

g

]

b

a

[

f

]

b

a

[

g

]

b

(

a

×

FCD

b

)

u

f

6

=

FCD

(

A

;

B

)

(

a

×

FCD

b

)

u

g

6

=

FCD

(

A

;

B

)

for every

a

atoms

A

and

b

atoms

B

(used the corollary

1125

and theorem

1091

).

Theorem

1139

.

Let (

A

;

Z

0

) and (

B

;

Z

1

) be primary filtrators over boolean

lattices. For every

f, g, h

FCD

(

A

;

B

),

R

P

FCD

(

A

;

B

):

1

.

f

u

(

g

t

h

) = (

f

u

g

)

t

(

f

u

h

);

2

.

f

t

d

R

=

d

h

f

ti

R

.

Proof.

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

atomistic lattice (corollary

1137

).

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

l

R

=

atoms

f

atoms

l

R

=

atoms

f

\

h

atoms

i

R

=

\

h

(atoms

f

)

∪i

h

atoms

i

R

= (use the following equality)

\

h

atoms

i

h

f

ti

R

=

atoms

l

h

f

ti

R.

h

(atoms

f

)

∪i

h

atoms

i

R

=

(atoms

f

)

A

A

∈ h

atoms

i

R

=

(atoms

f

)

A

C

R

:

A

= atoms

C

=

(atoms

f

)

(atoms

C

)

C

R

=

atoms(

f

t

C

)

C

R

=

atoms

B

C

R

:

B

=

f

t

C

=

atoms

B

B

∈ h

f

ti

C

=

h

atoms

i

h

f

ti

R.