Definition df-itgm 32620

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

(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

Step	Hyp	Ref	Expression
1		citgm 32594	. 2 class itgm
2		vw	. . 3 setvar 𝑤
3		vm	. . 3 setvar 𝑚
4		cvv 3441	. . 3 class V
5		cmeas 32461	. . . . 5 class measures
6	5	crn 5621	. . . 4 class ran measures
7	6	cuni 4852	. . 3 class ∪ ran measures
8	2	cv 1539	. . . . 5 class 𝑤
9	3	cv 1539	. . . . 5 class 𝑚
10		csitg 32596	. . . . 5 class sitg
11	8, 9, 10	co 7337	. . . 4 class (𝑤sitg𝑚)
12		csitm 32595	. . . . . . 7 class sitm
13	8, 9, 12	co 7337	. . . . . 6 class (𝑤sitm𝑚)
14		cmetu 20694	. . . . . 6 class metUnif
15	13, 14	cfv 6479	. . . . 5 class (metUnif‘(𝑤sitm𝑚))
16		cuss 23511	. . . . . 6 class UnifSt
17	8, 16	cfv 6479	. . . . 5 class (UnifSt‘𝑤)
18		ccnext 23316	. . . . 5 class CnExt
19	15, 17, 18	co 7337	. . . 4 class ((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))
20	11, 19	cfv 6479	. . 3 class (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚))
21	2, 3, 4, 7, 20	cmpo 7339	. 2 class (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚)))
22	1, 21	wceq 1540	1 wff itgm = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚)))

This definition is referenced by: (None)