Description: The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | climfvd.1 | |- ( ph -> F ~~> A ) |
|
| Assertion | climfvd | |- ( ph -> A = ( ~~> ` F ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | climfvd.1 | |- ( ph -> F ~~> A ) |
|
| 2 | climfv | |- ( F ~~> A -> A = ( ~~> ` F ) ) |
|
| 3 | 1 2 | syl | |- ( ph -> A = ( ~~> ` F ) ) |