Definition df-itgm

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 ( w sitm m ) .

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

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

	Ref	Expression
Assertion	df-itgm	|- itgm = ( w e. _V , m e. U. ran measures |-> ( ( ( metUnif ` ( w sitm m ) ) CnExt ( UnifSt ` w ) ) ` ( w sitg m ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		citgm	|- itgm
1		vw	|- w
2		cvv	|- _V
3		vm	|- m
4		cmeas	|- measures
5	4	crn	|- ran measures
6	5	cuni	|- U. ran measures
7		cmetu	|- metUnif
8	1	cv	|- w
9		csitm	|- sitm
10	3	cv	|- m
11	8 10 9	co	|- ( w sitm m )
12	11 7	cfv	|- ( metUnif ` ( w sitm m ) )
13		ccnext	|- CnExt
14		cuss	|- UnifSt
15	8 14	cfv	|- ( UnifSt ` w )
16	12 15 13	co	|- ( ( metUnif ` ( w sitm m ) ) CnExt ( UnifSt ` w ) )
17		csitg	|- sitg
18	8 10 17	co	|- ( w sitg m )
19	18 16	cfv	|- ( ( ( metUnif ` ( w sitm m ) ) CnExt ( UnifSt ` w ) ) ` ( w sitg m ) )
20	1 3 2 6 19	cmpo	|- ( w e. _V , m e. U. ran measures |-> ( ( ( metUnif ` ( w sitm m ) ) CnExt ( UnifSt ` w ) ) ` ( w sitg m ) ) )
21	0 20	wceq	|- itgm = ( w e. _V , m e. U. ran measures |-> ( ( ( metUnif ` ( w sitm m ) ) CnExt ( UnifSt ` w ) ) ` ( w sitg m ) ) )