Metamath Proof Explorer

Table of Contents - 20.39.19.4. Outer measures and Caratheodory's construction

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

1. come
2. df-ome
3. ccaragen
4. df-caragen
5. caragenval
6. isome
7. caragenel
8. omef
9. ome0
10. omessle
11. omedm
12. caragensplit
13. caragenelss
14. carageneld
15. omecl
16. caragenss
17. omeunile
18. caragen0
19. omexrcl
20. caragenunidm
21. caragensspw
22. omessre
23. caragenuni
24. caragenuncllem
25. caragenuncl
26. caragendifcl
27. caragenfiiuncl
28. omeunle
29. omeiunle
30. omelesplit
31. omeiunltfirp
32. omeiunlempt
33. carageniuncllem1
34. carageniuncllem2
35. carageniuncl
36. caragenunicl
37. caragensal
38. caratheodorylem1
39. caratheodorylem2
40. caratheodory
41. 0ome
42. isomenndlem
43. isomennd
44. caragenel2d
45. omege0
46. omess0
47. caragencmpl