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 e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccauold 
 |-  Cauchy
1 vf 
 |-  f
2 chba 
 |-  ~H
3 cmap 
 |-  ^m
4 cn 
 |-  NN
5 2 4 3 co 
 |-  ( ~H ^m NN )
6 vx 
 |-  x
7 crp 
 |-  RR+
8 vy 
 |-  y
9 vz 
 |-  z
10 cuz 
 |-  ZZ>=
11 8 cv 
 |-  y
12 11 10 cfv 
 |-  ( ZZ>= ` y )
13 cno 
 |-  normh
14 1 cv 
 |-  f
15 11 14 cfv 
 |-  ( f ` y )
16 cmv 
 |-  -h
17 9 cv 
 |-  z
18 17 14 cfv 
 |-  ( f ` z )
19 15 18 16 co 
 |-  ( ( f ` y ) -h ( f ` z ) )
20 19 13 cfv 
 |-  ( normh ` ( ( f ` y ) -h ( f ` z ) ) )
21 clt 
 |-  <
22 6 cv 
 |-  x
23 20 22 21 wbr 
 |-  ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
24 23 9 12 wral 
 |-  A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
25 24 8 4 wrex 
 |-  E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
26 25 6 7 wral 
 |-  A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x
27 26 1 5 crab 
 |-  { f e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }
28 0 27 wceq 
 |-  Cauchy = { f e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }