Definition df-hcau 29335

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 29546 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 29288	. 2 class Cauchy
2		vy	. . . . . . . . . . 11 setvar 𝑦
3	2	cv 1538	. . . . . . . . . 10 class 𝑦
4		vf	. . . . . . . . . . 11 setvar 𝑓
5	4	cv 1538	. . . . . . . . . 10 class 𝑓
6	3, 5	cfv 6433	. . . . . . . . 9 class (𝑓‘𝑦)
7		vz	. . . . . . . . . . 11 setvar 𝑧
8	7	cv 1538	. . . . . . . . . 10 class 𝑧
9	8, 5	cfv 6433	. . . . . . . . 9 class (𝑓‘𝑧)
10		cmv 29287	. . . . . . . . 9 class −ℎ
11	6, 9, 10	co 7275	. . . . . . . 8 class ((𝑓‘𝑦) −ℎ (𝑓‘𝑧))
12		cno 29285	. . . . . . . 8 class normℎ
13	11, 12	cfv 6433	. . . . . . 7 class (normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧)))
14		vx	. . . . . . . 8 setvar 𝑥
15	14	cv 1538	. . . . . . 7 class 𝑥
16		clt 11009	. . . . . . 7 class <
17	13, 15, 16	wbr 5074	. . . . . 6 wff (normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
18		cuz 12582	. . . . . . 7 class ℤ≥
19	3, 18	cfv 6433	. . . . . 6 class (ℤ≥‘𝑦)
20	17, 7, 19	wral 3064	. . . . 5 wff ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
21		cn 11973	. . . . 5 class ℕ
22	20, 2, 21	wrex 3065	. . . 4 wff ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
23		crp 12730	. . . 4 class ℝ+
24	22, 14, 23	wral 3064	. . 3 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥
25		chba 29281	. . . 4 class ℋ
26		cmap 8615	. . . 4 class ↑m
27	25, 21, 26	co 7275	. . 3 class ( ℋ ↑m ℕ)
28	24, 4, 27	crab 3068	. 2 class {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}
29	1, 28	wceq 1539	1 wff Cauchy = {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑦) −ℎ (𝑓‘𝑧))) < 𝑥}

This definition is referenced by:  h2hcau  29341  hcau  29546