Metamath Proof Explorer

Table of Contents - 16.2.11. Point inversions

1. cmir
2. df-mir
3. mirreu3
4. mirval
5. mirfv
6. mircgr
7. mirbtwn
8. ismir
9. mirf
10. mircl
11. mirmir
12. mircom
13. mirreu
14. mireq
15. mirinv
16. mirne
17. mircinv
18. mirf1o
19. miriso
20. mirbtwni
21. mirbtwnb
22. mircgrs
23. mirmir2
24. mirmot
25. mirln
26. mirln2
27. mirconn
28. mirhl
29. mirbtwnhl
30. mirhl2
31. mircgrextend
32. mirtrcgr
33. mirauto
34. miduniq
35. miduniq1
36. miduniq2
37. colmid
38. symquadlem
39. krippenlem
40. krippen
41. midexlem