Definition df-cauchy 5102

Description: Define the set of Cauchy sequences on a Hilbert space. See hcauchy 5103 for its membership relation. Note that f:ℕ–→ ℋ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in [Beran] p. 96.

Assertion

Ref	Expression
df-cauchy	⊢ Cauchy = {f∣(f:ℕ–→ ℋ ∧ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x)))}

Distinct variable group(s):   x,y,z,w,f

Detailed syntax breakdown of Definition df-cauchy

Step	Hyp	Ref	Expression
1		ccau 4965	. 2 class Cauchy
2		cn 4093	. . . . 5 class ℕ
3		chil 4958	. . . . 5 class ℋ
4		vf	. . . . . 6 set f
5	4	cv 1089	. . . . 5 class f
6	2, 3, 5	wf 2418	. . . 4 wff f:ℕ–→ ℋ
7		cc0 4028	. . . . . . 7 class 0
8		vx	. . . . . . . 8 set x
9	8	cv 1089	. . . . . . 7 class x
10		clt 4033	. . . . . . 7 class <
11	7, 9, 10	wbr 2054	. . . . . 6 wff 0 < x
12		vy	. . . . . . . . . . . . 13 set y
13	12	cv 1089	. . . . . . . . . . . 12 class y
14		vz	. . . . . . . . . . . . 13 set z
15	14	cv 1089	. . . . . . . . . . . 12 class z
16		cle 4092	. . . . . . . . . . . 12 class ≤
17	13, 15, 16	wbr 2054	. . . . . . . . . . 11 wff y ≤ z
18		vw	. . . . . . . . . . . . 13 set w
19	18	cv 1089	. . . . . . . . . . . 12 class w
20	13, 19, 16	wbr 2054	. . . . . . . . . . 11 wff y ≤ w
21	17, 20	wa 196	. . . . . . . . . 10 wff (y ≤ z ∧ y ≤ w)
22		cF	. . . . . . . . . . . . . 14 class F
23	15, 22	cfv 2422	. . . . . . . . . . . . 13 class (F ‘z)
24	19, 22	cfv 2422	. . . . . . . . . . . . 13 class (F ‘w)
25		cmv 4962	. . . . . . . . . . . . 13 class −v
26	23, 24, 25	co 3001	. . . . . . . . . . . 12 class ((F ‘z) −v (F ‘w))
27		cno 4964	. . . . . . . . . . . 12 class norm
28	26, 27	cfv 2422	. . . . . . . . . . 11 class (norm ‘((F ‘z) −v (F ‘w)))
29	28, 9, 10	wbr 2054	. . . . . . . . . 10 wff (norm ‘((F ‘z) −v (F ‘w))) < x
30	21, 29	wi 2	. . . . . . . . 9 wff ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x)
31	30, 18, 2	wral 1201	. . . . . . . 8 wff ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x)
32	31, 14, 2	wral 1201	. . . . . . 7 wff ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x)
33	32, 12, 2	wrex 1202	. . . . . 6 wff ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x)
34	11, 33	wi 2	. . . . 5 wff (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x))
35		cr 4027	. . . . 5 class ℝ
36	34, 8, 35	wral 1201	. . . 4 wff ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x))
37	6, 36	wa 196	. . 3 wff (f:ℕ–→ ℋ ∧ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x)))
38	37, 4	cab 1090	. 2 class {f∣(f:ℕ–→ ℋ ∧ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x)))}
39	1, 38	wceq 1091	1 wff Cauchy = {f∣(f:ℕ–→ ℋ ∧ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ ∀w ∈ ℕ ((y ≤ z ∧ y ≤ w) → (norm ‘((F ‘z) −v (F ‘w))) < x)))}

This definition is referenced by:  hcauchy 5103

metamath.org