Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sitm Structured version   Visualization version   GIF version

Definition df-sitm 33330
Description: Define the integral metric for simple functions, as the integral of the distances between the function values. Since distances take nonnegative values in ℝ*, the range structure for this integral is (ℝ*𝑠 β†Ύs (0[,]+∞)). See definition 2.3.1 of [Bogachev] p. 116. (Contributed by Thierry Arnoux, 22-Oct-2017.)
Assertion
Ref Expression
df-sitm sitm = (𝑀 ∈ V, π‘š ∈ βˆͺ ran measures ↦ (𝑓 ∈ dom (𝑀sitgπ‘š), 𝑔 ∈ dom (𝑀sitgπ‘š) ↦ (((ℝ*𝑠 β†Ύs (0[,]+∞))sitgπ‘š)β€˜(𝑓 ∘f (distβ€˜π‘€)𝑔))))
Distinct variable group:   𝑓,𝑔,π‘š,𝑀

Detailed syntax breakdown of Definition df-sitm
StepHypRef Expression
1 csitm 33327 . 2 class sitm
2 vw . . 3 setvar 𝑀
3 vm . . 3 setvar π‘š
4 cvv 3475 . . 3 class V
5 cmeas 33193 . . . . 5 class measures
65crn 5678 . . . 4 class ran measures
76cuni 4909 . . 3 class βˆͺ ran measures
8 vf . . . 4 setvar 𝑓
9 vg . . . 4 setvar 𝑔
102cv 1541 . . . . . 6 class 𝑀
113cv 1541 . . . . . 6 class π‘š
12 csitg 33328 . . . . . 6 class sitg
1310, 11, 12co 7409 . . . . 5 class (𝑀sitgπ‘š)
1413cdm 5677 . . . 4 class dom (𝑀sitgπ‘š)
158cv 1541 . . . . . 6 class 𝑓
169cv 1541 . . . . . 6 class 𝑔
17 cds 17206 . . . . . . . 8 class dist
1810, 17cfv 6544 . . . . . . 7 class (distβ€˜π‘€)
1918cof 7668 . . . . . 6 class ∘f (distβ€˜π‘€)
2015, 16, 19co 7409 . . . . 5 class (𝑓 ∘f (distβ€˜π‘€)𝑔)
21 cxrs 17446 . . . . . . 7 class ℝ*𝑠
22 cc0 11110 . . . . . . . 8 class 0
23 cpnf 11245 . . . . . . . 8 class +∞
24 cicc 13327 . . . . . . . 8 class [,]
2522, 23, 24co 7409 . . . . . . 7 class (0[,]+∞)
26 cress 17173 . . . . . . 7 class β†Ύs
2721, 25, 26co 7409 . . . . . 6 class (ℝ*𝑠 β†Ύs (0[,]+∞))
2827, 11, 12co 7409 . . . . 5 class ((ℝ*𝑠 β†Ύs (0[,]+∞))sitgπ‘š)
2920, 28cfv 6544 . . . 4 class (((ℝ*𝑠 β†Ύs (0[,]+∞))sitgπ‘š)β€˜(𝑓 ∘f (distβ€˜π‘€)𝑔))
308, 9, 14, 14, 29cmpo 7411 . . 3 class (𝑓 ∈ dom (𝑀sitgπ‘š), 𝑔 ∈ dom (𝑀sitgπ‘š) ↦ (((ℝ*𝑠 β†Ύs (0[,]+∞))sitgπ‘š)β€˜(𝑓 ∘f (distβ€˜π‘€)𝑔)))
312, 3, 4, 7, 30cmpo 7411 . 2 class (𝑀 ∈ V, π‘š ∈ βˆͺ ran measures ↦ (𝑓 ∈ dom (𝑀sitgπ‘š), 𝑔 ∈ dom (𝑀sitgπ‘š) ↦ (((ℝ*𝑠 β†Ύs (0[,]+∞))sitgπ‘š)β€˜(𝑓 ∘f (distβ€˜π‘€)𝑔))))
321, 31wceq 1542 1 wff sitm = (𝑀 ∈ V, π‘š ∈ βˆͺ ran measures ↦ (𝑓 ∈ dom (𝑀sitgπ‘š), 𝑔 ∈ dom (𝑀sitgπ‘š) ↦ (((ℝ*𝑠 β†Ύs (0[,]+∞))sitgπ‘š)β€˜(𝑓 ∘f (distβ€˜π‘€)𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  sitmval  33348
  Copyright terms: Public domain W3C validator