Definition df-hlim 29235

Description: Define the limit relation for Hilbert space. See hlimi 29451 for its relational expression. Note that 𝑓:ℕ⟶ ℋ 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.)

Assertion

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

Distinct variable group:   𝑥,𝑦,𝑧,𝑓,𝑤

Detailed syntax breakdown of Definition df-hlim

Step	Hyp	Ref	Expression
1		chli 29190	. 2 class ⇝𝑣
2		cn 11903	. . . . . 6 class ℕ
3		chba 29182	. . . . . 6 class ℋ
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1538	. . . . . 6 class 𝑓
6	2, 3, 5	wf 6414	. . . . 5 wff 𝑓:ℕ⟶ ℋ
7		vw	. . . . . . 7 setvar 𝑤
8	7	cv 1538	. . . . . 6 class 𝑤
9	8, 3	wcel 2108	. . . . 5 wff 𝑤 ∈ ℋ
10	6, 9	wa 395	. . . 4 wff (𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ)
11		vz	. . . . . . . . . . . 12 setvar 𝑧
12	11	cv 1538	. . . . . . . . . . 11 class 𝑧
13	12, 5	cfv 6418	. . . . . . . . . 10 class (𝑓‘𝑧)
14		cmv 29188	. . . . . . . . . 10 class −ℎ
15	13, 8, 14	co 7255	. . . . . . . . 9 class ((𝑓‘𝑧) −ℎ 𝑤)
16		cno 29186	. . . . . . . . 9 class normℎ
17	15, 16	cfv 6418	. . . . . . . 8 class (normℎ‘((𝑓‘𝑧) −ℎ 𝑤))
18		vx	. . . . . . . . 9 setvar 𝑥
19	18	cv 1538	. . . . . . . 8 class 𝑥
20		clt 10940	. . . . . . . 8 class <
21	17, 19, 20	wbr 5070	. . . . . . 7 wff (normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥
22		vy	. . . . . . . . 9 setvar 𝑦
23	22	cv 1538	. . . . . . . 8 class 𝑦
24		cuz 12511	. . . . . . . 8 class ℤ≥
25	23, 24	cfv 6418	. . . . . . 7 class (ℤ≥‘𝑦)
26	21, 11, 25	wral 3063	. . . . . 6 wff ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥
27	26, 22, 2	wrex 3064	. . . . 5 wff ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥
28		crp 12659	. . . . 5 class ℝ+
29	27, 18, 28	wral 3063	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥
30	10, 29	wa 395	. . 3 wff ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥)
31	30, 4, 7	copab 5132	. 2 class {⟨𝑓, 𝑤⟩ ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥)}
32	1, 31	wceq 1539	1 wff ⇝𝑣 = {⟨𝑓, 𝑤⟩ ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥)}

This definition is referenced by:  h2hlm  29243  hlimi  29451