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({\mathscr{H}}^{\mathbb{N}}\right)|\forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{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	$$setvarf$$
2		chba	$$class\mathscr{H}$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4		cn	$$class\mathbb{N}$$
5	2 4 3	co	$$class\left({\mathscr{H}}^{\mathbb{N}}\right)$$
6		vx	$$setvarx$$
7		crp	$$class{ℝ}^{+}$$
8		vy	$$setvary$$
9		vz	$$setvarz$$
10		cuz	$$class{\mathbb{Z}}_{\ge }$$
11	8	cv	$$setvary$$
12	11 10	cfv	$$class{\mathbb{Z}}_{\ge y}$$
13		cno	$$class{norm}_{ℎ}$$
14	1	cv	$$setvarf$$
15	11 14	cfv	$$classf\left(y\right)$$
16		cmv	$$class{-}_{ℎ}$$
17	9	cv	$$setvarz$$
18	17 14	cfv	$$classf\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	$$setvarx$$
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 {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(f\left(y\right){-}_{ℎ}f\left(z\right)\right)<x$$
25	24 8 4	wrex	$$wff\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(f\left(y\right){-}_{ℎ}f\left(z\right)\right)<x$$
26	25 6 7	wral	$$wff\forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(f\left(y\right){-}_{ℎ}f\left(z\right)\right)<x$$
27	26 1 5	crab	$$class\left\{f\in \left({\mathscr{H}}^{\mathbb{N}}\right)|\forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(f\left(y\right){-}_{ℎ}f\left(z\right)\right)<x\right\}$$
28	0 27	wceq	$$wff\mathrm{Cauchy}=\left\{f\in \left({\mathscr{H}}^{\mathbb{N}}\right)|\forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(f\left(y\right){-}_{ℎ}f\left(z\right)\right)<x\right\}$$