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

Definition df-hcau 27718
 Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 27929 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
StepHypRef Expression
1 ccau 27671 . 2 class Cauchy
2 vy . . . . . . . . . . 11 setvar 𝑦
32cv 1479 . . . . . . . . . 10 class 𝑦
4 vf . . . . . . . . . . 11 setvar 𝑓
54cv 1479 . . . . . . . . . 10 class 𝑓
63, 5cfv 5857 . . . . . . . . 9 class (𝑓𝑦)
7 vz . . . . . . . . . . 11 setvar 𝑧
87cv 1479 . . . . . . . . . 10 class 𝑧
98, 5cfv 5857 . . . . . . . . 9 class (𝑓𝑧)
10 cmv 27670 . . . . . . . . 9 class
116, 9, 10co 6615 . . . . . . . 8 class ((𝑓𝑦) − (𝑓𝑧))
12 cno 27668 . . . . . . . 8 class norm
1311, 12cfv 5857 . . . . . . 7 class (norm‘((𝑓𝑦) − (𝑓𝑧)))
14 vx . . . . . . . 8 setvar 𝑥
1514cv 1479 . . . . . . 7 class 𝑥
16 clt 10034 . . . . . . 7 class <
1713, 15, 16wbr 4623 . . . . . 6 wff (norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
18 cuz 11647 . . . . . . 7 class
193, 18cfv 5857 . . . . . 6 class (ℤ𝑦)
2017, 7, 19wral 2908 . . . . 5 wff 𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
21 cn 10980 . . . . 5 class
2220, 2, 21wrex 2909 . . . 4 wff 𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
23 crp 11792 . . . 4 class +
2422, 14, 23wral 2908 . . 3 wff 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
25 chil 27664 . . . 4 class
26 cmap 7817 . . . 4 class 𝑚
2725, 21, 26co 6615 . . 3 class ( ℋ ↑𝑚 ℕ)
2824, 4, 27crab 2912 . 2 class {𝑓 ∈ ( ℋ ↑𝑚 ℕ) ∣ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥}
291, 28wceq 1480 1 wff Cauchy = {𝑓 ∈ ( ℋ ↑𝑚 ℕ) ∣ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥}
 Colors of variables: wff setvar class This definition is referenced by:  h2hcau  27724  hcau  27929
 Copyright terms: Public domain W3C validator