Definition df-hcau 27214

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 27425 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 = {𝑓 ∈ ( ℋ ↑𝑚 ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}

Distinct variable group:   𝑥,𝑦,𝑧,𝑓

Detailed syntax breakdown of Definition df-hcau

Step	Hyp	Ref	Expression
1		ccau 27167	. 2 class Cauchy
2		vy	. . . . . . . . . . 11 setvar 𝑦
3	2	cv 1474	. . . . . . . . . 10 class 𝑦
4		vf	. . . . . . . . . . 11 setvar 𝑓
5	4	cv 1474	. . . . . . . . . 10 class 𝑓
6	3, 5	cfv 5804	. . . . . . . . 9 class (𝑓‘𝑦)
7		vz	. . . . . . . . . . 11 setvar 𝑧
8	7	cv 1474	. . . . . . . . . 10 class 𝑧
9	8, 5	cfv 5804	. . . . . . . . 9 class (𝑓‘𝑧)
10		cmv 27166	. . . . . . . . 9 class −ℎ
11	6, 9, 10	co 6549	. . . . . . . 8 class ((𝑓‘𝑦) −ℎ (𝑓‘𝑧))
12		cno 27164	. . . . . . . 8 class normℎ
13	11, 12	cfv 5804	. . . . . . 7 class (normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧)))
14		vx	. . . . . . . 8 setvar 𝑥
15	14	cv 1474	. . . . . . 7 class 𝑥
16		clt 9953	. . . . . . 7 class <
17	13, 15, 16	wbr 4583	. . . . . 6 wff (normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
18		cuz 11563	. . . . . . 7 class ℤ≥
19	3, 18	cfv 5804	. . . . . 6 class (ℤ≥‘𝑦)
20	17, 7, 19	wral 2896	. . . . 5 wff ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
21		cn 10897	. . . . 5 class ℕ
22	20, 2, 21	wrex 2897	. . . 4 wff ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
23		crp 11708	. . . 4 class ℝ+
24	22, 14, 23	wral 2896	. . 3 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
25		chil 27160	. . . 4 class ℋ
26		cmap 7744	. . . 4 class ↑𝑚
27	25, 21, 26	co 6549	. . 3 class ( ℋ ↑𝑚 ℕ)
28	24, 4, 27	crab 2900	. 2 class {𝑓 ∈ ( ℋ ↑𝑚 ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}
29	1, 28	wceq 1475	1 wff Cauchy = {𝑓 ∈ ( ℋ ↑𝑚 ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}

This definition is referenced by:  h2hcau  27220  hcau  27425