Metamath Proof Explorer

Definition df-hlim

Description: Define the limit relation for Hilbert space. See hlimi for its relational expression. Note that f : NN --> ~H 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.)

Ref Expression
Assertion df-hlim ⊢⇝v=fw|f:ℕ⟶ℋ∧w∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x

Detailed syntax breakdown

Step Hyp Ref Expression
0 chli class⇝v
1 vf setvarf
2 vw setvarw
3 1 cv setvarf
4 cn classℕ
5 chba classℋ
6 4 5 3 wf wfff:ℕ⟶ℋ
7 2 cv setvarw
8 7 5 wcel wffw∈ℋ
9 6 8 wa wfff:ℕ⟶ℋ∧w∈ℋ
10 vx setvarx
11 crp classℝ+
12 vy setvary
13 vz setvarz
14 cuz classℤ≥
15 12 cv setvary
16 15 14 cfv classℤ≥y
17 cno classnormℎ
18 13 cv setvarz
19 18 3 cfv classf⁡z
20 cmv class-ℎ
21 19 7 20 co classf⁡z-ℎw
22 21 17 cfv classnormℎ⁡f⁡z-ℎw
23 clt class<
24 10 cv setvarx
25 22 24 23 wbr wffnormℎ⁡f⁡z-ℎw<x
26 25 13 16 wral wff∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x
27 26 12 4 wrex wff∃y∈ℕ∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x
28 27 10 11 wral wff∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x
29 9 28 wa wfff:ℕ⟶ℋ∧w∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x
30 29 1 2 copab classfw|f:ℕ⟶ℋ∧w∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x
31 0 30 wceq wff⇝v=fw|f:ℕ⟶ℋ∧w∈ℋ∧∀x∈ℝ+∃y∈ℕ∀z∈ℤ≥ynormℎ⁡f⁡z-ℎw<x