Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-hcau Structured version   Visualization version   GIF version

Definition df-hcau 28855
 Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 29066 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
StepHypRef Expression
1 ccauold 28808 . 2 class Cauchy
2 vy . . . . . . . . . . 11 setvar 𝑦
32cv 1537 . . . . . . . . . 10 class 𝑦
4 vf . . . . . . . . . . 11 setvar 𝑓
54cv 1537 . . . . . . . . . 10 class 𝑓
63, 5cfv 6335 . . . . . . . . 9 class (𝑓𝑦)
7 vz . . . . . . . . . . 11 setvar 𝑧
87cv 1537 . . . . . . . . . 10 class 𝑧
98, 5cfv 6335 . . . . . . . . 9 class (𝑓𝑧)
10 cmv 28807 . . . . . . . . 9 class
116, 9, 10co 7150 . . . . . . . 8 class ((𝑓𝑦) − (𝑓𝑧))
12 cno 28805 . . . . . . . 8 class norm
1311, 12cfv 6335 . . . . . . 7 class (norm‘((𝑓𝑦) − (𝑓𝑧)))
14 vx . . . . . . . 8 setvar 𝑥
1514cv 1537 . . . . . . 7 class 𝑥
16 clt 10713 . . . . . . 7 class <
1713, 15, 16wbr 5032 . . . . . 6 wff (norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
18 cuz 12282 . . . . . . 7 class
193, 18cfv 6335 . . . . . 6 class (ℤ𝑦)
2017, 7, 19wral 3070 . . . . 5 wff 𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
21 cn 11674 . . . . 5 class
2220, 2, 21wrex 3071 . . . 4 wff 𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
23 crp 12430 . . . 4 class +
2422, 14, 23wral 3070 . . 3 wff 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
25 chba 28801 . . . 4 class
26 cmap 8416 . . . 4 class m
2725, 21, 26co 7150 . . 3 class ( ℋ ↑m ℕ)
2824, 4, 27crab 3074 . 2 class {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥}
291, 28wceq 1538 1 wff Cauchy = {𝑓 ∈ ( ℋ ↑m ℕ) ∣ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥}
 Colors of variables: wff setvar class This definition is referenced by:  h2hcau  28861  hcau  29066
 Copyright terms: Public domain W3C validator