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 28556
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 22198.

(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 28533 . 2  class itgm
2 vw . . 3  setvar  w
3 vm . . 3  setvar  m
4 cvv 3106 . . 3  class  _V
5 cmeas 28403 . . . . 5  class measures
65crn 4989 . . . 4  class  ran measures
76cuni 4235 . . 3  class  U. ran measures
82cv 1397 . . . . 5  class  w
93cv 1397 . . . . 5  class  m
10 csitg 28535 . . . . 5  class sitg
118, 9, 10co 6270 . . . 4  class  ( wsitg m )
12 csitm 28534 . . . . . . 7  class sitm
138, 9, 12co 6270 . . . . . 6  class  ( wsitm m )
14 cmetu 18605 . . . . . 6  class metUnif
1513, 14cfv 5570 . . . . 5  class  (metUnif `  (
wsitm m ) )
16 cuss 20922 . . . . . 6  class UnifSt
178, 16cfv 5570 . . . . 5  class  (UnifSt `  w )
18 ccnext 20725 . . . . 5  class CnExt
1915, 17, 18co 6270 . . . 4  class  ( (metUnif `  ( wsitm m ) )CnExt (UnifSt `  w )
)
2011, 19cfv 5570 . . 3  class  ( ( (metUnif `  ( wsitm m ) )CnExt (UnifSt `  w ) ) `  ( wsitg m ) )
212, 3, 4, 7, 20cmpt2 6272 . 2  class  ( w  e.  _V ,  m  e.  U. ran measures  |->  ( (
(metUnif `  ( wsitm m
) )CnExt (UnifSt `  w ) ) `  ( wsitg m ) ) )
221, 21wceq 1398 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