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 32993
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 25003.

(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 32967 . 2 class itgm
2 vw . . 3 setvar 𝑀
3 vm . . 3 setvar π‘š
4 cvv 3448 . . 3 class V
5 cmeas 32834 . . . . 5 class measures
65crn 5639 . . . 4 class ran measures
76cuni 4870 . . 3 class βˆͺ ran measures
82cv 1541 . . . . 5 class 𝑀
93cv 1541 . . . . 5 class π‘š
10 csitg 32969 . . . . 5 class sitg
118, 9, 10co 7362 . . . 4 class (𝑀sitgπ‘š)
12 csitm 32968 . . . . . . 7 class sitm
138, 9, 12co 7362 . . . . . 6 class (𝑀sitmπ‘š)
14 cmetu 20803 . . . . . 6 class metUnif
1513, 14cfv 6501 . . . . 5 class (metUnifβ€˜(𝑀sitmπ‘š))
16 cuss 23621 . . . . . 6 class UnifSt
178, 16cfv 6501 . . . . 5 class (UnifStβ€˜π‘€)
18 ccnext 23426 . . . . 5 class CnExt
1915, 17, 18co 7362 . . . 4 class ((metUnifβ€˜(𝑀sitmπ‘š))CnExt(UnifStβ€˜π‘€))
2011, 19cfv 6501 . . 3 class (((metUnifβ€˜(𝑀sitmπ‘š))CnExt(UnifStβ€˜π‘€))β€˜(𝑀sitgπ‘š))
212, 3, 4, 7, 20cmpo 7364 . 2 class (𝑀 ∈ V, π‘š ∈ βˆͺ ran measures ↦ (((metUnifβ€˜(𝑀sitmπ‘š))CnExt(UnifStβ€˜π‘€))β€˜(𝑀sitgπ‘š)))
221, 21wceq 1542 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