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

Definition df-cfilu 21239
 Description: Define the set of Cauchy filter bases on a uniform space. A Cauchy filter base is a filter base on the set such that for every entourage , there is an element of the filter "small enough in " i.e. such that every pair of points in is related by ". Definition 2 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017.)
Assertion
Ref Expression
df-cfilu CauFilu UnifOn
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-cfilu
StepHypRef Expression
1 ccfilu 21238 . 2 CauFilu
2 vu . . 3
3 cust 21151 . . . . 5 UnifOn
43crn 4846 . . . 4 UnifOn
54cuni 4213 . . 3 UnifOn
6 va . . . . . . . . 9
76cv 1436 . . . . . . . 8
87, 7cxp 4843 . . . . . . 7
9 vv . . . . . . . 8
109cv 1436 . . . . . . 7
118, 10wss 3433 . . . . . 6
12 vf . . . . . . 7
1312cv 1436 . . . . . 6
1411, 6, 13wrex 2774 . . . . 5
152cv 1436 . . . . 5
1614, 9, 15wral 2773 . . . 4
1715cuni 4213 . . . . . 6
1817cdm 4845 . . . . 5
19 cfbas 18899 . . . . 5
2018, 19cfv 5592 . . . 4
2116, 12, 20crab 2777 . . 3
222, 5, 21cmpt 4475 . 2 UnifOn
231, 22wceq 1437 1 CauFilu UnifOn
 Colors of variables: wff setvar class This definition is referenced by:  iscfilu  21240
 Copyright terms: Public domain W3C validator