Metamath Proof Explorer


Table of Contents - 21.3.18.13. Caratheodory's extension theorem

In this section, we define a function which constructs an outer measure, from a pre-measure . An explicit generic definition of an outer measure is not given. It consists of the three following statements: - the outer measure of an empty set is zero (oms0) - it is monotone (omsmon) - it is countably sub-additive (omssubadd) See Definition 1.11.1 of [Bogachev] p. 41.

  1. coms
  2. df-oms
  3. omsval
  4. omsfval
  5. omscl
  6. omsf
  7. oms0
  8. omsmon
  9. omssubaddlem
  10. omssubadd
  11. ccarsg
  12. df-carsg
  13. carsgval
  14. carsgcl
  15. elcarsg
  16. baselcarsg
  17. 0elcarsg
  18. carsguni
  19. elcarsgss
  20. difelcarsg
  21. inelcarsg
  22. unelcarsg
  23. difelcarsg2
  24. carsgmon
  25. carsgsigalem
  26. fiunelcarsg
  27. carsgclctunlem1
  28. carsggect
  29. carsgclctunlem2
  30. carsgclctunlem3
  31. carsgclctun
  32. carsgsiga
  33. omsmeas
  34. pmeasmono
  35. pmeasadd