background image

7.11. ATOMIC FUNCOIDS

167

7.11. Atomic funcoids

Theorem

895

.

An

f

FCD

(

A, B

) is an atom of the lattice

FCD

(

A, B

) (for

some sets

A

,

B

) iff it is a funcoidal product of two atomic filter objects.

Proof.

. Let

f

FCD

(

A, B

) be an atom of the lattice

FCD

(

A, B

). Let’s get elements

a

atoms dom

f

and

b

atoms

h

f

i

a

. Then for every

X ∈

F

(

A

)

a

a

×

FCD

b

X

=

⊥ v h

f

iX

,

X 6

a

a

×

FCD

b

X

=

b

v h

f

iX

.

So

a

×

FCD

b

v

f

; because

f

is atomic we have

f

=

a

×

FCD

b

.

. Let

a

atoms

F

(

A

)

,

b

atoms

F

(

B

)

,

f

FCD

(

A, B

). If

b

 h

f

i

a

then

¬

(

a

[

f

]

b

),

f

a

×

FCD

b

; if

b

v h

f

i

a

then

∀X ∈

F

(

A

) : (

X 6

a

⇒ h

f

iX w

b

),

f

w

a

×

FCD

b

. Consequently

f

a

×

FCD

b

f

w

a

×

FCD

b

; that is

a

×

FCD

b

is an atom.

Theorem

896

.

The lattice

FCD

(

A, B

) is atomic (for every fixed sets

A

,

B

).

Proof.

Let

f

be a non-empty funcoid from

A

to

B

. Then dom

f

6

=

, thus

by theorem

573

there exists

a

atoms dom

f

. So

h

f

i

a

6

=

thus it exists

b

atoms

h

f

i

a

. Finally the atomic funcoid

a

×

FCD

b

v

f

.

Theorem

897

.

The lattice

FCD

(

A, B

) is separable (for every fixed sets

A

,

B

).

Proof.

Let

f, g

FCD

(

A, B

),

f

@

g

. Then there exists

a

atoms

F

(

A

)

such

that

h

f

i

a

@

h

g

i

a

. So because the lattice

F

(

B

) is atomically separable, there exists

b

atoms such that

h

f

i

a

u

b

=

and

b

v h

g

i

a

. For every

x

atoms

F

(

A

)

h

f

i

a

u

a

×

FCD

b

a

=

h

f

i

a

u

b

=

,

x

6

=

a

⇒ h

f

i

x

u

a

×

FCD

b

x

=

h

f

i

x

u ⊥

=

.

Thus

h

f

i

x

u

a

×

FCD

b

x

=

and consequently

f

a

×

FCD

b

.

a

×

FCD

b

a

=

b

v h

g

i

a,

x

6

=

a

a

×

FCD

b

x

=

⊥ v h

g

i

x.

Thus

a

×

FCD

b

x

v h

g

i

x

and consequently

a

×

FCD

b

v

g

.

So the lattice

FCD

(

A, B

) is separable by theorem

222

.

Corollary

898

.

The lattice

FCD

(

A, B

) is:

1

. separable;

2

. strongly separable;

3

. atomically separable;

4

. conforming to Wallman’s disjunction property.

Proof.

By theorem

230

.

Remark

899

.

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

of funcoids see subsections “Separation subsets and full stars” and “Atomically

separable lattices”.

Corollary

900

.

The lattice

FCD

(

A, B

) is an atomistic lattice.

Proof.

By theorem

228

.

Proposition

901

.

atoms(

f

t

g

) = atoms

f

atoms

g

for every funcoids

f, g

FCD

(

A, B

) (for every sets

A

,

B

).