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 32835
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 32834 . 2 class measures
2 vs . . 3 setvar 𝑠
3 csiga 32747 . . . . 5 class sigAlgebra
43crn 5639 . . . 4 class ran sigAlgebra
54cuni 4870 . . 3 class ran sigAlgebra
62cv 1541 . . . . . 6 class 𝑠
7 cc0 11058 . . . . . . 7 class 0
8 cpnf 11193 . . . . . . 7 class +∞
9 cicc 13274 . . . . . . 7 class [,]
107, 8, 9co 7362 . . . . . 6 class (0[,]+∞)
11 vm . . . . . . 7 setvar 𝑚
1211cv 1541 . . . . . 6 class 𝑚
136, 10, 12wf 6497 . . . . 5 wff 𝑚:𝑠⟶(0[,]+∞)
14 c0 4287 . . . . . . 7 class
1514, 12cfv 6501 . . . . . 6 class (𝑚‘∅)
1615, 7wceq 1542 . . . . 5 wff (𝑚‘∅) = 0
17 vx . . . . . . . . . 10 setvar 𝑥
1817cv 1541 . . . . . . . . 9 class 𝑥
19 com 7807 . . . . . . . . 9 class ω
20 cdom 8888 . . . . . . . . 9 class
2118, 19, 20wbr 5110 . . . . . . . 8 wff 𝑥 ≼ ω
22 vy . . . . . . . . 9 setvar 𝑦
2322cv 1541 . . . . . . . . 9 class 𝑦
2422, 18, 23wdisj 5075 . . . . . . . 8 wff Disj 𝑦𝑥 𝑦
2521, 24wa 397 . . . . . . 7 wff (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)
2618cuni 4870 . . . . . . . . 9 class 𝑥
2726, 12cfv 6501 . . . . . . . 8 class (𝑚 𝑥)
2823, 12cfv 6501 . . . . . . . . 9 class (𝑚𝑦)
2918, 28, 22cesum 32666 . . . . . . . 8 class Σ*𝑦𝑥(𝑚𝑦)
3027, 29wceq 1542 . . . . . . 7 wff (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)
3125, 30wi 4 . . . . . 6 wff ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦))
326cpw 4565 . . . . . 6 class 𝒫 𝑠
3331, 17, 32wral 3065 . . . . 5 wff 𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦))
3413, 16, 33w3a 1088 . . . 4 wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))
3534, 11cab 2714 . . 3 class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑚 𝑥) = Σ*𝑦𝑥(𝑚𝑦)))}
362, 5, 35cmpt 5193 . 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  32836  measval  32837  ismeas  32838  isrnmeas  32839
  Copyright terms: Public domain W3C validator