Metamath Proof Explorer


Definition df-hcau

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau for its membership relation. Note that f : NN --> ~H 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.)

Ref Expression
Assertion df-hcau Cauchy = { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥 }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccauold Cauchy
1 vf 𝑓
2 chba
3 cmap m
4 cn
5 2 4 3 co ( ℋ ↑m ℕ )
6 vx 𝑥
7 crp +
8 vy 𝑦
9 vz 𝑧
10 cuz
11 8 cv 𝑦
12 11 10 cfv ( ℤ𝑦 )
13 cno norm
14 1 cv 𝑓
15 11 14 cfv ( 𝑓𝑦 )
16 cmv
17 9 cv 𝑧
18 17 14 cfv ( 𝑓𝑧 )
19 15 18 16 co ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) )
20 19 13 cfv ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) )
21 clt <
22 6 cv 𝑥
23 20 22 21 wbr ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥
24 23 9 12 wral 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥
25 24 8 4 wrex 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥
26 25 6 7 wral 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥
27 26 1 5 crab { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥 }
28 0 27 wceq Cauchy = { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑦 ) − ( 𝑓𝑧 ) ) ) < 𝑥 }