Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-hlim Structured version   Visualization version   GIF version

Definition df-hlim 27717
 Description: Define the limit relation for Hilbert space. See hlimi 27933 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
StepHypRef Expression
1 chli 27672 . 2 class 𝑣
2 cn 10980 . . . . . 6 class
3 chil 27664 . . . . . 6 class
4 vf . . . . . . 7 setvar 𝑓
54cv 1479 . . . . . 6 class 𝑓
62, 3, 5wf 5853 . . . . 5 wff 𝑓:ℕ⟶ ℋ
7 vw . . . . . . 7 setvar 𝑤
87cv 1479 . . . . . 6 class 𝑤
98, 3wcel 1987 . . . . 5 wff 𝑤 ∈ ℋ
106, 9wa 384 . . . 4 wff (𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ)
11 vz . . . . . . . . . . . 12 setvar 𝑧
1211cv 1479 . . . . . . . . . . 11 class 𝑧
1312, 5cfv 5857 . . . . . . . . . 10 class (𝑓𝑧)
14 cmv 27670 . . . . . . . . . 10 class
1513, 8, 14co 6615 . . . . . . . . 9 class ((𝑓𝑧) − 𝑤)
16 cno 27668 . . . . . . . . 9 class norm
1715, 16cfv 5857 . . . . . . . 8 class (norm‘((𝑓𝑧) − 𝑤))
18 vx . . . . . . . . 9 setvar 𝑥
1918cv 1479 . . . . . . . 8 class 𝑥
20 clt 10034 . . . . . . . 8 class <
2117, 19, 20wbr 4623 . . . . . . 7 wff (norm‘((𝑓𝑧) − 𝑤)) < 𝑥
22 vy . . . . . . . . 9 setvar 𝑦
2322cv 1479 . . . . . . . 8 class 𝑦
24 cuz 11647 . . . . . . . 8 class
2523, 24cfv 5857 . . . . . . 7 class (ℤ𝑦)
2621, 11, 25wral 2908 . . . . . 6 wff 𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥
2726, 22, 2wrex 2909 . . . . 5 wff 𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥
28 crp 11792 . . . . 5 class +
2927, 18, 28wral 2908 . . . 4 wff 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥
3010, 29wa 384 . . 3 wff ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥)
3130, 4, 7copab 4682 . 2 class {⟨𝑓, 𝑤⟩ ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥)}
321, 31wceq 1480 1 wff 𝑣 = {⟨𝑓, 𝑤⟩ ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥)}
 Colors of variables: wff setvar class This definition is referenced by:  h2hlm  27725  hlimi  27933
 Copyright terms: Public domain W3C validator