Definition df-hlim 8780

Description: Define the limit relation for Hilbert space. See hlim 8977 for its relational expression. Note that f:ℕ–→ ℋ is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of converge in [Beran] p. 96.

Assertion

Ref	Expression
df-hlim	⊢ ⇝v = {⟨f, w⟩∣((f:ℕ–→ ℋ ⋀ w ∈ ℋ ) ⋀ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (normh ‘((f ‘z) −h w)) < x)))}

Distinct variable group:   x,y,z,f,w

Detailed syntax breakdown of Definition df-hlim

Step	Hyp	Ref	Expression
1		chli 8735	. 2 class ⇝v
2		cn 5268	. . . . . 6 class ℕ
3		chil 8727	. . . . . 6 class ℋ
4		vf	. . . . . . 7 set f
5	4	cv 952	. . . . . 6 class f
6	2, 3, 5	wf 3168	. . . . 5 wff f:ℕ–→ ℋ
7		vw	. . . . . . 7 set w
8	7	cv 952	. . . . . 6 class w
9	8, 3	wcel 955	. . . . 5 wff w ∈ ℋ
10	6, 9	wa 223	. . . 4 wff (f:ℕ–→ ℋ ⋀ w ∈ ℋ )
11		cc0 5206	. . . . . . 7 class 0
12		vx	. . . . . . . 8 set x
13	12	cv 952	. . . . . . 7 class x
14		clt 5458	. . . . . . 7 class <
15	11, 13, 14	wbr 2609	. . . . . 6 wff 0 < x
16		vy	. . . . . . . . . . 11 set y
17	16	cv 952	. . . . . . . . . 10 class y
18		vz	. . . . . . . . . . 11 set z
19	18	cv 952	. . . . . . . . . 10 class z
20		cle 5267	. . . . . . . . . 10 class ≤
21	17, 19, 20	wbr 2609	. . . . . . . . 9 wff y ≤ z
22	19, 5	cfv 3172	. . . . . . . . . . . 12 class (f ‘z)
23		cmv 8731	. . . . . . . . . . . 12 class −h
24	22, 8, 23	co 3948	. . . . . . . . . . 11 class ((f ‘z) −h w)
25		cno 8733	. . . . . . . . . . 11 class normh
26	24, 25	cfv 3172	. . . . . . . . . 10 class (normh ‘((f ‘z) −h w))
27	26, 13, 14	wbr 2609	. . . . . . . . 9 wff (normh ‘((f ‘z) −h w)) < x
28	21, 27	wi 3	. . . . . . . 8 wff (y ≤ z → (normh ‘((f ‘z) −h w)) < x)
29	28, 18, 2	wral 1637	. . . . . . 7 wff ∀z ∈ ℕ (y ≤ z → (normh ‘((f ‘z) −h w)) < x)
30	29, 16, 2	wrex 1638	. . . . . 6 wff ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (normh ‘((f ‘z) −h w)) < x)
31	15, 30	wi 3	. . . . 5 wff (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (normh ‘((f ‘z) −h w)) < x))
32		cr 5205	. . . . 5 class ℝ
33	31, 12, 32	wral 1637	. . . 4 wff ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (normh ‘((f ‘z) −h w)) < x))
34	10, 33	wa 223	. . 3 wff ((f:ℕ–→ ℋ ⋀ w ∈ ℋ ) ⋀ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (normh ‘((f ‘z) −h w)) < x)))
35	34, 4, 7	copab 2656	. 2 class {⟨f, w⟩∣((f:ℕ–→ ℋ ⋀ w ∈ ℋ ) ⋀ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (normh ‘((f ‘z) −h w)) < x)))}
36	1, 35	wceq 953	1 wff ⇝v = {⟨f, w⟩∣((f:ℕ–→ ℋ ⋀ w ∈ ℋ ) ⋀ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (normh ‘((f ‘z) −h w)) < x)))}

This definition is referenced by:  h2hlm 8789  hlim 8977  hlim2 8981

Copyright terms: Public domain