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 = f w | f : ℕ ⟶ ℋ ∧ w ∈ ℋ ∧ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ f ⁡ z - ℎ w < x

Detailed syntax breakdown

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