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ℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) }