Metamath Proof Explorer

Table of Contents - 20.39.19.3. Measures

Proofs for most of the theorems in section 112 of [Fremlin1]

1. cmea
2. df-mea
3. ismea
4. dmmeasal
5. meaf
6. mea0
7. nnfoctbdjlem
8. nnfoctbdj
9. meadjuni
10. meacl
11. iundjiunlem
12. iundjiun
13. meaxrcl
14. meadjun
15. meassle
16. meaunle
17. meadjiunlem
18. meadjiun
19. ismeannd
20. meaiunlelem
21. meaiunle
22. psmeasurelem
23. psmeasure
24. voliunsge0lem
25. voliunsge0
26. volmea
27. meage0
28. meadjunre
29. meassre
30. meale0eq0
31. meadif
32. meaiuninclem
33. meaiuninc
34. meaiuninc2
35. meaiunincf
36. meaiuninc3v
37. meaiuninc3
38. meaiininclem
39. meaiininc
40. meaiininc2