 7.11. ATOMIC FUNCOIDS

168

Proof.

a

×

FCD

b

6

f

t

g

a

[

f

t

g

]

b

a

[

f

]

b

a

[

g

]

b

a

×

FCD

b

6

f

a

×

FCD

b

6

g

for every atomic filters

a

and

b

.

Theorem

902

.

The set of funcoids between sets

A

and

B

is a co-frame.

Proof.

Theorems

828

and

530

.

Remark

903

.

The above proof does not use axiom of choice (unlike the below

proof).

See also an older proof of the set of funcoids being co-brouwerian:

Theorem

904

.

For every

f, g, h

FCD

(

A, B

),

R

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

ti

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

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.