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 29392
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 29391 . 2 class measures
2 vs . . 3 setvar 𝑠
3 csiga 29303 . . . . 5 class sigAlgebra
43crn 5029 . . . 4 class ran sigAlgebra
54cuni 4366 . . 3 class ran sigAlgebra
62cv 1473 . . . . . 6 class 𝑠
7 cc0 9792 . . . . . . 7 class 0
8 cpnf 9927 . . . . . . 7 class +∞
9 cicc 12005 . . . . . . 7 class [,]
107, 8, 9co 6527 . . . . . 6 class (0[,]+∞)
11 vm . . . . . . 7 setvar 𝑚
1211cv 1473 . . . . . 6 class 𝑚
136, 10, 12wf 5786 . . . . 5 wff 𝑚:𝑠⟶(0[,]+∞)
14 c0 3873 . . . . . . 7 class
1514, 12cfv 5790 . . . . . 6 class (𝑚‘∅)
1615, 7wceq 1474 . . . . 5 wff (𝑚‘∅) = 0
17 vx . . . . . . . . . 10 setvar 𝑥
1817cv 1473 . . . . . . . . 9 class 𝑥
19 com 6934 . . . . . . . . 9 class ω
20 cdom 7816 . . . . . . . . 9 class
2118, 19, 20wbr 4577 . . . . . . . 8 wff 𝑥 ≼ ω
22 vy . . . . . . . . 9 setvar 𝑦
2322cv 1473 . . . . . . . . 9 class 𝑦
2422, 18, 23wdisj 4547 . . . . . . . 8 wff Disj 𝑦𝑥 𝑦
2521, 24wa 382 . . . . . . 7 wff (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)
2618cuni 4366 . . . . . . . . 9 class 𝑥
2726, 12cfv 5790 . . . . . . . 8 class (𝑚 𝑥)
2823, 12cfv 5790 . . . . . . . . 9 class (𝑚𝑦)
2918, 28, 22cesum 29222 . . . . . . . 8 class Σ*𝑦𝑥(𝑚𝑦)
3027, 29wceq 1474 . . . . . . 7 wff (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)
3125, 30wi 4 . . . . . 6 wff ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦))
326cpw 4107 . . . . . 6 class 𝒫 𝑠
3331, 17, 32wral 2895 . . . . 5 wff 𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦))
3413, 16, 33w3a 1030 . . . 4 wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))
3534, 11cab 2595 . . 3 class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))}
362, 5, 35cmpt 4637 . 2 class (𝑠 ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))})
371, 36wceq 1474 1 wff measures = (𝑠 ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))})
Colors of variables: wff setvar class
This definition is referenced by:  measbase  29393  measval  29394  ismeas  29395  isrnmeas  29396  measbasedom  29398
  Copyright terms: Public domain W3C validator