Metamath Proof Explorer

Table of Contents - 21.51.17. Kan extensions and related concepts

1. Kan extensions
   1. clan
   2. cran
   3. df-lan
   4. df-ran
   5. lanfn
   6. ranfn
   7. reldmlan
   8. reldmran
   9. lanfval
   10. ranfval
   11. lanpropd
   12. ranpropd
   13. reldmlan2
   14. reldmran2
   15. lanval
   16. ranval
   17. lanrcl
   18. ranrcl
   19. rellan
   20. relran
   21. islan
   22. islan2
   23. lanval2
   24. isran
   25. isran2
   26. ranval2
   27. ranval3
   28. lanrcl2
   29. lanrcl3
   30. lanrcl4
   31. lanrcl5
   32. ranrcl2
   33. ranrcl3
   34. ranrcl4lem
   35. ranrcl4
   36. ranrcl5
   37. lanup
   38. ranup
2. Limits and colimits
   1. clmd
   2. ccmd
   3. df-lmd
   4. df-cmd
   5. reldmlmd
   6. reldmcmd
   7. lmdfval
   8. cmdfval
   9. lmdrcl
   10. cmdrcl
   11. reldmlmd2
   12. reldmcmd2
   13. lmdfval2
   14. cmdfval2
   15. lmdpropd
   16. cmdpropd
   17. rellmd
   18. relcmd
   19. concl
   20. coccl
   21. concom
   22. coccom
   23. islmd
   24. iscmd
   25. lmddu
   26. cmddu
   27. initocmd
   28. termolmd
   29. lmdran
   30. cmdlan