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

Definition df-meas 31459
Description: Define a measure as a nonnegative countably additive function over a sigma-algebra onto (0[,]+∞). (Contributed by Thierry Arnoux, 10-Sep-2016.)
Assertion
Ref Expression
df-meas measures = (𝑠 ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))})
Distinct variable group:   𝑥,𝑚,𝑦,𝑠

Detailed syntax breakdown of Definition df-meas
StepHypRef Expression
1 cmeas 31458 . 2 class measures
2 vs . . 3 setvar 𝑠
3 csiga 31371 . . . . 5 class sigAlgebra
43crn 5528 . . . 4 class ran sigAlgebra
54cuni 4810 . . 3 class ran sigAlgebra
62cv 1536 . . . . . 6 class 𝑠
7 cc0 10511 . . . . . . 7 class 0
8 cpnf 10646 . . . . . . 7 class +∞
9 cicc 12716 . . . . . . 7 class [,]
107, 8, 9co 7129 . . . . . 6 class (0[,]+∞)
11 vm . . . . . . 7 setvar 𝑚
1211cv 1536 . . . . . 6 class 𝑚
136, 10, 12wf 6323 . . . . 5 wff 𝑚:𝑠⟶(0[,]+∞)
14 c0 4265 . . . . . . 7 class
1514, 12cfv 6327 . . . . . 6 class (𝑚‘∅)
1615, 7wceq 1537 . . . . 5 wff (𝑚‘∅) = 0
17 vx . . . . . . . . . 10 setvar 𝑥
1817cv 1536 . . . . . . . . 9 class 𝑥
19 com 7554 . . . . . . . . 9 class ω
20 cdom 8481 . . . . . . . . 9 class
2118, 19, 20wbr 5038 . . . . . . . 8 wff 𝑥 ≼ ω
22 vy . . . . . . . . 9 setvar 𝑦
2322cv 1536 . . . . . . . . 9 class 𝑦
2422, 18, 23wdisj 5003 . . . . . . . 8 wff Disj 𝑦𝑥 𝑦
2521, 24wa 398 . . . . . . 7 wff (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)
2618cuni 4810 . . . . . . . . 9 class 𝑥
2726, 12cfv 6327 . . . . . . . 8 class (𝑚 𝑥)
2823, 12cfv 6327 . . . . . . . . 9 class (𝑚𝑦)
2918, 28, 22cesum 31290 . . . . . . . 8 class Σ*𝑦𝑥(𝑚𝑦)
3027, 29wceq 1537 . . . . . . 7 wff (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)
3125, 30wi 4 . . . . . 6 wff ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦))
326cpw 4511 . . . . . 6 class 𝒫 𝑠
3331, 17, 32wral 3125 . . . . 5 wff 𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦))
3413, 16, 33w3a 1083 . . . 4 wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))
3534, 11cab 2798 . . 3 class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))}
362, 5, 35cmpt 5118 . 2 class (𝑠 ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))})
371, 36wceq 1537 1 wff measures = (𝑠 ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))})
Colors of variables: wff setvar class
This definition is referenced by:  measbase  31460  measval  31461  ismeas  31462  isrnmeas  31463  measbasedom  31465
  Copyright terms: Public domain W3C validator