Definition df-hlim 27213

Description: Define the limit relation for Hilbert space. See hlimi 27429 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 27168	. 2 class ⇝𝑣
2		cn 10897	. . . . . 6 class ℕ
3		chil 27160	. . . . . 6 class ℋ
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1474	. . . . . 6 class 𝑓
6	2, 3, 5	wf 5800	. . . . 5 wff 𝑓:ℕ⟶ ℋ
7		vw	. . . . . . 7 setvar 𝑤
8	7	cv 1474	. . . . . 6 class 𝑤
9	8, 3	wcel 1977	. . . . 5 wff 𝑤 ∈ ℋ
10	6, 9	wa 383	. . . 4 wff (𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ)
11		vz	. . . . . . . . . . . 12 setvar 𝑧
12	11	cv 1474	. . . . . . . . . . 11 class 𝑧
13	12, 5	cfv 5804	. . . . . . . . . 10 class (𝑓‘𝑧)
14		cmv 27166	. . . . . . . . . 10 class −ℎ
15	13, 8, 14	co 6549	. . . . . . . . 9 class ((𝑓‘𝑧) −ℎ 𝑤)
16		cno 27164	. . . . . . . . 9 class normℎ
17	15, 16	cfv 5804	. . . . . . . 8 class (normℎ‘((𝑓‘𝑧) −ℎ 𝑤))
18		vx	. . . . . . . . 9 setvar 𝑥
19	18	cv 1474	. . . . . . . 8 class 𝑥
20		clt 9953	. . . . . . . 8 class <
21	17, 19, 20	wbr 4583	. . . . . . 7 wff (normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥
22		vy	. . . . . . . . 9 setvar 𝑦
23	22	cv 1474	. . . . . . . 8 class 𝑦
24		cuz 11563	. . . . . . . 8 class ℤ≥
25	23, 24	cfv 5804	. . . . . . 7 class (ℤ≥‘𝑦)
26	21, 11, 25	wral 2896	. . . . . 6 wff ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥
27	26, 22, 2	wrex 2897	. . . . 5 wff ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥
28		crp 11708	. . . . 5 class ℝ+
29	27, 18, 28	wral 2896	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥
30	10, 29	wa 383	. . 3 wff ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥)
31	30, 4, 7	copab 4642	. 2 class {⟨𝑓, 𝑤⟩ ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥)}
32	1, 31	wceq 1475	1 wff ⇝𝑣 = {⟨𝑓, 𝑤⟩ ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ≥‘𝑦)(normℎ‘((𝑓‘𝑧) −ℎ 𝑤)) < 𝑥)}

This definition is referenced by:  h2hlm  27221  hlimi  27429