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

Definition df-hcau 27003
Description: Define the set of Cauchy sequences on a Hilbert space. See hcau 27214 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 26956 . 2 class Cauchy
2 vy . . . . . . . . . . 11 setvar 𝑦
32cv 1473 . . . . . . . . . 10 class 𝑦
4 vf . . . . . . . . . . 11 setvar 𝑓
54cv 1473 . . . . . . . . . 10 class 𝑓
63, 5cfv 5689 . . . . . . . . 9 class (𝑓𝑦)
7 vz . . . . . . . . . . 11 setvar 𝑧
87cv 1473 . . . . . . . . . 10 class 𝑧
98, 5cfv 5689 . . . . . . . . 9 class (𝑓𝑧)
10 cmv 26955 . . . . . . . . 9 class
116, 9, 10co 6425 . . . . . . . 8 class ((𝑓𝑦) − (𝑓𝑧))
12 cno 26953 . . . . . . . 8 class norm
1311, 12cfv 5689 . . . . . . 7 class (norm‘((𝑓𝑦) − (𝑓𝑧)))
14 vx . . . . . . . 8 setvar 𝑥
1514cv 1473 . . . . . . 7 class 𝑥
16 clt 9828 . . . . . . 7 class <
1713, 15, 16wbr 4481 . . . . . 6 wff (norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
18 cuz 11426 . . . . . . 7 class
193, 18cfv 5689 . . . . . 6 class (ℤ𝑦)
2017, 7, 19wral 2800 . . . . 5 wff 𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
21 cn 10774 . . . . 5 class
2220, 2, 21wrex 2801 . . . 4 wff 𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
23 crp 11573 . . . 4 class +
2422, 14, 23wral 2800 . . 3 wff 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥
25 chil 26949 . . . 4 class
26 cmap 7619 . . . 4 class 𝑚
2725, 21, 26co 6425 . . 3 class ( ℋ ↑𝑚 ℕ)
2824, 4, 27crab 2804 . 2 class {𝑓 ∈ ( ℋ ↑𝑚 ℕ) ∣ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥}
291, 28wceq 1474 1 wff Cauchy = {𝑓 ∈ ( ℋ ↑𝑚 ℕ) ∣ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑦) − (𝑓𝑧))) < 𝑥}
Colors of variables: wff setvar class
This definition is referenced by:  h2hcau  27009  hcau  27214
  Copyright terms: Public domain W3C validator