18.5. GENERALIZED LIMIT

279

Obvious

1476

.

xlim

x

f

=

n

ν

f

|

h

µ

i∗

@

{

x

}

◦↑

r

r

G

o

.

Remark

1477

.

xlim

x

f

is the same for funcoids

µ

and Compl

µ

.

The function

τ

will define an injection from the set of points of the space

ν

(“numbers”, “points”, or “vectors”) to the set of all (generalized) limits (i.e. values

which xlim

x

f

may take).

Definition

1478

.

τ

(

y

)

def

=

n

h

µ

i

@

{

x

FCD

h

ν

i

@

{

y

}

x

D

o

.

Proposition

1479

.

τ

(

y

) =

n

(

h

µ

i

@

{

x

FCD

h

ν

i

@

{

y

}

)

◦↑

r

r

G

o

for every (fixed)

x

D

.

Proof.

(

h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

)

◦ ↑

r

=

r

1

h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

=

h

µ

i

r

1

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

=

h

µ

i

@

{

r

1

x

} ×

FCD

h

ν

i

@

{

y

} ∈

h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

x

D

.

Reversely

h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

= (

h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

)

◦ ↑

e

where

e

is the identify element of

G

.

Proposition

1480

.

τ

(

y

) = xlim(

h

µ

i

@

{

x

FCD

Base(Ob

ν

)

{

y

}

) (for every

x

).

Informally: Every

τ

(

y

) is a generalized limit of a constant funcoid.

Proof.

xlim(

h

µ

i

@

{

x

FCD

Base(Ob

ν

)

{

y

}

) =

ν

(

h

µ

i

@

{

x

FCD

Base(Ob

ν

)

{

y

}

)

◦ ↑

r

r

G

=

(

h

µ

i

@

{

x

} ×

FCD

h

ν

i

@

{

y

}

)

◦ ↑

r

r

G

=

τ

(

y

)

.

Theorem

1481

.

If

f

is a function and

f

|

h

µ

i

@

{

x

}

C(

µ, ν

) and

h

µ

i

@

{

x

} w↑

Ob

µ

{

x

}

then xlim

x

f

=

τ

(

f x

).

Proof.

f

|

h

µ

i

@

{

x

}

µ

v

ν

f

|

h

µ

i

@

{

x

}

v

ν

f

; thus

h

f

ih

µ

i

@

{

x

} v

h

ν

ih

f

i

@

{

x

}

; consequently we have

ν

w h

ν

ih

f

i

@

{

x

} ×

FCD

h

ν

ih

f

i

@

{

x

} w h

f

ih

µ

i

@

{

x

} ×

FCD

h

ν

ih

f

i

@

{

x

}

.

ν

f

|

h

µ

i

@

{

x

}

w

(

h

f

ih

µ

i

@

{

x

} ×

FCD

h

ν

ih

f

i

@

{

x

}

)

f

|

h

µ

i

@

{

x

}

=

(

f

|

h

µ

i

{

x

}

)

1

h

f

ih

µ

i

@

{

x

} ×

FCD

h

ν

ih

f

i

@

{

x

} w

D

id

FCD

dom

f

|

h

µ

i∗ {

x

}

E

h

µ

i

@

{

x

} ×

FCD

h

ν

ih

f

i

@

{

x

} w

dom

f

|

h

µ

i

@

{

x

}

×

FCD

h

ν

ih

f

i

@

{

x

}

=

h

µ

i

@

{

x

} ×

FCD

h

ν

ih

f

i

@

{

x

}

.