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

Definition df-cfil 19246
 Description: Define the set of Cauchy filters on a metric space. A Cauchy filter is a filter on the set such that for every there is an element of the filter whose metric diameter is less than . (Contributed by Mario Carneiro, 13-Oct-2015.)
Assertion
Ref Expression
df-cfil CauFil
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-cfil
StepHypRef Expression
1 ccfil 19243 . 2 CauFil
2 vd . . 3
3 cxmt 16724 . . . . 5
43crn 4914 . . . 4
54cuni 4044 . . 3
62cv 1653 . . . . . . . 8
7 vy . . . . . . . . . 10
87cv 1653 . . . . . . . . 9
98, 8cxp 4911 . . . . . . . 8
106, 9cima 4916 . . . . . . 7
11 cc0 9028 . . . . . . . 8
12 vx . . . . . . . . 9
1312cv 1653 . . . . . . . 8
14 cico 10956 . . . . . . . 8
1511, 13, 14co 6117 . . . . . . 7
1610, 15wss 3309 . . . . . 6
17 vf . . . . . . 7
1817cv 1653 . . . . . 6
1916, 7, 18wrex 2713 . . . . 5
20 crp 10650 . . . . 5
2119, 12, 20wral 2712 . . . 4
226cdm 4913 . . . . . 6
2322cdm 4913 . . . . 5
24 cfil 17915 . . . . 5
2523, 24cfv 5489 . . . 4
2621, 17, 25crab 2716 . . 3
272, 5, 26cmpt 4297 . 2
281, 27wceq 1654 1 CauFil
 Colors of variables: wff set class This definition is referenced by:  cfilfval  19255  cfili  19259  cfilfcls  19265
 Copyright terms: Public domain W3C validator