background image

6.13. COMPLETION OF FUNCOIDS

125

Remark

684

.

It is obvious that funcoids

f

and

g

exist.

Proof.

X

[

g

]

Y

U

Y

6 h

g

i ↑

U

X

Y

6

cl(

X

)

y

Y

: ∆(

y

)

6↑

U

X

y

Y

:

h

f

i

{

y

} 6↑

U

X

(proposition

461

and properties of complete funcoids)

h

f

i

Y

6↑

U

X

Y

[

f

]

X.

So

g

=

f

1

.

6.13. Completion of funcoids

Theorem

685

.

Cor

f

= Cor

0

f

for an element

f

of a filtrator of funcoids.

Proof.

By theorems

301

and

675

.

Definition

686

.

Completion

of a funcoid

f

FCD

(

A

;

B

) is the complete

funcoid , Compl

f

FCD

(

A

;

B

) defined by the formula

h

Compl

f

i

{

α

}

=

h

f

i

{

α

}

for

α

Src

f

.

Definition

687

.

Co-completion

of a funcoid

f

is defined by the formula

CoCompl

f

= (Compl

f

1

)

1

.

Obvious

688

.

Compl

f

v

f

and CoCompl

f

v

f

.

Proposition

689

.

The filtrator (

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

)) is filtered.

Proof.

Because the filtrator of funcoids is filtered.

Theorem

690

.

Compl

f

=

Cor

(

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

))

f

=

Cor

0

(

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

))

f

for every funcoid

f

FCD

(

A

;

B

).

Proof.

Cor

(

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

))

f

= Cor

0

(

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

))

f

using

theorem

301

since the filtrator (

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

)) is filtered.

Let

g

up

(

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

))

f

. Then

g

ComplFCD

(

A

;

B

) and

g

w

f

.

Thus

g

= Compl

g

w

Compl

f

.

Thus

g

up

(

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

))

f

:

g

w

Compl

f

.

Let

g

up

(

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

))

f

:

h

v

g

for some

h

ComplFCD

(

A

;

B

).

Then

h

v

d

up

(

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

))

f

=

f

and consequently

h

= Compl

h

v

Compl

f

.

Thus

Compl

f

=

ComplFCD

(

A

;

B

)

l

up

(

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

))

f

= Cor

(

FCD

(

A

;

B

);

ComplFCD

(

A

;

B

))

f.

Theorem

691

.

h

CoCompl

f

i

X

= Cor

h

f

i

X

for every funcoid

f

and set

X

P

(Src

f

).