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 ) |