命題
X をフィルター(過去スレ006の75) Φ のついた集合とする。
f を X から R~ = [-∞, +∞] への写像とする。

lim f が存在するためには
lim.sup f = lim.inf f となることが必要十分である。

このとき、
lim f = lim.sup f = lim.inf f である。

証明
過去スレ007の36より、R の一点でない閉区間 [a, b] は R~ と
位相同型である。
よって、R~ はコンパクトだから >>320 より
lim f が存在するためには、f が Φ に関する接触点(>>318)を
ただ一つ持つことが必要十分である。

このとき、lim f は f の Φ に関する接触点である。

>>321 より、これは lim.sup f = lim.inf f と同値である。
証明終