7.3. FUNCOID AS CONTINUATION

148

2

.

X

[

f

]

Y ⇔

Y u h

f

iX 6

=

⊥ ⇔

Y

up

Y

:

Y

u h

f

iX 6

=

⊥ ⇔

Y

up

Y

:

X

[

f

]

Y.

Analogously

X

[

f

]

Y ⇔ ∀

X

up

X

:

X

[

f

]

Y

. Combining these two equiva-

lences we get

X

[

f

]

Y ⇔ ∀

X

up

X

, Y

up

Y

:

X

[

f

]

Y

⇔ ∀

X

up

X

, Y

up

Y

:

X

[

f

]

Y.

1

.

Y u h

f

iX 6

=

⊥ ⇔

X

[

f

]

Y ⇔

X

up

X

:

X

[

f

]

Y ⇔

X

up

X

:

Y u h

f

i

X

6

=

.

Let’s denote

W

=

n

Yuh

f

i

X

X

up

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

up

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

up

X

;

A

u

B

up

X

and

R v P u Q

for

R

=

h

f

i

(

A

u

B

)

V

. So

V

is a generalized filter base and

thus

W

is a generalized filter base.

/

W

d

W

6

=

by properties of generalized filter bases. That is

X

up

X

:

Y u h

f

i

X

6

=

F

(Dst

f

)

⇔ Y u

l

h

f

i

up

X 6

=

.

Comparing with the above,

Y u h

f

iX 6

=

F

(Dst

f

)

⇔ Y u

d

h

f

i

up

X 6

=

.

So

h

f

iX

=

d

h

f

i

up

X

because the lattice of filters is separable.

Corollary

826

.

Let

f

be a funcoid.

1

. The value of

f

can be restored from the value of

h

f

i

.

2

. The value of

f

can be restored from the value of [

f

]

.

Proposition

827

.

For every

f

FCD

(

A, B

) we have (for every

I, J

T

A

)

h

f

i

=

,

h

f

i

(

I

t

J

) =

h

f

i

I

t h

f

i

J

and

¬

(

I

[

f

]

)

,

I

t

J

[

f

]

K

I

[

f

]

K

J

[

f

]

K

(for every

I, J

T

A

,

K

T

B

)

,

¬

(

[

f

]

I

)

,

K

[

f

]

I

t

J

K

[

f

]

I

K

[

f

]

J

(for every

I, J

T

B

,

K

T

A

)

.

Proof.

h

f

i

=

h

f

i⊥

=

h

f

i⊥

=

;

h

f

i

(

I

t

J

) =

h

f

i ↑

(

I

t

J

) =

h

f

i ↑

I

t h

f

i ↑

J

=

h

f

i

I

t h

f

i

J.