background image

7.12. COMPLETE FUNCOIDS

169

Conjecture

905

.

f

u

d

S

=

d

h

f

ui

S

for principal funcoid

f

and a set

S

of

funcoids of appropriate sources and destinations.

Remark

906

.

See also example

1333

below.

The next proposition is one more (among the theorem

852

generalization for

funcoids of composition of relations.

Proposition

907

.

For every composable funcoids

f

,

g

atoms(

g

f

) =

x

×

FCD

z

x

atoms

F

(Src

f

)

, z

atoms

F

(Dst

g

)

,

y

atoms

F

(Dst

f

)

: (

x

×

FCD

y

atoms

f

y

×

FCD

z

atoms

g

)

.

Proof.

Using the theorem

852

,

x

×

FCD

z

6

g

f

x

[

g

f

]

z

⇔ ∃

y

atoms

F

(Dst

f

)

: (

x

×

FCD

y

6

f

y

×

FCD

z

6

g

)

.

Corollary

908

.

g

f

=

d

n

G

F

F

atoms

f,G

atoms

g

o

for every composable funcoids

f

,

g

.

Theorem

909

.

Let

f

be a funcoid.

1

.

X

[

f

]

Y ⇔ ∃

F

atoms

f

:

X

[

F

]

Y

for every

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

);

2

.

h

f

iX

=

d

F

atoms

f

h

F

iX

for every

X ∈

F

(Src

f

).

Proof.

1

.

F

atoms

f

:

X

[

F

]

Y ⇔

a

atoms

F

(Src

f

)

, b

atoms

F

(Dst

f

)

: (

a

×

FCD

b

6

f

∧ X

a

×

FCD

b

Y

)

a

atoms

F

(Src

f

)

, b

atoms

F

(Dst

f

)

: (

a

×

FCD

b

6

f

a

×

FCD

b

6 X ×

FCD

Y

)

F

atoms

f

: (

F

6

f

F

6 X ×

FCD

Y

)

f

6 X ×

FCD

Y ⇔

X

[

f

]

Y

.

2

Let

Y ∈

F

(Dst

f

). Suppose

Y 6 h

f

iX

. Then

X

[

f

]

Y

;

F

atoms

f

:

X

[

F

]

Y

;

F

atoms

f

:

Y 6 h

F

iX

;

Y 6

d

F

atoms

f

h

F

iX

. So

h

f

iX v

d

F

atoms

f

h

F

iX

. The contrary

h

f

iX w

d

F

atoms

f

h

F

iX

is obvious.

7.12. Complete funcoids

Definition

910

.

I will call

co-complete

such a funcoid

f

that

h

f

i

X

is a

principal filter for every

X

T

(Src

f

).

Obvious

911

.

Funcoid

f

is co-complete iff

h

f

iX ∈

P

(Dst

f

) for every

X ∈

P

(Src

f

).

Definition

912

.

I will call

generalized closure

such a function

α

(

T

B

)

T

A

(for some sets

A

,

B

) that