Metamath Proof Explorer


Table of Contents - 9.2.3. The dual of an ordered set

  1. codu
  2. df-odu
  3. oduval
  4. oduleval
  5. oduleg
  6. odubas
  7. pospropd
  8. odupos
  9. oduposb
  10. meet0
  11. join0
  12. oduglb
  13. odumeet
  14. odulub
  15. odujoin
  16. odulatb
  17. oduclatb
  18. odulat
  19. poslubmo
  20. posglbmo
  21. poslubd
  22. poslubdg
  23. posglbd