# Metamath Proof Explorer

## Definition df-hcau

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau for its membership relation. Note that f : NN --> ~H is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in Beran p. 96. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

Ref Expression
Assertion df-hcau ${⊢}\mathrm{Cauchy}=\left\{{f}\in \left({ℋ}^{ℕ}\right)|\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℤ}_{\ge {y}}\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({f}\left({y}\right){-}_{ℎ}{f}\left({z}\right)\right)<{x}\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccauold ${class}\mathrm{Cauchy}$
1 vf ${setvar}{f}$
2 chba ${class}ℋ$
3 cmap ${class}{↑}_{𝑚}$
4 cn ${class}ℕ$
5 2 4 3 co ${class}\left({ℋ}^{ℕ}\right)$
6 vx ${setvar}{x}$
7 crp ${class}{ℝ}^{+}$
8 vy ${setvar}{y}$
9 vz ${setvar}{z}$
10 cuz ${class}{ℤ}_{\ge }$
11 8 cv ${setvar}{y}$
12 11 10 cfv ${class}{ℤ}_{\ge {y}}$
13 cno ${class}{norm}_{ℎ}$
14 1 cv ${setvar}{f}$
15 11 14 cfv ${class}{f}\left({y}\right)$
16 cmv ${class}{-}_{ℎ}$
17 9 cv ${setvar}{z}$
18 17 14 cfv ${class}{f}\left({z}\right)$
19 15 18 16 co ${class}\left({f}\left({y}\right){-}_{ℎ}{f}\left({z}\right)\right)$
20 19 13 cfv ${class}{norm}_{ℎ}\left({f}\left({y}\right){-}_{ℎ}{f}\left({z}\right)\right)$
21 clt ${class}<$
22 6 cv ${setvar}{x}$
23 20 22 21 wbr ${wff}{norm}_{ℎ}\left({f}\left({y}\right){-}_{ℎ}{f}\left({z}\right)\right)<{x}$
24 23 9 12 wral ${wff}\forall {z}\in {ℤ}_{\ge {y}}\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({f}\left({y}\right){-}_{ℎ}{f}\left({z}\right)\right)<{x}$
25 24 8 4 wrex ${wff}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℤ}_{\ge {y}}\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({f}\left({y}\right){-}_{ℎ}{f}\left({z}\right)\right)<{x}$
26 25 6 7 wral ${wff}\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℤ}_{\ge {y}}\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({f}\left({y}\right){-}_{ℎ}{f}\left({z}\right)\right)<{x}$
27 26 1 5 crab ${class}\left\{{f}\in \left({ℋ}^{ℕ}\right)|\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℤ}_{\ge {y}}\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({f}\left({y}\right){-}_{ℎ}{f}\left({z}\right)\right)<{x}\right\}$
28 0 27 wceq ${wff}\mathrm{Cauchy}=\left\{{f}\in \left({ℋ}^{ℕ}\right)|\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℤ}_{\ge {y}}\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({f}\left({y}\right){-}_{ℎ}{f}\left({z}\right)\right)<{x}\right\}$