background image

Let continue

α

till a funcoid

f

(by the theorem 26):

h

f

iX

=

T

B

h

α

i

up

(

A

;

Z

0

)

X

.

Let’s prove the reverse of (5):

\

B

 [

B

◦ h

α

i ◦

atoms

A

up

(

A

;

Z

0

)

a

=

\

B

 [

B

◦ h

α

i

h

atoms

A

i

up

(

A

;

Z

0

)

a

\

B

 [

B

◦ h

α

i

{{

a

}}

=

\

B

[

B

◦ h

α

i

{

a

}

 

=

\

B

[

B

h

α

i{

a

}

 

=

\

B

[

B

{

αa

}

 

=

\

B

{

αa

}

=

α a.

Finally,

αa

=

\

B

 [

B

◦ h

α

i ◦

atoms

A

up

a

=

\

B

h

α

i

up

(

A

;

Z

0

)

a

=

h

f

i

a,

so

h

f

i

is a continuation of

α

.

2. Consider the relation

δ

P

(

Z

0

×

Z

1

)

defined by the formula (for every

X

Z

0

,

Y

Z

1

)

X δ

Y

⇔ ∃

x

atoms

A

X , y

atoms

B

Y

:

x δ y.

Obviously

¬

(

X δ

0

Z

1

)

and

¬

(0

Z

0

δ

Y

)

.

(

I

J

)

δ

Y

⇔ ∃

x

atoms

A

(

I

J

)

, y

atoms

B

Y

:

x δ y

⇔ ∃

x

atoms

A

I

atoms

A

J , y

atoms

B

Y

:

x δ y

⇔ ∃

x

atoms

A

I , y

atoms

B

Y

:

x δ y

∨ ∃

x

atoms

A

J , y

atoms

B

Y

:

x δ y

I δ

Y

J δ

Y

;

similarly

X δ

(

I

J

)

X δ

I

X δ

J

. Let’s continue

δ

till a funcoid

f

(by the theorem 26):

X

[

f

]

Y ⇔ ∀

X

up

(

A

;

Z

0

)

X

, Y

up

(

B

;

Z

1

)

Y

:

X δ

Y

The reverse of (7) implication is trivial, so

X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

x

atoms

A

X , y

atoms

B

Y

:

x δ y

a δ b.

X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

x

atoms

A

X , y

atoms

B

Y

:

x δ y

⇔ ∀

X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

:

X δ

Y

a

[

f

]

b

.

So

a δ b

a

[

f

]

b

, that is

[

f

]

is a continuation of

δ

.

One of uses of the previous theorem is the proof of the following theorem:

Theorem 56.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

are primary filtrators over boolean lattices. If

R

P

FCD

(

A

;

B

)

and

x

atoms

A

,

y

atoms

B

, then

1.

 T

FCD

(

A

;

B

)

R

x

=

T

B

{h

f

i

x

|

f

R

}

;

2.

x

 T

FCD

(

A

;

B

)

R

y

⇔ ∀

f

R

:

x

[

f

]

y

.

Proof.

2. Let denote

x δ y

⇔ ∀

f

R

:

x

[

f

]

y

.

X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

x

atoms

A

X , y

atoms

B

Y

:

x δ y

f

R, X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

x

atoms

A

X , y

atoms

B

Y

:

x

[

f

]

y

f

R, X

up

(

A

;

Z

0

)

a, Y

up

(

B

;

Z

1

)

b

:

X

[

f

]

Y

f

R

:

a

[

f

]

b

a δ b.

So, by the theorem 55,

δ

can be continued till

[

p

]

for some

p

FCD

(

A

;

B

)

.

For every

q

FCD

(

A

;

B

)

such that

f

R

:

q

f

we have

x

[

q

]

y

⇒ ∀

f

R

:

x

[

f

]

y

x δ y

x

[

p

]

y

,

so

q

p

. Consequently

p

=

T

FCD

(

A

;

B

)

R

.

Pointfree funcoids

11