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

Definition df-hlim 27002
Description: Define the limit relation for Hilbert space. See hlimi 27218 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 26957 . 2 class 𝑣
2 cn 10774 . . . . . 6 class
3 chil 26949 . . . . . 6 class
4 vf . . . . . . 7 setvar 𝑓
54cv 1473 . . . . . 6 class 𝑓
62, 3, 5wf 5685 . . . . 5 wff 𝑓:ℕ⟶ ℋ
7 vw . . . . . . 7 setvar 𝑤
87cv 1473 . . . . . 6 class 𝑤
98, 3wcel 1938 . . . . 5 wff 𝑤 ∈ ℋ
106, 9wa 382 . . . 4 wff (𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ)
11 vz . . . . . . . . . . . 12 setvar 𝑧
1211cv 1473 . . . . . . . . . . 11 class 𝑧
1312, 5cfv 5689 . . . . . . . . . 10 class (𝑓𝑧)
14 cmv 26955 . . . . . . . . . 10 class
1513, 8, 14co 6425 . . . . . . . . 9 class ((𝑓𝑧) − 𝑤)
16 cno 26953 . . . . . . . . 9 class norm
1715, 16cfv 5689 . . . . . . . 8 class (norm‘((𝑓𝑧) − 𝑤))
18 vx . . . . . . . . 9 setvar 𝑥
1918cv 1473 . . . . . . . 8 class 𝑥
20 clt 9828 . . . . . . . 8 class <
2117, 19, 20wbr 4481 . . . . . . 7 wff (norm‘((𝑓𝑧) − 𝑤)) < 𝑥
22 vy . . . . . . . . 9 setvar 𝑦
2322cv 1473 . . . . . . . 8 class 𝑦
24 cuz 11426 . . . . . . . 8 class
2523, 24cfv 5689 . . . . . . 7 class (ℤ𝑦)
2621, 11, 25wral 2800 . . . . . 6 wff 𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥
2726, 22, 2wrex 2801 . . . . 5 wff 𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥
28 crp 11573 . . . . 5 class +
2927, 18, 28wral 2800 . . . 4 wff 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥
3010, 29wa 382 . . 3 wff ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥)
3130, 4, 7copab 4540 . 2 class {⟨𝑓, 𝑤⟩ ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥)}
321, 31wceq 1474 1 wff 𝑣 = {⟨𝑓, 𝑤⟩ ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑤 ∈ ℋ) ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀𝑧 ∈ (ℤ𝑦)(norm‘((𝑓𝑧) − 𝑤)) < 𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  h2hlm  27010  hlimi  27218
  Copyright terms: Public domain W3C validator