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

Definition df-cfil 18681
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 18678 . 2  class CauFil
2 vd . . 3  set  d
3 cxmt 16369 . . . . 5  class  * Met
43crn 4690 . . . 4  class  ran  * Met
54cuni 3827 . . 3  class  U. ran  * Met
62cv 1622 . . . . . . . 8  class  d
7 vy . . . . . . . . . 10  set  y
87cv 1622 . . . . . . . . 9  class  y
98, 8cxp 4687 . . . . . . . 8  class  ( y  X.  y )
106, 9cima 4692 . . . . . . 7  class  ( d
" ( y  X.  y ) )
11 cc0 8737 . . . . . . . 8  class  0
12 vx . . . . . . . . 9  set  x
1312cv 1622 . . . . . . . 8  class  x
14 cico 10658 . . . . . . . 8  class  [,)
1511, 13, 14co 5858 . . . . . . 7  class  ( 0 [,) x )
1610, 15wss 3152 . . . . . 6  wff  ( d
" ( y  X.  y ) )  C_  ( 0 [,) x
)
17 vf . . . . . . 7  set  f
1817cv 1622 . . . . . 6  class  f
1916, 7, 18wrex 2544 . . . . 5  wff  E. y  e.  f  ( d " ( y  X.  y ) )  C_  ( 0 [,) x
)
20 crp 10354 . . . . 5  class  RR+
2119, 12, 20wral 2543 . . . 4  wff  A. x  e.  RR+  E. y  e.  f  ( d "
( y  X.  y
) )  C_  (
0 [,) x )
226cdm 4689 . . . . . 6  class  dom  d
2322cdm 4689 . . . . 5  class  dom  dom  d
24 cfil 17540 . . . . 5  class  Fil
2523, 24cfv 5255 . . . 4  class  ( Fil `  dom  dom  d )
2621, 17, 25crab 2547 . . 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 4077 . 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  18690  cfili  18694  cfilfcls  18700
  Copyright terms: Public domain W3C validator