Metamath Proof Explorer

Table of Contents - 21.45.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. pimltmnf2f
  4. pimltmnf2
  5. preimagelt
  6. preimalegt
  7. pimconstlt0
  8. pimconstlt1
  9. pimltpnff
  10. pimltpnf
  11. pimgtpnf2f
  12. pimgtpnf2
  13. salpreimagelt
  14. pimrecltpos
  15. salpreimalegt
  16. pimiooltgt
  17. preimaicomnf
  18. pimltpnf2f
  19. pimltpnf2
  20. pimgtmnf2
  21. pimdecfgtioc
  22. pimincfltioc
  23. pimdecfgtioo
  24. pimincfltioo
  25. preimaioomnf
  26. preimageiingt
  27. preimaleiinlt
  28. pimgtmnff
  29. pimgtmnf
  30. pimrecltneg
  31. salpreimagtge
  32. salpreimaltle
  33. issmflem
  34. issmf
  35. salpreimalelt
  36. salpreimagtlt
  37. smfpreimalt
  38. smff
  39. smfdmss
  40. issmff
  41. issmfd
  42. smfpreimaltf
  43. issmfdf
  44. sssmf
  45. mbfresmf
  46. cnfsmf
  47. incsmflem
  48. incsmf
  49. smfsssmf
  50. issmflelem
  51. issmfle
  52. smfpimltmpt
  53. smfpimltxr
  54. issmfdmpt
  55. smfconst
  56. sssmfmpt
  57. cnfrrnsmf
  58. smfid
  59. bormflebmf
  60. smfpreimale
  61. issmfgtlem
  62. issmfgt
  63. issmfled
  64. smfpimltxrmptf
  65. smfpimltxrmpt
  66. smfmbfcex
  67. issmfgtd
  68. smfpreimagt
  69. smfaddlem1
  70. smfaddlem2
  71. smfadd
  72. decsmflem
  73. decsmf
  74. smfpreimagtf
  75. issmfgelem
  76. issmfge
  77. smflimlem1
  78. smflimlem2
  79. smflimlem3
  80. smflimlem4
  81. smflimlem5
  82. smflimlem6
  83. smflim
  84. nsssmfmbflem
  85. nsssmfmbf
  86. smfpimgtxr
  87. smfpimgtmpt
  88. smfpreimage
  89. mbfpsssmf
  90. smfpimgtxrmptf
  91. smfpimgtxrmpt
  92. smfpimioompt
  93. smfpimioo
  94. smfresal
  95. smfrec
  96. smfres
  97. smfmullem1
  98. smfmullem2
  99. smfmullem3
  100. smfmullem4
  101. smfmul
  102. smfmulc1
  103. smfdiv
  104. smfpimbor1lem1
  105. smfpimbor1lem2
  106. smfpimbor1
  107. smf2id
  108. smfco
  109. smfneg
  110. smffmptf
  111. smffmpt
  112. smflim2
  113. smfpimcclem
  114. smfpimcc
  115. issmfle2d
  116. smflimmpt
  117. smfsuplem1
  118. smfsuplem2
  119. smfsuplem3
  120. smfsup
  121. smfsupmpt
  122. smfsupxr
  123. smfinflem
  124. smfinf
  125. smfinfmpt
  126. smflimsuplem1
  127. smflimsuplem2
  128. smflimsuplem3
  129. smflimsuplem4
  130. smflimsuplem5
  131. smflimsuplem6
  132. smflimsuplem7
  133. smflimsuplem8
  134. smflimsup
  135. smflimsupmpt
  136. smfliminflem
  137. smfliminf
  138. smfliminfmpt
  139. adddmmbl
  140. adddmmbl2
  141. muldmmbl
  142. muldmmbl2
  143. smfdmmblpimne
  144. smfdivdmmbl
  145. smfpimne
  146. smfpimne2
  147. smfdivdmmbl2
  148. fsupdm
  149. fsupdm2
  150. smfsupdmmbllem
  151. smfsupdmmbl
  152. finfdm
  153. finfdm2
  154. smfinfdmmbllem
  155. smfinfdmmbl