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 .

		Ref	Expression
	Assertion	df-itgm	$⊢ itgm = (w \in V, m \in ⋃ ran measures ⟼ (metUnif (w sitm m) CnExt UnifSt (w)) (w sitg m))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		citgm	$class itgm$
1		vw	$setvar w$
2		cvv	$class V$
3		vm	$setvar m$
4		cmeas	$class measures$
5	4	crn	$class ran measures$
6	5	cuni	$class ⋃ ran measures$
7		cmetu	$class metUnif$
8	1	cv	$setvar w$
9		csitm	$class sitm$
10	3	cv	$setvar m$
11	8 10 9	co	$class {\| . - . \|}_{m}^{w}$
12	11 7	cfv	$class metUnif (w sitm m)$
13		ccnext	$class CnExt$
14		cuss	$class UnifSt$
15	8 14	cfv	$class UnifSt (w)$
16	12 15 13	co	$class (metUnif (w sitm m) CnExt UnifSt (w))$
17		csitg	$class sitg$
18	8 10 17	co	$class (w sitg m)$
19	18 16	cfv	$class (metUnif (w sitm m) CnExt UnifSt (w)) (w sitg m)$
20	1 3 2 6 19	cmpo	$class (w \in V, m \in ⋃ ran measures ⟼ (metUnif (w sitm m) CnExt UnifSt (w)) (w sitg m))$
21	0 20	wceq	$wff itgm = (w \in V, m \in ⋃ ran measures ⟼ (metUnif (w sitm m) CnExt UnifSt (w)) (w sitg m))$

Metamath Proof Explorer

Definition df-itgm

Detailed syntax breakdown