MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cfil Unicode version

Definition df-cfil 18677
Description: Define the set of Cauchy filters on a metric space. A Cauchy filter is a filter on the set such that for every  0  <  x there is an element of the filter whose metric diameter is less than  x. (Contributed by Mario Carneiro, 13-Oct-2015.)
Assertion
Ref Expression
df-cfil  |- CauFil  =  ( d  e.  U. ran  * Met  |->  { f  e.  ( Fil `  dom  dom  d )  |  A. x  e.  RR+  E. y  e.  f  ( d " ( y  X.  y ) )  C_  ( 0 [,) x
) } )
Distinct variable group:    f, d, x, y

Detailed syntax breakdown of Definition df-cfil
StepHypRef Expression
1 ccfil 18674 . 2  class CauFil
2 vd . . 3  set  d
3 cxmt 16365 . . . . 5  class  * Met
43crn 4689 . . . 4  class  ran  * Met
54cuni 3828 . . 3  class  U. ran  * Met
62cv 1622 . . . . . . . 8  class  d
7 vy . . . . . . . . . 10  set  y
87cv 1622 . . . . . . . . 9  class  y
98, 8cxp 4686 . . . . . . . 8  class  ( y  X.  y )
106, 9cima 4691 . . . . . . 7  class  ( d
" ( y  X.  y ) )
11 cc0 8733 . . . . . . . 8  class  0
12 vx . . . . . . . . 9  set  x
1312cv 1622 . . . . . . . 8  class  x
14 cico 10654 . . . . . . . 8  class  [,)
1511, 13, 14co 5820 . . . . . . 7  class  ( 0 [,) x )
1610, 15wss 3153 . . . . . 6  wff  ( d
" ( y  X.  y ) )  C_  ( 0 [,) x
)
17 vf . . . . . . 7  set  f
1817cv 1622 . . . . . 6  class  f
1916, 7, 18wrex 2545 . . . . 5  wff  E. y  e.  f  ( d " ( y  X.  y ) )  C_  ( 0 [,) x
)
20 crp 10350 . . . . 5  class  RR+
2119, 12, 20wral 2544 . . . 4  wff  A. x  e.  RR+  E. y  e.  f  ( d "
( y  X.  y
) )  C_  (
0 [,) x )
226cdm 4688 . . . . . 6  class  dom  d
2322cdm 4688 . . . . 5  class  dom  dom  d
24 cfil 17536 . . . . 5  class  Fil
2523, 24cfv 5221 . . . 4  class  ( Fil `  dom  dom  d )
2621, 17, 25crab 2548 . . 3  class  { f  e.  ( Fil `  dom  dom  d )  |  A. x  e.  RR+  E. y  e.  f  ( d " ( y  X.  y ) )  C_  ( 0 [,) x
) }
272, 5, 26cmpt 4078 . 2  class  ( d  e.  U. ran  * Met  |->  { f  e.  ( Fil `  dom  dom  d )  |  A. x  e.  RR+  E. y  e.  f  ( d " ( y  X.  y ) )  C_  ( 0 [,) x
) } )
281, 27wceq 1623 1  wff CauFil  =  ( d  e.  U. ran  * Met  |->  { f  e.  ( Fil `  dom  dom  d )  |  A. x  e.  RR+  E. y  e.  f  ( d " ( y  X.  y ) )  C_  ( 0 [,) x
) } )
Colors of variables: wff set class
This definition is referenced by:  cfilfval  18686  cfili  18690  cfilfcls  18696
  Copyright terms: Public domain W3C validator