Metamath Proof Explorer


Table of Contents - 20.3.8. Extensible Structures

  1. Structure restriction operator
    1. ressplusf
    2. ressnm
    3. abvpropd2
  2. The opposite group
    1. oppgle
    2. oppgleOLD
    3. oppglt
  3. Posets
    1. ressprs
    2. oduprs
    3. posrasymb
    4. resspos
    5. resstos
    6. odutos
    7. tlt2
    8. tlt3
    9. trleile
    10. toslublem
    11. toslub
    12. tosglblem
    13. tosglb
  4. Complete lattices
    1. clatp0cl
    2. clatp1cl
  5. Order Theory
    1. cmnt
    2. cmgc
    3. df-mnt
    4. df-mgc
    5. mntoval
    6. ismnt
    7. ismntd
    8. mntf
    9. mgcoval
    10. mgcval
    11. mgcf1
    12. mgcf2
    13. mgccole1
    14. mgccole2
    15. mgcmnt1
    16. mgcmnt2
    17. mgcmntco
    18. dfmgc2lem
    19. dfmgc2
    20. mgcmnt1d
    21. mgcmnt2d
    22. mgccnv
    23. pwrssmgc
    24. mgcf1olem1
    25. mgcf1olem2
    26. mgcf1o
  6. Extended reals Structure - misc additions
    1. ax-xrssca
    2. ax-xrsvsca
    3. xrs0
    4. xrslt
    5. xrsinvgval
    6. xrsmulgzz
    7. xrstos
    8. xrsclat
    9. xrsp0
    10. xrsp1
    11. ressmulgnn
    12. ressmulgnn0
  7. The extended nonnegative real numbers commutative monoid
    1. xrge0base
    2. xrge00
    3. xrge0plusg
    4. xrge0le
    5. xrge0mulgnn0
    6. xrge0addass
    7. xrge0addgt0
    8. xrge0adddir
    9. xrge0adddi
    10. xrge0npcan
    11. fsumrp0cl