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 30568
 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 30567 . 2 class measures
2 vs . . 3 setvar 𝑠
3 csiga 30479 . . . . 5 class sigAlgebra
43crn 5267 . . . 4 class ran sigAlgebra
54cuni 4588 . . 3 class ran sigAlgebra
62cv 1631 . . . . . 6 class 𝑠
7 cc0 10128 . . . . . . 7 class 0
8 cpnf 10263 . . . . . . 7 class +∞
9 cicc 12371 . . . . . . 7 class [,]
107, 8, 9co 6813 . . . . . 6 class (0[,]+∞)
11 vm . . . . . . 7 setvar 𝑚
1211cv 1631 . . . . . 6 class 𝑚
136, 10, 12wf 6045 . . . . 5 wff 𝑚:𝑠⟶(0[,]+∞)
14 c0 4058 . . . . . . 7 class
1514, 12cfv 6049 . . . . . 6 class (𝑚‘∅)
1615, 7wceq 1632 . . . . 5 wff (𝑚‘∅) = 0
17 vx . . . . . . . . . 10 setvar 𝑥
1817cv 1631 . . . . . . . . 9 class 𝑥
19 com 7230 . . . . . . . . 9 class ω
20 cdom 8119 . . . . . . . . 9 class
2118, 19, 20wbr 4804 . . . . . . . 8 wff 𝑥 ≼ ω
22 vy . . . . . . . . 9 setvar 𝑦
2322cv 1631 . . . . . . . . 9 class 𝑦
2422, 18, 23wdisj 4772 . . . . . . . 8 wff Disj 𝑦𝑥 𝑦
2521, 24wa 383 . . . . . . 7 wff (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)
2618cuni 4588 . . . . . . . . 9 class 𝑥
2726, 12cfv 6049 . . . . . . . 8 class (𝑚 𝑥)
2823, 12cfv 6049 . . . . . . . . 9 class (𝑚𝑦)
2918, 28, 22cesum 30398 . . . . . . . 8 class Σ*𝑦𝑥(𝑚𝑦)
3027, 29wceq 1632 . . . . . . 7 wff (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)
3125, 30wi 4 . . . . . 6 wff ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦))
326cpw 4302 . . . . . 6 class 𝒫 𝑠
3331, 17, 32wral 3050 . . . . 5 wff 𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦))
3413, 16, 33w3a 1072 . . . 4 wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))
3534, 11cab 2746 . . 3 class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))}
362, 5, 35cmpt 4881 . 2 class (𝑠 ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))})
371, 36wceq 1632 1 wff measures = (𝑠 ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))})
 Colors of variables: wff setvar class This definition is referenced by:  measbase  30569  measval  30570  ismeas  30571  isrnmeas  30572  measbasedom  30574
 Copyright terms: Public domain W3C validator