 18.6. EXPRESSING LIMITS AS IMPLICATIONS

281

2

3

Obvious.

3

2

Let

3

hold. Then for

x

F

(Ob

µ

) we have

x

µ

α

x

v h

µ

i

α

⇔ ∀

x

0

atoms

x

:

x

0

v h

µ

i

α

⇔ ∀

x

0

atoms

x

:

x

0

µ

α

⇒ ∀

x

0

atoms

x

:

h

f

i

x

0

ν

β

⇔ ∀

x

0

atoms

x

:

h

f

i

x

0

v h

ν

i

β

d

x

0

atoms

x

h

f

i

x

0

v h

ν

i

β

⇔ h

f

i

x

v

h

ν

i

β

⇔ h

f

i

x

ν

β

.

Lemma

1483

.

If

f

is an enterely defined monovalued funcoid and

x

is an ul-

trafilter,

y

is a filter, then

h

f

i

x

v

y

x

v h

f

1

i

y

.

Proof.

h

f

i

x

is an ultrafilter.

h

f

i

x

v

y

⇔ h

f

i

x

6

y

x

6 h

f

1

i

y

x

v

h

f

1

i

y

.

Proposition

1484

.

The following are pairwise equivalent for funcoids

µ

,

ν

,

f

,

g

of suitable (“compatible”) sources and destinations provided that

g

is entirely

defined and monovalued:

1

. (

f

g

1

)

|

h

µ

i

{

α

}

ν

β

;

2

.

x

F

(Ob

µ

) :

h

g

i

x

µ

α

⇒ h

f

i

x

ν

β

;

3

.

x

atoms

F

(Ob

µ

)

:

h

g

i

x

µ

α

⇒ h

f

i

x

ν

β

.

Proof.

1

3

Equivalently transforming: (

f

g

1

)

|

h

µ

i

{

α

}

ν

β

;

h

f

ih

g

1

i

h

µ

i

{

α

} v

h

ν

i

{

β

}

; for every

x

atoms

F

(Ob

µ

)

we have

x

v h

g

1

ih

µ

i

{

α

} ⇒ h

f

i

x

v

h

ν

i

{

β

}

; what by the lemma is equivalent to

h

g

i

x

v h

µ

i

{

α

} ⇒ h

f

i

x

v

h

ν

i

{

β

}

that is

h

g

i

x

µ

α

⇒ h

f

i

x

ν

β

.

3

2

Let

x

F

(Ob

µ

) and

3

holds. Let

h

g

i

x

µ

α

. Then

x

0

atoms

x

:

h

g

i

x

0

µ

α

and thus

h

f

i

x

0

ν

β

that is

h

f

i

x

0

v h

ν

i

β

.

h

f

i

x

=

d

x

0

atoms

x

h

f

i

x

0

v h

ν

i

β

that is

h

f

i

x

ν

β

.

Problem

1485

.

Can the theorem be strenhtened for: a. non-monovalued; b.

not entirely defined

g

? (The problem seems easy but I have not checked it.)