18.6. EXPRESSING LIMITS AS IMPLICATIONS

280

im(

ν

f

|

h

µ

i

@

{

x

}

) =

h

ν

ih

f

i

@

{

x

}

;

ν

f

|

h

µ

i

@

{

x

}

v

h

µ

i

@

{

x

} ×

FCD

im(

ν

f

|

h

µ

i

@

{

x

}

) =

h

µ

i

@

{

x

} ×

FCD

h

ν

ih

f

i

@

{

x

}

.

So

ν

f

|

h

µ

i

@

{

x

}

=

h

µ

i

@

{

x

} ×

FCD

h

ν

ih

f

i

@

{

x

}

.

Thus xlim

x

f

=

n

(

h

µ

i

@

{

x

FCD

h

ν

ih

f

i

@

{

x

}

)

◦↑

r

r

G

o

=

τ

(

f x

).

Remark

1479

.

Without the requirement of

h

µ

i

@

{

x

} w↑

Ob

µ

{

x

}

the last

theorem would not work in the case of removable singularity.

Theorem

1480

.

Let

ν

v

ν

ν

. If

f

|

h

µ

i

@

{

x

}

ν

→↑

Ob

µ

{

y

}

then xlim

x

f

=

τ

(

y

).

Proof.

im

f

|

h

µ

i

@

{

x

}

v h

ν

i

@

{

y

}

;

h

f

ih

µ

i

@

{

x

} v h

ν

i

@

{

y

}

;

ν

f

|

h

µ

i

@

{

x

}

w

(

h

ν

i

@

{

y

} ×

FCD

h

ν

i

@

{

y

}

)

f

|

h

µ

i

@

{

x

}

=

(

f

|

h

µ

i

@

{

x

}

)

1

h

ν

i

@

{

y

} ×

FCD

h

ν

i

@

{

y

}

=

D

id

FCD

h

µ

i

{

x

}

f

1

E

h

ν

i

@

{

y

} ×

FCD

h

ν

i

@

{

y

} w

D

id

FCD

h

µ

i

{

x

}

f

1

E

h

f

ih

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

=

D

id

FCD

h

µ

i

{

x

}

E

f

1

f

h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

} w

D

id

FCD

h

µ

i

{

x

}

ED

id

FCD

h

µ

i

{

x

}

E

h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

=

h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

.

On the other hand,

f

|

h

µ

i

@

{

x

}

v h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

;

ν

f

|

h

µ

i

@

{

x

}

v h

µ

i

@

{

x

} ×

FCD

h

ν

ih

ν

i

@

{

y

} v h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

.

So

ν

f

|

h

µ

i

@

{

x

}

=

h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

.

xlim

x

f

=

n

ν

f

|

h

µ

i∗

@

{

x

}

◦↑

r

r

G

o

=

n

(

h

µ

i

@

{

x

FCD

h

ν

i

@

{

y

}

)

◦↑

r

r

G

o

=

τ

(

y

).

Corollary

1481

.

If lim

ν

h

µ

i

@

{

x

}

f

=

y

then xlim

x

f

=

τ

(

y

) (provided that

ν

v

ν

ν

).

We have injective

τ

if

h

ν

i

@

{

y

1

} u h

ν

i

@

{

y

2

}

=

F

(Ob

µ

)

for every distinct

y

1

, y

2

Ob

ν

that is if

ν

is

T

2

-separable.

18.6. Expressing limits as implications

When you studied limits in the school, you was told that lim

x

α

f

(

x

) =

β

when

x

α

implies

f

(

x

)

β

. Now let us formalize this.

Proposition

1482

.

The following are pairwise equivalent for funcoids

µ

,

ν

,

f

of suitable (“compatible”) sources and destinations:

1

.

f

|

h

µ

i

{

α

}

ν

β

;

2

.

x

F

(Ob

µ

) :

x

µ

α

⇒ h

f

i

x

ν

β

;

3

.

x

atoms

F

(Ob

µ

)

:

x

µ

α

⇒ h

f

i

x

ν

β

.

Proof.

1

2

.

x

F

(Ob

µ

) :

x

µ

α

⇒ h

f

i

x

ν

β

⇔ ∀

x

F

(Ob

µ

) : (

x

v h

µ

i

α

h

f

i

x

v h

ν

i

β

)

⇔ h

f

ih

µ

i

α

v h

ν

i

β

f

|

h

µ

i

{

α

}

ν

β

.