Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sitg Structured version   Unicode version

Definition df-sitg 29032
 Description: Define the integral of simple functions from a measurable space to a generic space equipped with the right scalar product. will later be required to be a Banach space. These simple functions are required to take finitely many different values: this is expressed by in the definition. Moreover, for each , the pre-image is requested to be measurable, of finite measure. In this definition, sigaGen is the Borel sigma-algebra on , and the functions range over the measurable functions over that Borel algebra. Definition 2.4.1 of [Bogachev] p. 118. (Contributed by Thierry Arnoux, 21-Oct-2017.)
Assertion
Ref Expression
df-sitg sitg measures MblFnMsigaGen g RRHomScalar
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-sitg
StepHypRef Expression
1 csitg 29031 . 2 sitg
2 vw . . 3
3 vm . . 3
4 cvv 3078 . . 3
5 cmeas 28897 . . . . 5 measures
65crn 4846 . . . 4 measures
76cuni 4213 . . 3 measures
8 vf . . . 4
9 vg . . . . . . . . 9
109cv 1436 . . . . . . . 8
1110crn 4846 . . . . . . 7
12 cfn 7568 . . . . . . 7
1311, 12wcel 1867 . . . . . 6
1410ccnv 4844 . . . . . . . . . 10
15 vx . . . . . . . . . . . 12
1615cv 1436 . . . . . . . . . . 11
1716csn 3993 . . . . . . . . . 10
1814, 17cima 4848 . . . . . . . . 9
193cv 1436 . . . . . . . . 9
2018, 19cfv 5592 . . . . . . . 8
21 cc0 9528 . . . . . . . . 9
22 cpnf 9661 . . . . . . . . 9
23 cico 11626 . . . . . . . . 9
2421, 22, 23co 6296 . . . . . . . 8
2520, 24wcel 1867 . . . . . . 7
262cv 1436 . . . . . . . . . 10
27 c0g 15298 . . . . . . . . . 10
2826, 27cfv 5592 . . . . . . . . 9
2928csn 3993 . . . . . . . 8
3011, 29cdif 3430 . . . . . . 7
3125, 15, 30wral 2773 . . . . . 6
3213, 31wa 370 . . . . 5
3319cdm 4845 . . . . . 6
34 ctopn 15280 . . . . . . . 8
3526, 34cfv 5592 . . . . . . 7
36 csigagen 28840 . . . . . . 7 sigaGen
3735, 36cfv 5592 . . . . . 6 sigaGen
38 cmbfm 28952 . . . . . 6 MblFnM
3933, 37, 38co 6296 . . . . 5 MblFnMsigaGen
4032, 9, 39crab 2777 . . . 4 MblFnMsigaGen
418cv 1436 . . . . . . . 8
4241crn 4846 . . . . . . 7
4342, 29cdif 3430 . . . . . 6
4441ccnv 4844 . . . . . . . . . 10
4544, 17cima 4848 . . . . . . . . 9
4645, 19cfv 5592 . . . . . . . 8
47 csca 15153 . . . . . . . . . 10 Scalar
4826, 47cfv 5592 . . . . . . . . 9 Scalar
49 crrh 28677 . . . . . . . . 9 RRHom
5048, 49cfv 5592 . . . . . . . 8 RRHomScalar
5146, 50cfv 5592 . . . . . . 7 RRHomScalar
52 cvsca 15154 . . . . . . . 8
5326, 52cfv 5592 . . . . . . 7
5451, 16, 53co 6296 . . . . . 6 RRHomScalar
5515, 43, 54cmpt 4475 . . . . 5 RRHomScalar
56 cgsu 15299 . . . . 5 g
5726, 55, 56co 6296 . . . 4 g RRHomScalar
588, 40, 57cmpt 4475 . . 3 MblFnMsigaGen g RRHomScalar
592, 3, 4, 7, 58cmpt2 6298 . 2 measures MblFnMsigaGen g RRHomScalar
601, 59wceq 1437 1 sitg measures MblFnMsigaGen g RRHomScalar
 Colors of variables: wff setvar class This definition is referenced by:  sitgval  29034
 Copyright terms: Public domain W3C validator