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 32160
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 32159 . 2 class measures
2 vs . . 3 setvar 𝑠
3 csiga 32072 . . . . 5 class sigAlgebra
43crn 5591 . . . 4 class ran sigAlgebra
54cuni 4845 . . 3 class ran sigAlgebra
62cv 1541 . . . . . 6 class 𝑠
7 cc0 10872 . . . . . . 7 class 0
8 cpnf 11007 . . . . . . 7 class +∞
9 cicc 13081 . . . . . . 7 class [,]
107, 8, 9co 7271 . . . . . 6 class (0[,]+∞)
11 vm . . . . . . 7 setvar 𝑚
1211cv 1541 . . . . . 6 class 𝑚
136, 10, 12wf 6428 . . . . 5 wff 𝑚:𝑠⟶(0[,]+∞)
14 c0 4262 . . . . . . 7 class
1514, 12cfv 6432 . . . . . 6 class (𝑚‘∅)
1615, 7wceq 1542 . . . . 5 wff (𝑚‘∅) = 0
17 vx . . . . . . . . . 10 setvar 𝑥
1817cv 1541 . . . . . . . . 9 class 𝑥
19 com 7706 . . . . . . . . 9 class ω
20 cdom 8714 . . . . . . . . 9 class
2118, 19, 20wbr 5079 . . . . . . . 8 wff 𝑥 ≼ ω
22 vy . . . . . . . . 9 setvar 𝑦
2322cv 1541 . . . . . . . . 9 class 𝑦
2422, 18, 23wdisj 5044 . . . . . . . 8 wff Disj 𝑦𝑥 𝑦
2521, 24wa 396 . . . . . . 7 wff (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)
2618cuni 4845 . . . . . . . . 9 class 𝑥
2726, 12cfv 6432 . . . . . . . 8 class (𝑚 𝑥)
2823, 12cfv 6432 . . . . . . . . 9 class (𝑚𝑦)
2918, 28, 22cesum 31991 . . . . . . . 8 class Σ*𝑦𝑥(𝑚𝑦)
3027, 29wceq 1542 . . . . . . 7 wff (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)
3125, 30wi 4 . . . . . 6 wff ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦))
326cpw 4539 . . . . . 6 class 𝒫 𝑠
3331, 17, 32wral 3066 . . . . 5 wff 𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦))
3413, 16, 33w3a 1086 . . . 4 wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))
3534, 11cab 2717 . . 3 class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))}
362, 5, 35cmpt 5162 . 2 class (𝑠 ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))})
371, 36wceq 1542 1 wff measures = (𝑠 ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))})
Colors of variables: wff setvar class
This definition is referenced by:  measbase  32161  measval  32162  ismeas  32163  isrnmeas  32164  measbasedom  32166
  Copyright terms: Public domain W3C validator