6.3. FUNCOID AS CONTINUATION

101

Analogously

X

[

f

]

Y ⇔ ∀

X

∈ X

:

Src

f

X

[

f

]

Y

. Combining these two

equivalences we get

X

[

f

]

Y ⇔ ∀

X

∈ X

, Y

∈ Y

:

Src

f

X

[

f

]

Dst

f

Y

⇔ ∀

X

∈ X

, Y

∈ Y

:

X

[

f

]

Y.

1

.

Y u h

f

iX 6

=

F

(Dst

f

)

X

[

f

]

Y ⇔

X

∈ X

:

Src

f

X

[

f

]

Y ⇔

X

∈ X

:

Y u h

f

i

X

6

=

F

(Dst

f

)

.

Let’s denote

W

=

n

Yuh

f

i

X

X

∈X

o

. We will prove that

W

is a generalized filter

base. To prove this it is enough to show that

V

=

n

h

f

i

X

X

∈X

o

is a generalized filter

base.

Let

P

,

Q ∈

V

. Then

P

=

h

f

i

A

,

Q

=

h

f

i

B

where

A, B

∈ X

;

A

B

∈ X

and

R v P u Q

for

R

=

h

f

i

(

A

B

)

V

. So

V

is a generalized filter base and thus

W

is a generalized filter base.

F

(Dst

f

)

/

W

d

W

6

=

F

(Dst

f

)

by properties of generalized filter bases.

That is

X

∈ X

:

Y u h

f

i

X

6≡ ⊥

F

(Dst

f

)

⇔ Y u

l

h

f

i

X 6

=

F

(Dst

f

)

.

Comparing with the above,

Y uh

f

iX 6

=

F

(Dst

f

)

⇔ Y u

d

h

f

i

X 6

=

F

(Dst

f

)

.

So

h

f

iX

=

d

h

f

i

X

because the lattice of filters is separable.

Corollary

593

.

Let

f

be a funcoid.

1

. The value of

f

can be restored knowing

h

f

i

.

2

. The value of

f

can be restored knowing [

f

]

.

Proposition

594

.

For every

f

FCD

(

A

;

B

) we have (for every

I, J

P

A

)

h

f

i

=

F

(

B

)

,

h

f

i

(

I

J

) =

h

f

i

I

t h

f

i

J

and

¬

(

I

[

f

]

)

,

I

J

[

f

]

K

I

[

f

]

K

J

[

f

]

K

(for every

I, J

P

A

,

K

P

B

)

,

¬

(

[

f

]

I

)

,

K

[

f

]

I

J

K

[

f

]

I

K

[

f

]

J

(for every

I, J

P

B

,

K

P

A

)

.

Proof.

h

f

i

=

h

f

i ↑

A

=

h

f

i⊥

F

(

A

)

=

F

(

B

)

;

h

f

i

(

I

J

) =

h

f

i ↑

A

(

I

J

) =

h

f

i ↑

A

I

t h

f

i ↑

A

J

=

h

f

i

I

t h

f

i

J.

I

[

f

]

∅ ⇔ ⊥

F

(

B

)

6 h

f

i ↑

A

I

0;

I

J

[

f

]

K

A

(

I

J

) [

f

]

B

K

B

K

6 h

f

i ↑

A

(

I

J

)

B

K

6 h

f

i

(

I

J

)

B

K

6 h

f

i

I

t h

f

i

J

B

K

6 h

f

i

I

∨ ↑

B

K

6 h

f

i

J

I

[

f

]

K

J

[

f

]

K.

The rest follows from symmetry.