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

Definition df-fil 17541
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  RR. 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  |-  Fil  =  ( z  e.  _V  |->  { f  e.  (
fBas `  z )  |  A. x  e.  ~P  z ( ( f  i^i  ~P x )  =/=  (/)  ->  x  e.  f ) } )
Distinct variable group:    x, f, z

Detailed syntax breakdown of Definition df-fil
StepHypRef Expression
1 cfil 17540 . 2  class  Fil
2 vz . . 3  set  z
3 cvv 2788 . . 3  class  _V
4 vf . . . . . . . . 9  set  f
54cv 1622 . . . . . . . 8  class  f
6 vx . . . . . . . . . 10  set  x
76cv 1622 . . . . . . . . 9  class  x
87cpw 3625 . . . . . . . 8  class  ~P x
95, 8cin 3151 . . . . . . 7  class  ( f  i^i  ~P x )
10 c0 3455 . . . . . . 7  class  (/)
119, 10wne 2446 . . . . . 6  wff  ( f  i^i  ~P x )  =/=  (/)
126, 4wel 1685 . . . . . 6  wff  x  e.  f
1311, 12wi 4 . . . . 5  wff  ( ( f  i^i  ~P x
)  =/=  (/)  ->  x  e.  f )
142cv 1622 . . . . . 6  class  z
1514cpw 3625 . . . . 5  class  ~P z
1613, 6, 15wral 2543 . . . 4  wff  A. x  e.  ~P  z ( ( f  i^i  ~P x
)  =/=  (/)  ->  x  e.  f )
17 cfbas 17518 . . . . 5  class  fBas
1814, 17cfv 5255 . . . 4  class  ( fBas `  z )
1916, 4, 18crab 2547 . . 3  class  { f  e.  ( fBas `  z
)  |  A. x  e.  ~P  z ( ( f  i^i  ~P x
)  =/=  (/)  ->  x  e.  f ) }
202, 3, 19cmpt 4077 . 2  class  ( z  e.  _V  |->  { f  e.  ( fBas `  z
)  |  A. x  e.  ~P  z ( ( f  i^i  ~P x
)  =/=  (/)  ->  x  e.  f ) } )
211, 20wceq 1623 1  wff  Fil  =  ( z  e.  _V  |->  { f  e.  (
fBas `  z )  |  A. x  e.  ~P  z ( ( f  i^i  ~P x )  =/=  (/)  ->  x  e.  f ) } )
Colors of variables: wff set class
This definition is referenced by:  isfil  17542  filunirn  17577
  Copyright terms: Public domain W3C validator