Metamath Proof Explorer

Table of Contents - 21.47. Mathbox for Ender Ting

1. Increasing sequences and subsequences
   1. et-ltneverrefl
   2. et-equeucl
   3. et-sqrtnegnre
   4. ormklocald
   5. ormkglobd
   6. natlocalincr
   7. natglobalincr
   8. cupword
   9. df-upword
   10. upwordnul
   11. upwordisword
   12. singoutnword
   13. singoutnupword
   14. upwordsing
   15. upwordsseti
   16. tworepnotupword
   17. upwrdfi
2. Scratchpad for number theory
   1. evenwodadd
3. Scratchpad for math on real numbers
   1. squeezedltsq
   2. lambert0
   3. lamberte
4. Scratchpad for probability theory