Metamath Proof Explorer


Table of Contents - 20.39.19.6. Measurable functions

Proofs for most of the theorems in section 121 of [Fremlin1]. Real-valued functions are considered, and measurability is defined with respect to an arbitrary sigma-algebra. When the sigma-algebra on the domain is the Lebesgue measure on the reals, then all real-valued measurable functions in the sense of df-mbf are also sigma-measurable, but the definition in this section considers as measurable functions, some that are not measurable in the sense of df-mbf (see mbfpsssmf and smfmbfcex).

  1. csmblfn
  2. df-smblfn
  3. pimltmnf2
  4. preimagelt
  5. preimalegt
  6. pimconstlt0
  7. pimconstlt1
  8. pimltpnf
  9. pimgtpnf2
  10. salpreimagelt
  11. pimrecltpos
  12. salpreimalegt
  13. pimiooltgt
  14. preimaicomnf
  15. pimltpnf2
  16. pimgtmnf2
  17. pimdecfgtioc
  18. pimincfltioc
  19. pimdecfgtioo
  20. pimincfltioo
  21. preimaioomnf
  22. preimageiingt
  23. preimaleiinlt
  24. pimgtmnf
  25. pimrecltneg
  26. salpreimagtge
  27. salpreimaltle
  28. issmflem
  29. issmf
  30. salpreimalelt
  31. salpreimagtlt
  32. smfpreimalt
  33. smff
  34. smfdmss
  35. issmff
  36. issmfd
  37. smfpreimaltf
  38. issmfdf
  39. sssmf
  40. mbfresmf
  41. cnfsmf
  42. incsmflem
  43. incsmf
  44. smfsssmf
  45. issmflelem
  46. issmfle
  47. smfpimltmpt
  48. smfpimltxr
  49. issmfdmpt
  50. smfconst
  51. sssmfmpt
  52. cnfrrnsmf
  53. smfid
  54. bormflebmf
  55. smfpreimale
  56. issmfgtlem
  57. issmfgt
  58. issmfled
  59. smfpimltxrmpt
  60. smfmbfcex
  61. issmfgtd
  62. smfpreimagt
  63. smfaddlem1
  64. smfaddlem2
  65. smfadd
  66. decsmflem
  67. decsmf
  68. smfpreimagtf
  69. issmfgelem
  70. issmfge
  71. smflimlem1
  72. smflimlem2
  73. smflimlem3
  74. smflimlem4
  75. smflimlem5
  76. smflimlem6
  77. smflim
  78. nsssmfmbflem
  79. nsssmfmbf
  80. smfpimgtxr
  81. smfpimgtmpt
  82. smfpreimage
  83. mbfpsssmf
  84. smfpimgtxrmpt
  85. smfpimioompt
  86. smfpimioo
  87. smfresal
  88. smfrec
  89. smfres
  90. smfmullem1
  91. smfmullem2
  92. smfmullem3
  93. smfmullem4
  94. smfmul
  95. smfmulc1
  96. smfdiv
  97. smfpimbor1lem1
  98. smfpimbor1lem2
  99. smfpimbor1
  100. smf2id
  101. smfco
  102. smfneg
  103. smffmpt
  104. smflim2
  105. smfpimcclem
  106. smfpimcc
  107. issmfle2d
  108. smflimmpt
  109. smfsuplem1
  110. smfsuplem2
  111. smfsuplem3
  112. smfsup
  113. smfsupmpt
  114. smfsupxr
  115. smfinflem
  116. smfinf
  117. smfinfmpt
  118. smflimsuplem1
  119. smflimsuplem2
  120. smflimsuplem3
  121. smflimsuplem4
  122. smflimsuplem5
  123. smflimsuplem6
  124. smflimsuplem7
  125. smflimsuplem8
  126. smflimsup
  127. smflimsupmpt
  128. smfliminflem
  129. smfliminf
  130. smfliminfmpt