Description: Two ways to express that a function has a limit. (The expression ( ~>F ) is sometimes useful as a shorthand for "the unique limit of the function F "). (Contributed by Mario Carneiro, 18-Mar-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | climdm | |- ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fclim | |- ~~> : dom ~~> --> CC |
|
| 2 | ffun | |- ( ~~> : dom ~~> --> CC -> Fun ~~> ) |
|
| 3 | funfvbrb | |- ( Fun ~~> -> ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) ) ) |
|
| 4 | 1 2 3 | mp2b | |- ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) ) |