Definition df-hcau 28744

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 28955 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 28697	. 2 class Cauchy
2		vy	. . . . . . . . . . 11 setvar 𝑦
3	2	cv 1532	. . . . . . . . . 10 class 𝑦
4		vf	. . . . . . . . . . 11 setvar 𝑓
5	4	cv 1532	. . . . . . . . . 10 class 𝑓
6	3, 5	cfv 6349	. . . . . . . . 9 class (𝑓‘𝑦)
7		vz	. . . . . . . . . . 11 setvar 𝑧
8	7	cv 1532	. . . . . . . . . 10 class 𝑧
9	8, 5	cfv 6349	. . . . . . . . 9 class (𝑓‘𝑧)
10		cmv 28696	. . . . . . . . 9 class −ℎ
11	6, 9, 10	co 7150	. . . . . . . 8 class ((𝑓‘𝑦) −ℎ (𝑓‘𝑧))
12		cno 28694	. . . . . . . 8 class normℎ
13	11, 12	cfv 6349	. . . . . . 7 class (normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧)))
14		vx	. . . . . . . 8 setvar 𝑥
15	14	cv 1532	. . . . . . 7 class 𝑥
16		clt 10669	. . . . . . 7 class <
17	13, 15, 16	wbr 5058	. . . . . 6 wff (normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
18		cuz 12237	. . . . . . 7 class ℤ≥
19	3, 18	cfv 6349	. . . . . 6 class (ℤ≥‘𝑦)
20	17, 7, 19	wral 3138	. . . . 5 wff ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
21		cn 11632	. . . . 5 class ℕ
22	20, 2, 21	wrex 3139	. . . 4 wff ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
23		crp 12383	. . . 4 class ℝ+
24	22, 14, 23	wral 3138	. . 3 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
25		chba 28690	. . . 4 class ℋ
26		cmap 8400	. . . 4 class ↑m
27	25, 21, 26	co 7150	. . 3 class ( ℋ ↑m ℕ)
28	24, 4, 27	crab 3142	. 2 class {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}
29	1, 28	wceq 1533	1 wff Cauchy = {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}

This definition is referenced by:  h2hcau  28750  hcau  28955