Metamath Proof Explorer

Table of Contents - 8.1.4. Sections, inverses, isomorphisms

1. csect
2. cinv
3. ciso
4. df-sect
5. df-inv
6. df-iso
7. sectffval
8. sectfval
9. sectss
10. issect
11. issect2
12. sectcan
13. sectco
14. isofval
15. invffval
16. invfval
17. isinv
18. invss
19. invsym
20. invsym2
21. invfun
22. isoval
23. inviso1
24. inviso2
25. invf
26. invf1o
27. invinv
28. invco
29. dfiso2
30. dfiso3
31. inveq
32. isofn
33. isohom
34. isoco
35. oppcsect
36. oppcsect2
37. oppcinv
38. oppciso
39. sectmon
40. monsect
41. sectepi
42. episect
43. sectid
44. invid
45. idiso
46. idinv
47. invisoinvl
48. invisoinvr
49. invcoisoid
50. isocoinvid
51. rcaninv