Definition df-itgm 30415

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 23392.

(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

Step	Hyp	Ref	Expression
1		citgm 30389	. 2 class itgm
2		vw	. . 3 setvar w
3		vm	. . 3 setvar m
4		cvv 3200	. . 3 class _V
5		cmeas 30258	. . . . 5 class measures
6	5	crn 5115	. . . 4 class ran measures
7	6	cuni 4436	. . 3 class U. ran measures
8	2	cv 1482	. . . . 5 class w
9	3	cv 1482	. . . . 5 class m
10		csitg 30391	. . . . 5 class sitg
11	8, 9, 10	co 6650	. . . 4 class ( wsitg m )
12		csitm 30390	. . . . . . 7 class sitm
13	8, 9, 12	co 6650	. . . . . 6 class ( wsitm m )
14		cmetu 19737	. . . . . 6 class metUnif
15	13, 14	cfv 5888	. . . . 5 class (metUnif ` ( wsitm m ) )
16		cuss 22057	. . . . . 6 class UnifSt
17	8, 16	cfv 5888	. . . . 5 class (UnifSt ` w )
18		ccnext 21863	. . . . 5 class CnExt
19	15, 17, 18	co 6650	. . . 4 class ( (metUnif ` ( wsitm m ) )CnExt (UnifSt ` w ) )
20	11, 19	cfv 5888	. . 3 class ( ( (metUnif ` ( wsitm m ) )CnExt (UnifSt ` w ) ) ` ( wsitg m ) )
21	2, 3, 4, 7, 20	cmpt2 6652	. 2 class ( w e. _V , m e. U. ran measures |-> ( ( (metUnif ` ( wsitm m ) )CnExt (UnifSt ` w ) ) ` ( wsitg m ) ) )
22	1, 21	wceq 1483	1 wff itgm = ( w e. _V , m e. U. ran measures |-> ( ( (metUnif ` ( wsitm m ) )CnExt (UnifSt ` w ) ) ` ( wsitg m ) ) )

This definition is referenced by: (None)