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

Definition df-itgm 29544
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 (𝑤sitm𝑚).

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

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

Assertion
Ref Expression
df-itgm itgm = (𝑤 ∈ V, 𝑚 ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚)))
Distinct variable group:   𝑤,𝑚

Detailed syntax breakdown of Definition df-itgm
StepHypRef Expression
1 citgm 29518 . 2 class itgm
2 vw . . 3 setvar 𝑤
3 vm . . 3 setvar 𝑚
4 cvv 3168 . . 3 class V
5 cmeas 29387 . . . . 5 class measures
65crn 5025 . . . 4 class ran measures
76cuni 4362 . . 3 class ran measures
82cv 1473 . . . . 5 class 𝑤
93cv 1473 . . . . 5 class 𝑚
10 csitg 29520 . . . . 5 class sitg
118, 9, 10co 6523 . . . 4 class (𝑤sitg𝑚)
12 csitm 29519 . . . . . . 7 class sitm
138, 9, 12co 6523 . . . . . 6 class (𝑤sitm𝑚)
14 cmetu 19500 . . . . . 6 class metUnif
1513, 14cfv 5786 . . . . 5 class (metUnif‘(𝑤sitm𝑚))
16 cuss 21805 . . . . . 6 class UnifSt
178, 16cfv 5786 . . . . 5 class (UnifSt‘𝑤)
18 ccnext 21611 . . . . 5 class CnExt
1915, 17, 18co 6523 . . . 4 class ((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))
2011, 19cfv 5786 . . 3 class (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚))
212, 3, 4, 7, 20cmpt2 6525 . 2 class (𝑤 ∈ V, 𝑚 ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚)))
221, 21wceq 1474 1 wff itgm = (𝑤 ∈ V, 𝑚 ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚)))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator