Metamath Proof Explorer

Table of Contents - 12.2. Filters and filter bases

1. Filter bases
   1. elmptrab
   2. elmptrab2
   3. isfbas
   4. fbasne0
   5. 0nelfb
   6. fbsspw
   7. fbelss
   8. fbdmn0
   9. isfbas2
   10. fbasssin
   11. fbssfi
   12. fbssint
   13. fbncp
   14. fbun
   15. fbfinnfr
   16. opnfbas
   17. trfbas2
   18. trfbas
2. Filters
   1. cfil
   2. df-fil
   3. isfil
   4. filfbas
   5. 0nelfil
   6. fileln0
   7. filsspw
   8. filelss
   9. filss
   10. filin
   11. filtop
   12. isfil2
   13. isfildlem
   14. isfild
   15. filfi
   16. filinn0
   17. filintn0
   18. filn0
   19. infil
   20. snfil
   21. fbasweak
   22. snfbas
   23. fsubbas
   24. fbasfip
   25. fbunfip
   26. fgval
   27. elfg
   28. ssfg
   29. fgss
   30. fgss2
   31. fgfil
   32. elfilss
   33. filfinnfr
   34. fgcl
   35. fgabs
   36. neifil
   37. filunibas
   38. filunirn
   39. filconn
   40. fbasrn
   41. filuni
   42. trfil1
   43. trfil2
   44. trfil3
   45. trfilss
   46. fgtr
   47. trfg
   48. trnei
   49. cfinfil
   50. csdfil
   51. supfil
   52. zfbas
   53. uzrest
   54. uzfbas
3. Ultrafilters
   1. cufil
   2. cufl
   3. df-ufil
   4. df-ufl
   5. isufil
   6. ufilfil
   7. ufilss
   8. ufilb
   9. ufilmax
   10. isufil2
   11. ufprim
   12. trufil
   13. filssufilg
   14. filssufil
   15. isufl
   16. ufli
   17. numufl
   18. fiufl
   19. acufl
   20. ssufl
   21. ufileu
   22. filufint
   23. uffix
   24. fixufil
   25. uffixfr
   26. uffix2
   27. uffixsn
   28. ufildom1
   29. uffinfix
   30. cfinufil
   31. ufinffr
   32. ufilen
   33. ufildr
   34. fin1aufil
4. Filter limits
   1. cfm
   2. cflim
   3. cflf
   4. cfcls
   5. cfcf
   6. df-fm
   7. df-flim
   8. df-flf
   9. df-fcls
   10. df-fcf
   11. fmval
   12. fmfil
   13. fmf
   14. fmss
   15. elfm
   16. elfm2
   17. fmfg
   18. elfm3
   19. imaelfm
   20. rnelfmlem
   21. rnelfm
   22. fmfnfmlem1
   23. fmfnfmlem2
   24. fmfnfmlem3
   25. fmfnfmlem4
   26. fmfnfm
   27. fmufil
   28. fmid
   29. fmco
   30. ufldom
   31. flimval
   32. elflim2
   33. flimtop
   34. flimneiss
   35. flimnei
   36. flimelbas
   37. flimfil
   38. flimtopon
   39. elflim
   40. flimss2
   41. flimss1
   42. neiflim
   43. flimopn
   44. fbflim
   45. fbflim2
   46. flimclsi
   47. hausflimlem
   48. hausflimi
   49. hausflim
   50. flimcf
   51. flimrest
   52. flimclslem
   53. flimcls
   54. flimsncls
   55. hauspwpwf1
   56. hauspwpwdom
   57. flffval
   58. flfval
   59. flfnei
   60. flfneii
   61. isflf
   62. flfelbas
   63. flffbas
   64. flftg
   65. hausflf
   66. hausflf2
   67. cnpflfi
   68. cnpflf2
   69. cnpflf
   70. cnflf
   71. cnflf2
   72. flfcnp
   73. lmflf
   74. txflf
   75. flfcnp2
   76. fclsval
   77. isfcls
   78. fclsfil
   79. fclstop
   80. fclstopon
   81. isfcls2
   82. fclsopn
   83. fclsopni
   84. fclselbas
   85. fclsneii
   86. fclssscls
   87. fclsnei
   88. supnfcls
   89. fclsbas
   90. fclsss1
   91. fclsss2
   92. fclsrest
   93. fclscf
   94. flimfcls
   95. fclsfnflim
   96. flimfnfcls
   97. fclscmpi
   98. fclscmp
   99. uffclsflim
   100. ufilcmp
   101. fcfval
   102. isfcf
   103. fcfnei
   104. fcfelbas
   105. fcfneii
   106. flfssfcf
   107. uffcfflf
   108. cnpfcfi
   109. cnpfcf
   110. cnfcf
   111. flfcntr
   112. alexsublem
   113. alexsub
   114. alexsubb
   115. alexsubALTlem1
   116. alexsubALTlem2
   117. alexsubALTlem3
   118. alexsubALTlem4
   119. alexsubALT
   120. ptcmplem1
   121. ptcmplem2
   122. ptcmplem3
   123. ptcmplem4
   124. ptcmplem5
   125. ptcmpg
   126. ptcmp
5. Extension by continuity
   1. ccnext
   2. df-cnext
   3. cnextval
   4. cnextfval
   5. cnextrel
   6. cnextfun
   7. cnextfvval
   8. cnextf
   9. cnextcn
   10. cnextfres1
   11. cnextfres
6. Topological groups
   1. ctmd
   2. ctgp
   3. df-tmd
   4. df-tgp
   5. istmd
   6. tmdmnd
   7. tmdtps
   8. istgp
   9. tgpgrp
   10. tgptmd
   11. tgptps
   12. tmdtopon
   13. tgptopon
   14. tmdcn
   15. tgpcn
   16. tgpinv
   17. grpinvhmeo
   18. cnmpt1plusg
   19. cnmpt2plusg
   20. tmdcn2
   21. tgpsubcn
   22. istgp2
   23. tmdmulg
   24. tgpmulg
   25. tgpmulg2
   26. tmdgsum
   27. tmdgsum2
   28. oppgtmd
   29. oppgtgp
   30. distgp
   31. indistgp
   32. efmndtmd
   33. tmdlactcn
   34. tgplacthmeo
   35. submtmd
   36. subgtgp
   37. symgtgp
   38. subgntr
   39. opnsubg
   40. clssubg
   41. clsnsg
   42. cldsubg
   43. tgpconncompeqg
   44. tgpconncomp
   45. tgpconncompss
   46. ghmcnp
   47. snclseqg
   48. tgphaus
   49. tgpt1
   50. tgpt0
   51. qustgpopn
   52. qustgplem
   53. qustgp
   54. qustgphaus
   55. prdstmdd
   56. prdstgpd
7. Infinite group sum on topological groups
   1. ctsu
   2. df-tsms
   3. tsmsfbas
   4. tsmslem1
   5. tsmsval2
   6. tsmsval
   7. tsmspropd
   8. eltsms
   9. tsmsi
   10. tsmscl
   11. haustsms
   12. haustsms2
   13. tsmscls
   14. tsmsgsum
   15. tsmsid
   16. haustsmsid
   17. tsms0
   18. tsmssubm
   19. tsmsres
   20. tsmsf1o
   21. tsmsmhm
   22. tsmsadd
   23. tsmsinv
   24. tsmssub
   25. tgptsmscls
   26. tgptsmscld
   27. tsmssplit
   28. tsmsxplem1
   29. tsmsxplem2
   30. tsmsxp
8. Topological rings, fields, vector spaces
   1. ctrg
   2. ctdrg
   3. ctlm
   4. ctvc
   5. df-trg
   6. df-tdrg
   7. df-tlm
   8. df-tvc
   9. istrg
   10. trgtmd
   11. istdrg
   12. tdrgunit
   13. trgtgp
   14. trgtmd2
   15. trgtps
   16. trgring
   17. trggrp
   18. tdrgtrg
   19. tdrgdrng
   20. tdrgring
   21. tdrgtmd
   22. tdrgtps
   23. istdrg2
   24. mulrcn
   25. invrcn2
   26. invrcn
   27. cnmpt1mulr
   28. cnmpt2mulr
   29. dvrcn
   30. istlm
   31. vscacn
   32. tlmtmd
   33. tlmtps
   34. tlmlmod
   35. tlmtrg
   36. tlmscatps
   37. istvc
   38. tvctdrg
   39. cnmpt1vsca
   40. cnmpt2vsca
   41. tlmtgp
   42. tvctlm
   43. tvclmod
   44. tvclvec