Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dffil  Structured version Unicode version 
Description: The set of filters on a set. Definition 1 (axioms FI, FIIa, FIIb, FIII) of [BourbakiTop1] p. I.36. Filters are used to define the concept of limit in the general case. They are a generalization of the idea of neighborhoods. Suppose you are in . With neighborhoods you can express the idea of a variable that tends to a specific number but you can't express the idea of a variable that tends to infinity. Filters relax the "axioms" of neighborhoods and then succeed in expressing the idea of something that tends to infinity. Filters were invented by Cartan in 1937 and made famous by Bourbaki in his treatise. A notion similar to the notion of filter is the concept of net invented by Moore and Smith in 1922. (Contributed by FL, 20Jul2007.) (Revised by Stefan O'Rear, 28Jul2015.) 
Ref  Expression 

dffil 
Step  Hyp  Ref  Expression 

1  cfil 17869  . 2  
2  vz  . . 3  
3  cvv 2948  . . 3  
4  vf  . . . . . . . . 9  
5  4  cv 1651  . . . . . . . 8 
6  vx  . . . . . . . . . 10  
7  6  cv 1651  . . . . . . . . 9 
8  7  cpw 3791  . . . . . . . 8 
9  5, 8  cin 3311  . . . . . . 7 
10  c0 3620  . . . . . . 7  
11  9, 10  wne 2598  . . . . . 6 
12  6, 4  wel 1726  . . . . . 6 
13  11, 12  wi 4  . . . . 5 
14  2  cv 1651  . . . . . 6 
15  14  cpw 3791  . . . . 5 
16  13, 6, 15  wral 2697  . . . 4 
17  cfbas 16681  . . . . 5  
18  14, 17  cfv 5446  . . . 4 
19  16, 4, 18  crab 2701  . . 3 
20  2, 3, 19  cmpt 4258  . 2 
21  1, 20  wceq 1652  1 
Colors of variables: wff set class 
This definition is referenced by: isfil 17871 filunirn 17906 
Copyright terms: Public domain  W3C validator 