Metamath Proof Explorer

Table of Contents - 20.21. Mathbox for Jeff Madsen

1. Logic and set theory
   1. unirep
   2. cover2
   3. cover2g
   4. brabg2
   5. opelopab3
   6. cocanfo
   7. brresi2
   8. fnopabeqd
   9. fvopabf4g
   10. eqfnun
   11. fnopabco
   12. opropabco
   13. cocnv
   14. f1ocan1fv
   15. f1ocan2fv
   16. inixp
   17. upixp
   18. abrexdom
   19. abrexdom2
   20. ac6gf
   21. indexa
   22. indexdom
   23. frinfm
   24. welb
   25. supex2g
   26. supclt
   27. supubt
2. Real and complex numbers; integers
   1. filbcmb
   2. fzmul
3. Sequences and sums
   1. sdclem2
   2. sdclem1
   3. sdc
   4. fdc
   5. fdc1
   6. seqpo
   7. incsequz
   8. incsequz2
   9. nnubfi
   10. nninfnub
4. Topology
   1. subspopn
   2. neificl
   3. lpss2
5. Metric spaces
   1. metf1o
   2. blssp
   3. mettrifi
   4. lmclim2
   5. geomcau
   6. caures
   7. caushft
6. Continuous maps and homeomorphisms
   1. constcncf
   2. cnres2
   3. cnresima
   4. cncfres
7. Boundedness
   1. ctotbnd
   2. cbnd
   3. df-totbnd
   4. istotbnd
   5. istotbnd2
   6. istotbnd3
   7. totbndmet
   8. 0totbnd
   9. sstotbnd2
   10. sstotbnd
   11. sstotbnd3
   12. totbndss
   13. equivtotbnd
   14. df-bnd
   15. isbnd
   16. bndmet
   17. isbndx
   18. isbnd2
   19. isbnd3
   20. isbnd3b
   21. bndss
   22. blbnd
   23. ssbnd
   24. totbndbnd
   25. equivbnd
   26. bnd2lem
   27. equivbnd2
   28. prdsbnd
   29. prdstotbnd
   30. prdsbnd2
   31. cntotbnd
   32. cnpwstotbnd
8. Isometries
   1. cismty
   2. df-ismty
   3. ismtyval
   4. isismty
   5. ismtycnv
   6. ismtyima
   7. ismtyhmeolem
   8. ismtyhmeo
   9. ismtybndlem
   10. ismtybnd
   11. ismtyres
9. Heine-Borel Theorem
   1. heibor1lem
   2. heibor1
   3. heiborlem1
   4. heiborlem2
   5. heiborlem3
   6. heiborlem4
   7. heiborlem5
   8. heiborlem6
   9. heiborlem7
   10. heiborlem8
   11. heiborlem9
   12. heiborlem10
   13. heibor
10. Banach Fixed Point Theorem
    1. bfplem1
    2. bfplem2
    3. bfp
11. Euclidean space
    1. crrn
    2. df-rrn
    3. rrnval
    4. rrnmval
    5. rrnmet
    6. rrndstprj1
    7. rrndstprj2
    8. rrncmslem
    9. rrncms
    10. repwsmet
    11. rrnequiv
    12. rrntotbnd
    13. rrnheibor
12. Intervals (continued)
    1. ismrer1
    2. reheibor
    3. iccbnd
    4. icccmpALT
13. Operation properties
    1. cass
    2. df-ass
    3. cexid
    4. df-exid
    5. isass
    6. isexid
14. Groups and related structures
    1. cmagm
    2. df-mgmOLD
    3. ismgmOLD
    4. clmgmOLD
    5. opidonOLD
    6. rngopidOLD
    7. opidon2OLD
    8. isexid2
    9. exidu1
    10. idrval
    11. iorlid
    12. cmpidelt
    13. csem
    14. df-sgrOLD
    15. smgrpismgmOLD
    16. issmgrpOLD
    17. smgrpmgm
    18. smgrpassOLD
    19. cmndo
    20. df-mndo
    21. mndoissmgrpOLD
    22. mndoisexid
    23. mndoismgmOLD
    24. mndomgmid
    25. ismndo
    26. ismndo1
    27. ismndo2
    28. grpomndo
    29. exidcl
    30. exidreslem
    31. exidres
    32. exidresid
    33. ablo4pnp
    34. grpoeqdivid
    35. grposnOLD
15. Group homomorphism and isomorphism
    1. cghomOLD
    2. df-ghomOLD
    3. elghomlem1OLD
    4. elghomlem2OLD
    5. elghomOLD
    6. ghomlinOLD
    7. ghomidOLD
    8. ghomf
    9. ghomco
    10. ghomdiv
    11. grpokerinj
16. Rings
    1. crngo
    2. df-rngo
    3. relrngo
    4. isrngo
    5. isrngod
    6. rngoi
    7. rngosm
    8. rngocl
    9. rngoid
    10. rngoideu
    11. rngodi
    12. rngodir
    13. rngoass
    14. rngo2
    15. rngoablo
    16. rngoablo2
    17. rngogrpo
    18. rngone0
    19. rngogcl
    20. rngocom
    21. rngoaass
    22. rngoa32
    23. rngoa4
    24. rngorcan
    25. rngolcan
    26. rngo0cl
    27. rngo0rid
    28. rngo0lid
    29. rngolz
    30. rngorz
    31. rngosn3
    32. rngosn4
    33. rngosn6
    34. rngonegcl
    35. rngoaddneg1
    36. rngoaddneg2
    37. rngosub
    38. rngmgmbs4
    39. rngodm1dm2
    40. rngorn1
    41. rngorn1eq
    42. rngomndo
    43. rngoidmlem
    44. rngolidm
    45. rngoridm
    46. rngo1cl
    47. rngoueqz
    48. rngonegmn1l
    49. rngonegmn1r
    50. rngoneglmul
    51. rngonegrmul
    52. rngosubdi
    53. rngosubdir
    54. zerdivemp1x
17. Division Rings
    1. cdrng
    2. df-drngo
    3. isdivrngo
    4. drngoi
    5. gidsn
    6. zrdivrng
    7. dvrunz
    8. isgrpda
    9. isdrngo1
    10. divrngcl
    11. isdrngo2
    12. isdrngo3
18. Ring homomorphisms
    1. crnghom
    2. crngiso
    3. crisc
    4. df-rngohom
    5. rngohomval
    6. isrngohom
    7. rngohomf
    8. rngohomcl
    9. rngohom1
    10. rngohomadd
    11. rngohommul
    12. rngogrphom
    13. rngohom0
    14. rngohomsub
    15. rngohomco
    16. rngokerinj
    17. df-rngoiso
    18. rngoisoval
    19. isrngoiso
    20. rngoiso1o
    21. rngoisohom
    22. rngoisocnv
    23. rngoisoco
    24. df-risc
    25. isriscg
    26. isrisc
    27. risc
    28. risci
    29. riscer
19. Commutative rings
    1. ccm2
    2. df-com2
    3. cfld
    4. df-fld
    5. ccring
    6. df-crngo
    7. iscom2
    8. iscrngo
    9. iscrngo2
    10. iscringd
    11. flddivrng
    12. crngorngo
    13. crngocom
    14. crngm23
    15. crngm4
    16. fldcrng
    17. isfld2
    18. crngohomfo
20. Ideals
    1. cidl
    2. cpridl
    3. cmaxidl
    4. df-idl
    5. df-pridl
    6. df-maxidl
    7. idlval
    8. isidl
    9. isidlc
    10. idlss
    11. idlcl
    12. idl0cl
    13. idladdcl
    14. idllmulcl
    15. idlrmulcl
    16. idlnegcl
    17. idlsubcl
    18. rngoidl
    19. 0idl
    20. 1idl
    21. 0rngo
    22. divrngidl
    23. intidl
    24. inidl
    25. unichnidl
    26. keridl
    27. pridlval
    28. ispridl
    29. pridlidl
    30. pridlnr
    31. pridl
    32. ispridl2
    33. maxidlval
    34. ismaxidl
    35. maxidlidl
    36. maxidlnr
    37. maxidlmax
    38. maxidln1
    39. maxidln0
21. Prime rings and integral domains
    1. cprrng
    2. cdmn
    3. df-prrngo
    4. df-dmn
    5. isprrngo
    6. prrngorngo
    7. smprngopr
    8. divrngpr
    9. isdmn
    10. isdmn2
    11. dmncrng
    12. dmnrngo
    13. flddmn
22. Ideal generators
    1. cigen
    2. df-igen
    3. igenval
    4. igenss
    5. igenidl
    6. igenmin
    7. igenidl2
    8. igenval2
    9. prnc
    10. isfldidl
    11. isfldidl2
    12. ispridlc
    13. pridlc
    14. pridlc2
    15. pridlc3
    16. isdmn3
    17. dmnnzd
    18. dmncan1
    19. dmncan2