Metamath Proof Explorer


Table of Contents - 20.46.3. Greater than, greater than or equal to.

As a stylistic issue, set.mm prefers 'less than' instead of 'greater than' to reduce the number of conversion steps. Here we formally define the widely-used relations 'greater than' and 'greater than or equal to', so that we have formal definitions of them, as well as a few related theorems.

  1. cge-real
  2. cgt
  3. df-gte
  4. df-gt
  5. gte-lte
  6. gt-lt
  7. gte-lteh
  8. gt-lth
  9. ex-gt
  10. ex-gte