Definition df-hcau 31605

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 31816 for its membership relation. Note that 𝑓:ℕ⟶ ℋ 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.)

Assertion

Ref	Expression
df-hcau	⊢ Cauchy = {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}

Distinct variable group:   𝑥,𝑦,𝑧,𝑓

Detailed syntax breakdown of Definition df-hcau

Step	Hyp	Ref	Expression
1		ccauold 31558	. 2 class Cauchy
2		vy	. . . . . . . . . . 11 setvar 𝑦
3	2	cv 1569	. . . . . . . . . 10 class 𝑦
4		vf	. . . . . . . . . . 11 setvar 𝑓
5	4	cv 1569	. . . . . . . . . 10 class 𝑓
6	3, 5	cfv 6558	. . . . . . . . 9 class (𝑓‘𝑦)
7		vz	. . . . . . . . . . 11 setvar 𝑧
8	7	cv 1569	. . . . . . . . . 10 class 𝑧
9	8, 5	cfv 6558	. . . . . . . . 9 class (𝑓‘𝑧)
10		cmv 31557	. . . . . . . . 9 class −ℎ
11	6, 9, 10	co 7443	. . . . . . . 8 class ((𝑓‘𝑦) −ℎ (𝑓‘𝑧))
12		cno 31555	. . . . . . . 8 class normℎ
13	11, 12	cfv 6558	. . . . . . 7 class (normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧)))
14		vx	. . . . . . . 8 setvar 𝑥
15	14	cv 1569	. . . . . . 7 class 𝑥
16		clt 11370	. . . . . . 7 class <
17	13, 15, 16	wbr 5106	. . . . . 6 wff (normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
18		cuz 12992	. . . . . . 7 class ℤ≥
19	3, 18	cfv 6558	. . . . . 6 class (ℤ≥‘𝑦)
20	17, 7, 19	wral 3080	. . . . 5 wff ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
21		cn 12362	. . . . 5 class ℕ
22	20, 2, 21	wrex 3090	. . . 4 wff ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
23		crp 13147	. . . 4 class ℝ+
24	22, 14, 23	wral 3080	. . 3 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
25		chba 31551	. . . 4 class ℋ
26		cmap 8875	. . . 4 class ↑m
27	25, 21, 26	co 7443	. . 3 class ( ℋ ↑m ℕ)
28	24, 4, 27	crab 3416	. 2 class {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}
29	1, 28	wceq 1570	1 wff Cauchy = {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}

This definition is used by:  h2hcau  31611  hcau  31816