Description: Express the property " F is a Cauchy sequence of metric D ". Part of Definition 1.4-3 of Kreyszig p. 28. The condition F C_ ( CC X. X ) allows to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | iscau | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caufval | |
|
2 | 1 | eleq2d | |
3 | reseq1 | |
|
4 | eqidd | |
|
5 | fveq1 | |
|
6 | 5 | oveq1d | |
7 | 3 4 6 | feq123d | |
8 | 7 | rexbidv | |
9 | 8 | ralbidv | |
10 | 9 | elrab | |
11 | 2 10 | bitrdi | |