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

Definition df-itgm 26881
Description: Define the Bochner integral as the extension by continuity of the Bochnel integral for simple functions.

Bogachev first defines 'fundamental in the mean' sequences, in definition 2.3.1 of [Bogachev] p. 116, and notes that those are actually Cauchy sequences for the pseudometric  ( wsitm m ).

He then defines the Bochner integral in chapter 2.4.4 in [Bogachev] p. 118. The definition of the Lebesgue integral, df-itg 21237.

(Contributed by Thierry Arnoux, 13-Feb-2018.)

Assertion
Ref Expression
df-itgm  |- itgm  =  ( w  e.  _V ,  m  e.  U. ran measures  |->  ( ( (metUnif `  ( wsitm m ) )CnExt (UnifSt `  w ) ) `  ( wsitg m ) ) )
Distinct variable group:    w, m

Detailed syntax breakdown of Definition df-itgm
StepHypRef Expression
1 citgm 26858 . 2  class itgm
2 vw . . 3  setvar  w
3 vm . . 3  setvar  m
4 cvv 3078 . . 3  class  _V
5 cmeas 26755 . . . . 5  class measures
65crn 4950 . . . 4  class  ran measures
76cuni 4200 . . 3  class  U. ran measures
82cv 1369 . . . . 5  class  w
93cv 1369 . . . . 5  class  m
10 csitg 26860 . . . . 5  class sitg
118, 9, 10co 6201 . . . 4  class  ( wsitg m )
12 csitm 26859 . . . . . . 7  class sitm
138, 9, 12co 6201 . . . . . 6  class  ( wsitm m )
14 cmetu 17934 . . . . . 6  class metUnif
1513, 14cfv 5527 . . . . 5  class  (metUnif `  (
wsitm m ) )
16 cuss 19961 . . . . . 6  class UnifSt
178, 16cfv 5527 . . . . 5  class  (UnifSt `  w )
18 ccnext 19764 . . . . 5  class CnExt
1915, 17, 18co 6201 . . . 4  class  ( (metUnif `  ( wsitm m ) )CnExt (UnifSt `  w )
)
2011, 19cfv 5527 . . 3  class  ( ( (metUnif `  ( wsitm m ) )CnExt (UnifSt `  w ) ) `  ( wsitg m ) )
212, 3, 4, 7, 20cmpt2 6203 . 2  class  ( w  e.  _V ,  m  e.  U. ran measures  |->  ( (
(metUnif `  ( wsitm m
) )CnExt (UnifSt `  w ) ) `  ( wsitg m ) ) )
221, 21wceq 1370 1  wff itgm  =  ( w  e.  _V ,  m  e.  U. ran measures  |->  ( ( (metUnif `  ( wsitm m ) )CnExt (UnifSt `  w ) ) `  ( wsitg m ) ) )
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator