Metamath Proof Explorer


Definition df-hlim

Description: Define the limit relation for Hilbert space. See hlimi for its relational expression. Note that f : NN --> ~H is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of converge in Beran p. 96. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

Ref Expression
Assertion df-hlim 𝑣 = { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑧 ) − 𝑤 ) ) < 𝑥 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 chli 𝑣
1 vf 𝑓
2 vw 𝑤
3 1 cv 𝑓
4 cn
5 chba
6 4 5 3 wf 𝑓 : ℕ ⟶ ℋ
7 2 cv 𝑤
8 7 5 wcel 𝑤 ∈ ℋ
9 6 8 wa ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ )
10 vx 𝑥
11 crp +
12 vy 𝑦
13 vz 𝑧
14 cuz
15 12 cv 𝑦
16 15 14 cfv ( ℤ𝑦 )
17 cno norm
18 13 cv 𝑧
19 18 3 cfv ( 𝑓𝑧 )
20 cmv
21 19 7 20 co ( ( 𝑓𝑧 ) − 𝑤 )
22 21 17 cfv ( norm ‘ ( ( 𝑓𝑧 ) − 𝑤 ) )
23 clt <
24 10 cv 𝑥
25 22 24 23 wbr ( norm ‘ ( ( 𝑓𝑧 ) − 𝑤 ) ) < 𝑥
26 25 13 16 wral 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑧 ) − 𝑤 ) ) < 𝑥
27 26 12 4 wrex 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑧 ) − 𝑤 ) ) < 𝑥
28 27 10 11 wral 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑧 ) − 𝑤 ) ) < 𝑥
29 9 28 wa ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑧 ) − 𝑤 ) ) < 𝑥 )
30 29 1 2 copab { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑧 ) − 𝑤 ) ) < 𝑥 ) }
31 0 30 wceq 𝑣 = { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝑓𝑧 ) − 𝑤 ) ) < 𝑥 ) }