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

Definition df-fil 17866
 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, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
Assertion
Ref Expression
df-fil
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-fil
StepHypRef Expression
1 cfil 17865 . 2
2 vz . . 3
3 cvv 2948 . . 3
4 vf . . . . . . . . 9
54cv 1651 . . . . . . . 8
6 vx . . . . . . . . . 10
76cv 1651 . . . . . . . . 9
87cpw 3791 . . . . . . . 8
95, 8cin 3311 . . . . . . 7
10 c0 3620 . . . . . . 7
119, 10wne 2598 . . . . . 6
126, 4wel 1726 . . . . . 6
1311, 12wi 4 . . . . 5
142cv 1651 . . . . . 6
1514cpw 3791 . . . . 5
1613, 6, 15wral 2697 . . . 4
17 cfbas 16677 . . . . 5
1814, 17cfv 5445 . . . 4
1916, 4, 18crab 2701 . . 3
202, 3, 19cmpt 4258 . 2
211, 20wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  isfil  17867  filunirn  17902
 Copyright terms: Public domain W3C validator