df-sitm

Description: Define the integral metric for simple functions, as the integral of the distances between the function values. Since distances take nonnegative values in RR* , the range structure for this integral is ` ( RR*s |``s ( 0 , +oo ) ) ` . See definition 2.3.1 of Bogachev p. 116. (Contributed by Thierry Arnoux, 22-Oct-2017)

		Ref	Expression
	Assertion	df-sitm	$⊢ sitm = (w \in V, m \in ⋃ ran measures ⟼ (f \in ℑ_{m}^{w}, g \in ℑ_{m}^{w} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (w)}_{f} g) d m))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csitm	$class sitm$
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		vf	$setvar f$
8	1	cv	$setvar w$
9		csitg	$class sitg$
10	3	cv	$setvar m$
11	8 10 9	co	$class (w sitg m)$
12	11	cdm	$class ℑ_{m}^{w}$
13		vg	$setvar g$
14		cxrs	$class ℝ_{𝑠}^{*}$
15		cress	$class ↾_{𝑠}$
16		cc0	$class 0$
17		cicc	$class [.]$
18		cpnf	$class +∞$
19	16 18 17	co	$class [0, +∞]$
20	14 19 15	co	$class (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
21	20 10 9	co	$class ((ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]) sitg m)$
22	7	cv	$setvar f$
23		cds	$class dist$
24	8 23	cfv	$class dist (w)$
25	24	cof	$class \circ_{f} dist (w)$
26	13	cv	$setvar g$
27	22 26 25	co	$class (f {dist (w)}_{f} g)$
28	27 21	cfv	$class \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (w)}_{f} g) d m$
29	7 13 12 12 28	cmpo	$class (f \in ℑ_{m}^{w}, g \in ℑ_{m}^{w} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (w)}_{f} g) d m)$
30	1 3 2 6 29	cmpo	$class (w \in V, m \in ⋃ ran measures ⟼ (f \in ℑ_{m}^{w}, g \in ℑ_{m}^{w} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (w)}_{f} g) d m))$
31	0 30	wceq	$wff sitm = (w \in V, m \in ⋃ ran measures ⟼ (f \in ℑ_{m}^{w}, g \in ℑ_{m}^{w} ⟼ \int_{ℑ}^{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} (f {dist (w)}_{f} g) d m))$

Metamath Proof Explorer

Definition df-sitm

Detailed syntax breakdown