7.3. FUNCOID AS CONTINUATION

150

what is equivalent to

X

up

X

, Y

up

Y

:

Y

u

αX

6

=

⊥ ⇔

X

up

X

, Y

up

Y

:

Y

(

αX

)

X

up

X

, Y

up

Y

:

X δ Y.

Combining the equivalencies we get

Y u

α

0

X 6

=

⊥ ⇔ X

δ

0

Y

. Analogously

X u

β

0

Y 6

=

⊥ ⇔ X

δ

0

Y

. So

Y u

α

0

X 6

=

⊥ ⇔ X u

β

0

Y 6

=

, that is (

A, B, α

0

, β

0

) is

a funcoid. From the formula

Y u

α

0

X 6

=

F

(

B

)

⇔ X

δ

0

Y

it follows that

X

[(

A, B, α

0

, β

0

)]

Y

⇔↑

Y

u

α

0

X

6

=

⊥ ⇔↑

X δ

0

Y

X δ Y.

1

Let define the relation

δ

P

(

T

A

×

T

B

) by the formula

X δ Y

⇔↑

Y

u

αX

6

=

.

That

¬

(

I δ

) and

¬

(

δ I

) is obvious. We have

I

t

J δ K

K

u

α

(

I

t

J

)

6

=

⊥ ⇔

K

u

(

αI

t

αJ

)

6

=

⊥ ⇔

K

u

αI

6

=

⊥∨ ↑

K

u

αJ

6

=

⊥ ⇔

I δ K

J δ K

and

K δ I

t

J

(

I

t

J

)

u

αK

6

=

⊥ ⇔

(

I

t ↑

J

)

u

αK

6

=

⊥ ⇔

I

u

αK

6

=

⊥∨ ↑

J

u

αK

6

=

⊥ ⇔

K δ I

K δ J.

That is the formulas (

7

are true.

Accordingly to the above there exists a funcoid

f

such that

X

[

f

]

Y ⇔ ∀

X

up

X

, Y

up

Y

:

X δ Y.

For every

X

T

A

,

Y

T

B

we have:

Y

u h

f

i ↑

X

6

=

⊥ ⇔↑

X

[

f

]

Y

X δ Y

⇔↑

Y

u

αX

6

=

,

consequently

X

T

A

:

αX

=

h

f

i ↑

X

=

h

f

i

X

.

Note that by the last theorem to every (quasi-)proximity

δ

corresponds a unique

funcoid. So funcoids are a generalization of (quasi-)proximity structures. Reverse

funcoids can be considered as a generalization of conjugate quasi-proximity.

Corollary

829

.

If

α

F

(

B

)

T

A

,

β

F

(

A

)

T

B

are functions such that

Y

6

αX

X

6

βY

for every

X

T

A

,

Y

T

B

, then there exists exactly one

funcoid

f

such that

h

f

i

=

α

,

h

f

1

i

=

β

.

Proof.

Prove

α

(

I

t

J

) =

αI

t

αJ

. Really,

Y

6

α

(

I

t

J

)

I

t

J

6

βY

I

6

βY

J

6

βY

Y

6

αI

Y

6

αJ

Y

6

αI

t

αJ

. So

α

(

I

t

J

) =

αI

t

αJ

by star-separability. Similarly

β

(

I

t

J

) =

βI

t

βJ

.

Thus by the theorem there exists a funcoid

f

such that

h

f

i

=

α

,

h

f

1

i

=

β

.

That this funcoid is unique, follows from the above.

Definition

830

.

Any

Rel

-morphism

F

:

A

B

corresponds to a funcoid

FCD

F

FCD

(

A, B

), where by definition

FCD

F

X

=

d

F

h

F

i

up

X

for every

X ∈

F

(

A

).