Metamath Proof Explorer


Definition df-mbfm

Description: Define the measurable function builder, which generates the set of measurable functions from a measurable space to another one. Here, the measurable spaces are given using their sigma-algebras s and t , and the spaces themselves are recovered by U. s and U. t .

Note the similarities between the definition of measurable functions in measure theory, and of continuous functions in topology.

This is the definition for the generic measure theory. For the specific case of functions from RR to CC , see df-mbf . (Contributed by Thierry Arnoux, 23-Jan-2017)

Ref Expression
Assertion df-mbfm MblFnμ=sransigAlgebra,transigAlgebrafts|xtf-1xs

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmbfm classMblFnμ
1 vs setvars
2 csiga classsigAlgebra
3 2 crn classransigAlgebra
4 3 cuni classransigAlgebra
5 vt setvart
6 vf setvarf
7 5 cv setvart
8 7 cuni classt
9 cmap class𝑚
10 1 cv setvars
11 10 cuni classs
12 8 11 9 co classts
13 vx setvarx
14 6 cv setvarf
15 14 ccnv classf-1
16 13 cv setvarx
17 15 16 cima classf-1x
18 17 10 wcel wfff-1xs
19 18 13 7 wral wffxtf-1xs
20 19 6 12 crab classfts|xtf-1xs
21 1 5 4 4 20 cmpo classsransigAlgebra,transigAlgebrafts|xtf-1xs
22 0 21 wceq wffMblFnμ=sransigAlgebra,transigAlgebrafts|xtf-1xs