Metamath Proof Explorer

Table of Contents - 20.11. Mathbox for Jeff Hankins

1. Miscellany
   1. a1i14
   2. a1i24
   3. exp5d
   4. exp5g
   5. exp5k
   6. exp56
   7. exp58
   8. exp510
   9. exp511
   10. exp512
   11. 3com12d
   12. imp5p
   13. imp5q
   14. ecase13d
   15. subtr
   16. subtr2
   17. trer
   18. elicc3
   19. finminlem
   20. gtinf
   21. opnrebl
   22. opnrebl2
   23. nn0prpwlem
   24. nn0prpw
2. Basic topological facts
   1. topbnd
   2. opnbnd
   3. cldbnd
   4. ntruni
   5. clsun
   6. clsint2
   7. opnregcld
   8. cldregopn
   9. neiin
   10. hmeoclda
   11. hmeocldb
3. Topology of the real numbers
   1. ivthALT
4. Refinements
   1. cfne
   2. df-fne
   3. fnerel
   4. isfne
   5. isfne4
   6. isfne4b
   7. isfne2
   8. isfne3
   9. fnebas
   10. fnetg
   11. fnessex
   12. fneuni
   13. fneint
   14. fness
   15. fneref
   16. fnetr
   17. fneval
   18. fneer
   19. topfne
   20. topfneec
   21. topfneec2
   22. fnessref
   23. refssfne
5. Neighborhood bases determine topologies
   1. neibastop1
   2. neibastop2lem
   3. neibastop2
   4. neibastop3
6. Lattice structure of topologies
   1. topmtcl
   2. topmeet
   3. topjoin
   4. fnemeet1
   5. fnemeet2
   6. fnejoin1
   7. fnejoin2
7. Filter bases
   1. fgmin
   2. neifg
8. Directed sets, nets
   1. tailfval
   2. tailval
   3. eltail
   4. tailf
   5. tailini
   6. tailfb
   7. filnetlem1
   8. filnetlem2
   9. filnetlem3
   10. filnetlem4
   11. filnet