Description: A Hilbert space sequence converges to at most one limit. (Contributed by NM, 19-Aug-1999) (Revised by Mario Carneiro, 2-May-2015) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hlimuni | |- ( ( F ~~>v A /\ F ~~>v B ) -> A = B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hlimf | |- ~~>v : dom ~~>v --> ~H |
|
| 2 | ffun | |- ( ~~>v : dom ~~>v --> ~H -> Fun ~~>v ) |
|
| 3 | funbrfv | |- ( Fun ~~>v -> ( F ~~>v A -> ( ~~>v ` F ) = A ) ) |
|
| 4 | 1 2 3 | mp2b | |- ( F ~~>v A -> ( ~~>v ` F ) = A ) |
| 5 | funbrfv | |- ( Fun ~~>v -> ( F ~~>v B -> ( ~~>v ` F ) = B ) ) |
|
| 6 | 1 2 5 | mp2b | |- ( F ~~>v B -> ( ~~>v ` F ) = B ) |
| 7 | 4 6 | sylan9req | |- ( ( F ~~>v A /\ F ~~>v B ) -> A = B ) |