Description: The limit operator can be expressed as a filter limit, from the filter of neighborhoods of B restricted to A \ { B } , to the topology of the complex numbers. (If B is not a limit point of A , then it is still formally a filter limit, but the neighborhood filter is not a proper filter in this case.) (Contributed by Mario Carneiro, 25-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | limcflf.f | |
|
limcflf.a | |
||
limcflf.b | |
||
limcflf.k | |
||
limcflf.c | |
||
limcflf.l | |
||
Assertion | limcflf | |