This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-hcau

Description: Define the set of Cauchy sequences on a Hilbert space. See hcau for its membership relation. Note that f : NN --> ~H is an infinite sequence of vectors, i.e. a mapping from integers to vectors. Definition of Cauchy sequence in Beran p. 96. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

Ref Expression
Assertion df-hcau ⊢ Cauchy = f ∈ ℋ ℕ | ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccauold class Cauchy
1 vf setvar f
2 chba class ℋ
3 cmap class ↑ 𝑚
4 cn class ℕ
5 2 4 3 co class ℋ ℕ
6 vx setvar x
7 crp class ℝ +
8 vy setvar y
9 vz setvar z
10 cuz class ℤ ≥
11 8 cv setvar y
12 11 10 cfv class ℤ ≥ y
13 cno class norm ℎ
14 1 cv setvar f
15 11 14 cfv class f ⁡ y
16 cmv class - ℎ
17 9 cv setvar z
18 17 14 cfv class f ⁡ z
19 15 18 16 co class f ⁡ y - ℎ f ⁡ z
20 19 13 cfv class norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z
21 clt class <
22 6 cv setvar x
23 20 22 21 wbr wff norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x
24 23 9 12 wral wff ∀ z ∈ ℤ ≥ y norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x
25 24 8 4 wrex wff ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x
26 25 6 7 wral wff ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x
27 26 1 5 crab class f ∈ ℋ ℕ | ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x
28 0 27 wceq wff Cauchy = f ∈ ℋ ℕ | ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ f ⁡ y - ℎ f ⁡ z < x