Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-totbnd Unicode version

Definition df-totbnd 26595
Description: Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
df-totbnd  |-  TotBnd  =  ( x  e.  _V  |->  { m  e.  ( Met `  x )  |  A. d  e.  RR+  E. v  e.  Fin  ( U. v  =  x  /\  A. b  e.  v  E. y  e.  x  b  =  ( y ( ball `  m ) d ) ) } )
Distinct variable group:    b, d, m, v, x, y

Detailed syntax breakdown of Definition df-totbnd
StepHypRef Expression
1 ctotbnd 26593 . 2  class  TotBnd
2 vx . . 3  set  x
3 cvv 2801 . . 3  class  _V
4 vv . . . . . . . . . 10  set  v
54cv 1631 . . . . . . . . 9  class  v
65cuni 3843 . . . . . . . 8  class  U. v
72cv 1631 . . . . . . . 8  class  x
86, 7wceq 1632 . . . . . . 7  wff  U. v  =  x
9 vb . . . . . . . . . . 11  set  b
109cv 1631 . . . . . . . . . 10  class  b
11 vy . . . . . . . . . . . 12  set  y
1211cv 1631 . . . . . . . . . . 11  class  y
13 vd . . . . . . . . . . . 12  set  d
1413cv 1631 . . . . . . . . . . 11  class  d
15 vm . . . . . . . . . . . . 13  set  m
1615cv 1631 . . . . . . . . . . . 12  class  m
17 cbl 16387 . . . . . . . . . . . 12  class  ball
1816, 17cfv 5271 . . . . . . . . . . 11  class  ( ball `  m )
1912, 14, 18co 5874 . . . . . . . . . 10  class  ( y ( ball `  m
) d )
2010, 19wceq 1632 . . . . . . . . 9  wff  b  =  ( y ( ball `  m ) d )
2120, 11, 7wrex 2557 . . . . . . . 8  wff  E. y  e.  x  b  =  ( y ( ball `  m ) d )
2221, 9, 5wral 2556 . . . . . . 7  wff  A. b  e.  v  E. y  e.  x  b  =  ( y ( ball `  m ) d )
238, 22wa 358 . . . . . 6  wff  ( U. v  =  x  /\  A. b  e.  v  E. y  e.  x  b  =  ( y (
ball `  m )
d ) )
24 cfn 6879 . . . . . 6  class  Fin
2523, 4, 24wrex 2557 . . . . 5  wff  E. v  e.  Fin  ( U. v  =  x  /\  A. b  e.  v  E. y  e.  x  b  =  ( y ( ball `  m ) d ) )
26 crp 10370 . . . . 5  class  RR+
2725, 13, 26wral 2556 . . . 4  wff  A. d  e.  RR+  E. v  e. 
Fin  ( U. v  =  x  /\  A. b  e.  v  E. y  e.  x  b  =  ( y ( ball `  m ) d ) )
28 cme 16386 . . . . 5  class  Met
297, 28cfv 5271 . . . 4  class  ( Met `  x )
3027, 15, 29crab 2560 . . 3  class  { m  e.  ( Met `  x
)  |  A. d  e.  RR+  E. v  e. 
Fin  ( U. v  =  x  /\  A. b  e.  v  E. y  e.  x  b  =  ( y ( ball `  m ) d ) ) }
312, 3, 30cmpt 4093 . 2  class  ( x  e.  _V  |->  { m  e.  ( Met `  x
)  |  A. d  e.  RR+  E. v  e. 
Fin  ( U. v  =  x  /\  A. b  e.  v  E. y  e.  x  b  =  ( y ( ball `  m ) d ) ) } )
321, 31wceq 1632 1  wff  TotBnd  =  ( x  e.  _V  |->  { m  e.  ( Met `  x )  |  A. d  e.  RR+  E. v  e.  Fin  ( U. v  =  x  /\  A. b  e.  v  E. y  e.  x  b  =  ( y ( ball `  m ) d ) ) } )
Colors of variables: wff set class
This definition is referenced by:  istotbnd  26596
  Copyright terms: Public domain W3C validator