Theory lebesgue

⊢ ∀m v.
    RADON_F m v =
    {f |
     f ∈ Borel_measurable (measurable_space m) ∧ (∀x. 0 ≤ f x) ∧
     ∀A. A ∈ measurable_sets m ⇒ ∫⁺ m (λx. f x * 𝟙 A x) ≤ measure v A}

⊢ ∀m v. RADON_F_integrals m v = {r | ∃f. r = ∫⁺ m f ∧ f ∈ RADON_F m v}

⊢ ∀m f. density m f = (m_space m,measurable_sets m,f * m)

⊢ ∀m f. f * m = (λs. ∫⁺ m (λx. f x * 𝟙 s x))

⊢ ∀M f.
    density_of M f =
    (m_space M,measurable_sets M,
     (λA.
          if A ∈ measurable_sets M then ∫⁺ M (λx. max 0 (f x * 𝟙 A x))
          else 0))

⊢ ∀m f. distr m f = (λs. measure m (PREIMAGE f s ∩ m_space m))

⊢ ∀M N f.
    distr_of M N f =
    (m_space N,measurable_sets N,
     (λs.
          if s ∈ measurable_sets N then
            measure M (PREIMAGE f s ∩ m_space M)
          else 0))

⊢ ∀m f.
    finite_space_integral m f =
    ∑ (λr. r * measure m (PREIMAGE f {r} ∩ m_space m))
      (IMAGE f (m_space m))

⊢ ∀m f.
    fn_seq_integral m f =
    (λn.
         ∑
           (λk.
                &k / 2 pow n *
                measure m
                  {x |
                   x ∈ m_space m ∧ &k / 2 pow n ≤ f x ∧
                   f x < (&k + 1) / 2 pow n}) (count (4 ** n)) +
         2 pow n * measure m {x | x ∈ m_space m ∧ 2 pow n ≤ f x})

⊢ ∀m f.
    integrable m f ⇔
    f ∈ Borel_measurable (measurable_space m) ∧ ∫⁺ m f⁺ ≠ +∞ ∧ ∫⁺ m f⁻ ≠ +∞

⊢ ∀m f. ∫ m f = ∫⁺ m f⁺ − ∫⁺ m f⁻

⊢ ∀m f.
    ∫⁺ m f = sup {r | (∃g. r ∈ psfis m g ∧ ∀x. x ∈ m_space m ⇒ g x ≤ f x)}

⊢ ∀m f s a x.
    pos_simple_fn m f s a x ⇔
    (∀t. t ∈ m_space m ⇒ 0 ≤ f t) ∧
    (∀t. t ∈ m_space m ⇒ f t = ∑ (λi. Normal (x i) * 𝟙 (a i) t) s) ∧
    (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧ FINITE s ∧
    (∀i. i ∈ s ⇒ 0 ≤ x i) ∧
    (∀i j. i ∈ s ∧ j ∈ s ∧ i ≠ j ⇒ DISJOINT (a i) (a j)) ∧
    BIGUNION (IMAGE a s) = m_space m

⊢ ∀m s a x.
    pos_simple_fn_integral m s a x =
    ∑ (λi. Normal (x i) * measure m (a i)) s

⊢ ∀m f.
    psfis m f = IMAGE (λ(s,a,x). pos_simple_fn_integral m s a x) (psfs m f)

⊢ ∀m f. psfs m f = {(s,a,x) | pos_simple_fn m f s a x}

⊢ ∀f m P.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. 0 ≤ f x) ∧
    (∀f g.
       f ∈ Borel_measurable (measurable_space m) ∧
       g ∈ Borel_measurable (measurable_space m) ∧
       (∀x. x ∈ m_space m ⇒ f x = g x) ∧ P f ⇒
       P g) ∧ (∀A. A ∈ measurable_sets m ⇒ P (𝟙 A)) ∧
    (∀f c.
       f ∈ Borel_measurable (measurable_space m) ∧ 0 ≤ c ∧ (∀x. 0 ≤ f x) ∧
       P f ⇒
       P (λx. c * f x)) ∧
    (∀f g.
       f ∈ Borel_measurable (measurable_space m) ∧
       g ∈ Borel_measurable (measurable_space m) ∧ (∀x. 0 ≤ f x) ∧ P f ∧
       (∀x. 0 ≤ g x) ∧ P g ⇒
       P (λx. f x + g x)) ∧
    (∀u. (∀i. u i ∈ Borel_measurable (measurable_space m)) ∧
         (∀i x. 0 ≤ u i x) ∧ (∀x. mono_increasing (λi. u i x)) ∧
         (∀i. P (u i)) ⇒
         P (λx. sup (IMAGE (λi. u i x) 𝕌(:num)))) ⇒
    P f

⊢ ∀m f.
    measure_space m ∧ (∃s a x. pos_simple_fn m f s a x) ⇒
    f ∈ Borel_measurable (measurable_space m)

⊢ ∀m r f.
    r ∈ psfis m f ⇒
    ∃s a x. pos_simple_fn m f s a x ∧ r = pos_simple_fn_integral m s a x

⊢ ∀m r f.
    r ∈ psfis m f ⇔
    ∃s a x. pos_simple_fn m f s a x ∧ r = pos_simple_fn_integral m s a x

⊢ ∀M N.
    measure_space M ∧ measure_space N ∧
    measurable_sets M = measurable_sets N ∧ sigma_finite M ∧
    measure_absolutely_continuous' N M ⇒
    ∃f. f ∈ Borel_measurable (measurable_space M) ∧
        (∀x. x ∈ m_space M ⇒ 0 ≤ f x) ∧
        ∀A. A ∈ measurable_sets M ⇒ ∫⁺ M (λx. f x * 𝟙 A x) = measure N A

⊢ ∀m v.
    measure_space m ∧ sigma_finite m ∧
    measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ⇒
    ∃f. f ∈ Borel_measurable (measurable_space m) ∧ (∀x. 0 ≤ f x) ∧
        ∀s. s ∈ measurable_sets m ⇒ (f * m) s = v s

⊢ ∀m v.
    measure_space m ∧ sigma_finite m ∧
    measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ⇒
    ∃f. f ∈ Borel_measurable (measurable_space m) ∧
        (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
        ∀s. s ∈ measurable_sets m ⇒ (f * m) s = v s

⊢ ∀M N.
    measure_space M ∧ measure_space N ∧
    measurable_sets M = measurable_sets N ∧ measure M (m_space M) ≠ +∞ ∧
    measure N (m_space N) ≠ +∞ ∧ measure_absolutely_continuous' N M ⇒
    ∃f. f ∈ Borel_measurable (measurable_space M) ∧ (∀x. 0 ≤ f x) ∧
        ∀A. A ∈ measurable_sets M ⇒ ∫⁺ M (λx. f x * 𝟙 A x) = measure N A

⊢ ∀M N.
    measure_space M ∧ measure_space N ∧ m_space M = m_space N ∧
    measurable_sets M = measurable_sets N ∧ measure M (m_space M) ≠ +∞ ∧
    measure_absolutely_continuous' N M ⇒
    ∃f. f ∈ Borel_measurable (measurable_space M) ∧ (∀x. 0 ≤ f x) ∧
        ∀A. A ∈ measurable_sets M ⇒ ∫⁺ M (λx. f x * 𝟙 A x) = measure N A

⊢ ∀M N.
    measure_space M ∧ measure_space N ∧
    measurable_sets M = measurable_sets N ∧ sigma_finite M ∧
    measure_absolutely_continuous' N M ⇒
    ∃f. f ∈ Borel_measurable (measurable_space M) ∧ (∀x. 0 ≤ f x) ∧
        ∀A. A ∈ measurable_sets M ⇒ ∫⁺ M (λx. f x * 𝟙 A x) = measure N A

⊢ ∀m f.
    density m f =
    (m_space m,measurable_sets m,(λs. ∫⁺ m (λx. f x * 𝟙 s x)))

⊢ ∀M f.
    density M f⁺ =
    (m_space M,measurable_sets M,(λA. ∫⁺ M (λx. max 0 (f x * 𝟙 A x))))

⊢ ∀m f s. (f * m) s = ∫⁺ m (λx. f x * 𝟙 s x)

⊢ ∀M N f.
    distr_of M N f =
    (m_space N,measurable_sets N,
     (λs. if s ∈ measurable_sets N then distr M f s else 0))

⊢ ∀m. measure_space m ∧ sigma_finite m ⇒
      ∃h. h ∈ Borel_measurable (measurable_space m) ∧ ∫⁺ m h ≠ +∞ ∧
          (∀x. x ∈ m_space m ⇒ 0 < h x ∧ h x < +∞) ∧ ∀x. 0 ≤ h x

⊢ ∀m f.
    measure_space m ∧ POW (m_space m) = measurable_sets m ∧
    FINITE (m_space m) ∧ (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧
    measure m (m_space m) < +∞ ⇒
    ∫ m f = ∑ (λx. f x * measure m {x}) (m_space m)

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧ FINITE (m_space m) ∧
    measure m (m_space m) < +∞ ∧ integrable m f ⇒
    ∫ m f = finite_space_integral m f

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧
    FINITE (IMAGE f (m_space m)) ∧ integrable m f ∧
    measure m (m_space m) < +∞ ⇒
    ∫ m f = finite_space_integral m f

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ AE x::m. f x < +∞

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ AE x::m. f x ≠ +∞ ∧ f x ≠ −∞

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m (abs ∘ f)

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    (integrable m (abs ∘ f) ⇔ ∫⁺ m (abs ∘ f) ≠ +∞)

⊢ ∀m u.
    measure_space m ∧ integrable m (abs ∘ u) ⇒
    ∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
        ∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    (integrable m (abs ∘ f) ⇔ integrable m f)

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞) ⇒
    integrable m (λx. f x + g x)

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ⇒
    integrable m (λx. f⁺ x + g⁺ x) ∧ integrable m (λx. f⁻ x + g⁻ x)

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ⇒
    integrable m (λx. f x + g x)

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m (λx. -f x)

⊢ ∀m u.
    measure_space m ∧ integrable m u ⇒
    ∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
        ∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧
    g ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ abs (g x) ≤ f x) ⇒
    integrable m g

⊢ ∀m f c.
    measure_space m ∧ integrable m f ∧ c ≠ 0 ⇒
    integrable m (λx. f x / Normal c)

⊢ ∀m f c.
    measure_space m ∧ integrable m f ⇒ integrable m (λx. Normal c * f x)

⊢ ∀m f g.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ f x = g x) ⇒
    (integrable m f ⇔ integrable m g)

⊢ ∀m c.
    measure_space m ∧ measure m (m_space m) < +∞ ⇒
    integrable m (λx. Normal c)

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ f x = g x) ⇒
    integrable m g

⊢ ∀m f g.
    complete_measure_space m ∧ integrable m f ∧ (AE x::m. f x = g x) ⇒
    integrable m g

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ ∫ m f ≠ +∞ ∧ ∫ m f ≠ −∞

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m f⁻

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m f⁺

⊢ ∀m u.
    measure_space m ∧ u ∈ Borel_measurable (measurable_space m) ∧
    integrable m (abs ∘ u) ⇒
    integrable m u

⊢ ∀m u.
    measure_space m ∧ u ∈ Borel_measurable (measurable_space m) ∧
    (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
         ∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x) ⇒
    integrable m u

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
    integrable m (𝟙 s)

⊢ ∀m s n.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ∧ 0 < n ⇒
    integrable m (λx. 𝟙 s x pow n)

⊢ ∀m f s.
    measure_space m ∧ integrable m f ∧ s ∈ measurable_sets m ∧
    (∀x. x ∈ s ⇒ f x = +∞) ⇒
    measure m s = 0

⊢ ∀m f s.
    measure_space m ∧ integrable m f ∧ s ∈ measurable_sets m ∧
    (∀x. x ∈ s ⇒ f x = −∞) ⇒
    measure m s = 0

⊢ ∀m f.
    measure_space m ∧ integrable m f ⇒
    null_set m {x | x ∈ m_space m ∧ f x = +∞}

⊢ ∀m f.
    measure_space m ∧ integrable m f ⇒
    null_set m {x | x ∈ m_space m ∧ f x = −∞}

⊢ ∀m s f.
    measure_space m ∧ s ∈ measurable_sets m ∧ integrable m f ⇒
    integrable m (λx. f x * 𝟙 s x)

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ ∃r. ∫ m f = Normal r

⊢ ∀m f.
    measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    ∃g. integrable m g ∧ (∀x. 0 ≤ g x) ∧ (∀x. g x ≠ +∞) ∧ ∫ m f = ∫ m g

⊢ ∀m f.
    measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    integrable m (λx. if f x = +∞ then 0 else f x) ∧
    ∫ m f = ∫ m (λx. if f x = +∞ then 0 else f x)

⊢ ∀m f.
    measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    integrable m (λx. if f x = +∞ then 0 else f x) ∧
    ∫⁺ m f = ∫⁺ m (λx. if f x = +∞ then 0 else f x)

⊢ ∀m f.
    measure_space m ∧ integrable m f ⇒
    integrable m (λx. if f x = −∞ ∨ f x = +∞ then 0 else f x) ∧
    ∫ m f = ∫ m (λx. if f x = −∞ ∨ f x = +∞ then 0 else f x)

⊢ ∀m f.
    measure_space m ⇒
    (integrable m f ⇔
     f ∈ Borel_measurable (measurable_space m) ∧ integrable m f⁺ ∧
     integrable m f⁻)

⊢ ∀m f.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    (integrable m f ⇔
     f ∈ Borel_measurable (measurable_space m) ∧ ∫⁺ m f ≠ +∞)

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ +∞) ⇒
    integrable m (λx. f x − g x)

⊢ ∀m f s.
    FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ∧
    (∀i x. i ∈ s ∧ x ∈ m_space m ⇒ f i x ≠ +∞ ∧ f i x ≠ −∞) ⇒
    integrable m (λx. ∑ (λi. f i x) s)

⊢ ∀m c. measure_space m ⇒ integrable m (λx. 0)

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    (∫ m (abs ∘ f) = 0 ⇔ AE x::m. (abs ∘ f) x = 0) ∧
    ((AE x::m. (abs ∘ f) x = 0) ⇔
     measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0)

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    ∫ m (abs ∘ f) = 0 ⇒
    integrable m f

⊢ ∀m f. measure_space m ⇒ ∫ m (abs ∘ f) = ∫⁺ m (abs ∘ f)

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞) ⇒
    ∫ m (λx. f x + g x) = ∫ m f + ∫ m g

⊢ ∀m f f1 f2.
    measure_space m ∧ integrable m f ∧ integrable m f1 ∧ integrable m f2 ∧
    (∀x. x ∈ m_space m ⇒ f x = f1 x − f2 x) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f1 x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f2 x) ∧
    (∀x. x ∈ m_space m ⇒ f1 x ≠ +∞ ∨ f2 x ≠ +∞) ⇒
    ∫ m f = ∫⁺ m f1 − ∫⁺ m f2

⊢ ∀m f f1 f2.
    measure_space m ∧ integrable m f ∧ integrable m f1 ∧ integrable m f2 ∧
    (∀x. x ∈ m_space m ⇒ f x = f1 x − f2 x) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f1 x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f2 x) ⇒
    ∫ m f = ∫⁺ m f1 − ∫⁺ m f2

⊢ ∀m f c.
    measure_space m ∧ integrable m f ⇒
    ∫ m (λx. Normal c * f x) = Normal c * ∫ m f

⊢ ∀m s c.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
    ∫ m (λx. Normal c * 𝟙 s x) = Normal c * measure m s

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    ∫ m (λx. +∞ * 𝟙 s x) = +∞ * measure m s

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    ∫ m (λx. −∞ * 𝟙 s x) = −∞ * measure m s

⊢ ∀m f g. measure_space m ∧ (∀x. x ∈ m_space m ⇒ f x = g x) ⇒ ∫ m f = ∫ m g

⊢ ∀m f g. measure_space m ∧ (AE x::m. f x = g x) ⇒ ∫ m f = ∫ m g

⊢ ∀m c.
    measure_space m ⇒ ∫ m (λx. Normal c) = Normal c * measure m (m_space m)

⊢ ∀m f.
    f ∈ Borel_measurable (measurable_space m) ∧ measure_space m ∧
    (AE x::m. 0 ≤ f x) ⇒
    (∫ m f = 0 ⇔ measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0)

⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ ∫ m (𝟙 s) = measure m s

⊢ ∀m s n.
    measure_space m ∧ s ∈ measurable_sets m ∧ 0 < n ⇒
    ∫ m (λx. 𝟙 s x pow n) = measure m s

⊢ ∀m s n.
    measure_space m ∧ s ∈ measurable_sets m ∧ 0 < n ⇒
    ∫ m (λx. 𝟙 s x pow n) = ∫ m (𝟙 s)

⊢ ∀m f1 f2.
    measure_space m ∧ integrable m f1 ∧ integrable m f2 ∧
    (∀x. x ∈ m_space m ⇒ f1 x ≤ f2 x) ⇒
    ∫ m f1 ≤ ∫ m f2

⊢ ∀m f. measure_space m ⇒ ∫ m f = ∫ m (λx. f x * 𝟙 (m_space m) x)

⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ f x ≤ 0) ⇒ ∫ m f ≤ 0

⊢ ∀m. measure_space m ∧ 0 < measure m (m_space m) ⇒ ∫ m (λx. −∞) = −∞

⊢ ∀m f N.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    N ∈ null_set m ⇒
    integrable m (λx. f x * 𝟙 N x) ∧ ∫ m (λx. f x * 𝟙 N x) = 0

⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ 0 ≤ ∫ m f

⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ ∫ m f = ∫⁺ m f

⊢ ∀m. measure_space m ∧ 0 < measure m (m_space m) ⇒ ∫ m (λx. +∞) = +∞

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    ∫⁺ m f = sup (IMAGE (λi. ∫⁺ m (fn_seq m f i)) 𝕌(:num))

⊢ ∀m f s.
    measure_space m ∧ s ∈ measurable_sets m ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    f ∈ Borel_measurable (measurable_space m) ⇒
    ∫ m f = ∫ m (λx. f x * 𝟙 s x) + ∫ m (λx. f x * 𝟙 (m_space m DIFF s) x)

⊢ ∀m f s.
    measure_space m ∧ integrable m f ∧ s ∈ measurable_sets m ⇒
    ∫ m f = ∫ m (λx. f x * 𝟙 s x) + ∫ m (λx. f x * 𝟙 (m_space m DIFF s) x)

⊢ ∀m f g.
    measure_space m ∧ integrable m f ∧ integrable m g ∧
    (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ +∞ ∨ f x ≠ +∞ ∧ g x ≠ −∞) ⇒
    ∫ m (λx. f x − g x) = ∫ m f − ∫ m g

⊢ ∀m f s.
    FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ∧
    (∀x i. i ∈ s ∧ x ∈ m_space m ⇒ f i x ≠ +∞ ∧ f i x ≠ −∞) ⇒
    ∫ m (λx. ∑ (λi. f i x) s) = ∑ (λi. ∫ m (f i)) s

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ abs (∫ m f) ≤ ∫ m (abs ∘ f)

⊢ ∀m f. measure_space m ∧ integrable m f ⇒ abs (∫ m f) ≤ ∫⁺ m (abs ∘ f)

⊢ ∀m. measure_space m ⇒ ∫ m (λx. 0) = 0

⊢ ∀m f fi.
    measure_space m ∧ (∀i. fi i ∈ Borel_measurable (measurable_space m)) ∧
    (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x) ∧
    (∀x. x ∈ m_space m ⇒ mono_increasing (λi. fi i x)) ∧
    (∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ⇒
    ∫⁺ m f = sup (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num))

⊢ ∀m f fi.
    measure_space m ∧ (∀i. fi i ∈ Borel_measurable (measurable_space m)) ∧
    (AE x::m. ∀i. fi i x ≤ fi (SUC i) x ∧ 0 ≤ fi i x) ∧
    (∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ⇒
    ∫⁺ m f⁺ = sup (IMAGE (λi. ∫⁺ m (fi i)⁺) 𝕌(:num))

⊢ ∀m f fi.
    measure_space m ∧ (∀i. fi i ∈ Borel_measurable (measurable_space m)) ∧
    (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x ∧ fi i x < +∞) ∧
    (∀i. ∫⁺ m (fi i) ≠ +∞) ∧
    (∀x. x ∈ m_space m ⇒ mono_decreasing (λi. fi i x)) ∧
    (∀x. x ∈ m_space m ⇒ inf (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ⇒
    ∫⁺ m f = inf (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num))

⊢ ∀m f fi A.
    measure_space m ∧ (∀i. fi i ∈ Borel_measurable (measurable_space m)) ∧
    (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x ∧ fi i x < +∞) ∧
    (∀i. ∫⁺ m (fi i) ≠ +∞) ∧
    (∀x. x ∈ m_space m ⇒ mono_decreasing (λi. fi i x)) ∧
    (∀x. x ∈ m_space m ⇒ inf (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ∧
    A ∈ measurable_sets m ⇒
    ∫⁺ m (λx. f x * 𝟙 A x) =
    inf (IMAGE (λi. ∫⁺ m (λx. fi i x * 𝟙 A x)) 𝕌(:num))

⊢ ∀m f fi A.
    measure_space m ∧ (∀i. fi i ∈ Borel_measurable (measurable_space m)) ∧
    (∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x) ∧
    (∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ∧
    (∀x. x ∈ m_space m ⇒ mono_increasing (λi. fi i x)) ∧
    A ∈ measurable_sets m ⇒
    ∫⁺ m (λx. f x * 𝟙 A x) =
    sup (IMAGE (λi. ∫⁺ m (λx. fi i x * 𝟙 A x)) 𝕌(:num))

⊢ ∀m f n.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    fn_seq m f n ∈ Borel_measurable (measurable_space m)

⊢ ∀m f. m_space (density m f) = m_space m

⊢ ∀m f c.
    measure_space m ∧ integrable m f ∧ 0 < c ⇒
    measure m ({x | c ≤ abs (f x)} ∩ m_space m) ≤ c⁻¹ * ∫ m (abs ∘ f)

⊢ ∀m f a c.
    measure_space m ∧ integrable m f ∧ a ∈ measurable_sets m ∧ 0 < c ⇒
    measure m ({x | c ≤ abs (f x)} ∩ a) ≤ c⁻¹ * ∫ m (λx. abs (f x) * 𝟙 a x)

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    (∃fi ri.
       (∀x. mono_increasing (λi. fi i x)) ∧
       (∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f⁺ x) ∧
       (∀i. ri i ∈ psfis m (fi i)) ∧ (∀i x. fi i x ≤ f⁺ x) ∧
       (∀i x. 0 ≤ fi i x) ∧ ∫⁺ m f⁺ = sup (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num))) ∧
    ∃gi vi.
      (∀x. mono_increasing (λi. gi i x)) ∧
      (∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. gi i x) 𝕌(:num)) = f⁻ x) ∧
      (∀i. vi i ∈ psfis m (gi i)) ∧ (∀i x. gi i x ≤ f⁻ x) ∧
      (∀i x. 0 ≤ gi i x) ∧ ∫⁺ m f⁻ = sup (IMAGE (λi. ∫⁺ m (gi i)) 𝕌(:num))

⊢ ∀m f. measurable_sets (density m f) = measurable_sets m

⊢ measurable_space (density m f) = measurable_space m

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    measure (density m (𝟙 s)) t = measure m (s ∩ t)

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    measure (m_space m,measurable_sets m,(λA. ∫⁺ m (λx. 𝟙 s x * 𝟙 A x))) t =
    measure m (s ∩ t)

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    measure_space (density m f)

⊢ ∀M f.
    measure_space M ∧ f ∈ Borel_measurable (measurable_space M) ⇒
    measure_space (density M f⁺)

⊢ ∀M f.
    measure_space M ∧ f ∈ Borel_measurable (measurable_space M) ⇒
    measure_space (density_of M f)

⊢ ∀M B f.
    measure_space M ∧ sigma_algebra B ∧
    f ∈ measurable (measurable_space M) B ⇒
    measure_space (space B,subsets B,distr M f)

⊢ ∀M N f.
    measure_space M ∧ measure_space N ∧
    f ∈ measurable (measurable_space M) (measurable_space N) ⇒
    measure_space (distr_of M N f)

⊢ ∀m f g.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ∧
    f ∈ Borel_measurable (measurable_space m) ∧
    g ∈ Borel_measurable (measurable_space m) ⇒
    ∫⁺ m (λx. f x + g x) = ∫⁺ m f + ∫⁺ m g

⊢ ∀m f c.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ 0 ≤ c ⇒
    ∫⁺ m (λx. Normal c * f x) = Normal c * ∫⁺ m f

⊢ ∀m f c.
    measure_space m ∧ 0 ≤ c ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    ∫⁺ m (λx. c * f x) = c * ∫⁺ m f

⊢ ∀m s c.
    measure_space m ∧ s ∈ measurable_sets m ∧ 0 ≤ c ⇒
    ∫⁺ m (λx. Normal c * 𝟙 s x) = Normal c * measure m s

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    ∫⁺ m (λx. +∞ * 𝟙 s x) = +∞ * measure m s

⊢ ∀f c m.
    measure_space m ∧ 0 ≤ c ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    ∫⁺ m (λx. c * f⁺ x) = c * ∫⁺ m f⁺

⊢ ∀f c m.
    measure_space m ∧ 0 ≤ c ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    ∫⁺ m (λx. max 0 (c * f x)) = c * ∫⁺ m (λx. max 0 (f x))

⊢ ∀m u v.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (∀x. x ∈ m_space m ⇒ u x = v x) ⇒
    ∫⁺ m u = ∫⁺ m v

⊢ ∀m u v.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (AE x::m. u x = v x) ⇒
    ∫⁺ m u = ∫⁺ m v

⊢ ∀m c.
    measure_space m ∧ 0 ≤ c ⇒
    ∫⁺ m (λx. Normal c) = Normal c * measure m (m_space m)

⊢ ∀f g M.
    measure_space M ∧ f ∈ Borel_measurable (measurable_space M) ∧
    g ∈ Borel_measurable (measurable_space M) ∧ (AE x::M. 0 ≤ f x) ∧
    (∀x. 0 ≤ g x) ⇒
    ∫⁺ (m_space M,measurable_sets M,(λA. ∫⁺ M (λx. max 0 (f x * 𝟙 A x))))
      (λx. max 0 (g x)) =
    ∫⁺ M (λx. max 0 (f x * g x))

⊢ ∀m f s t.
    measure_space m ∧ DISJOINT s t ∧ s ∈ measurable_sets m ∧
    t ∈ measurable_sets m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    ∫⁺ m (λx. f x * 𝟙 (s ∪ t) x) =
    ∫⁺ m (λx. f x * 𝟙 s x) + ∫⁺ m (λx. f x * 𝟙 t x)

⊢ ∀m f s a.
    FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    (∀i j. i ∈ s ∧ j ∈ s ∧ i ≠ j ⇒ DISJOINT (a i) (a j)) ∧
    f ∈ Borel_measurable (measurable_space m) ⇒
    ∫⁺ m (λx. f x * 𝟙 (BIGUNION (IMAGE a s)) x) =
    ∑ (λi. ∫⁺ m (λx. f x * 𝟙 (a i) x)) s

⊢ ∀m f.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    f ∈ Borel_measurable (measurable_space m) ⇒
    (∫⁺ m f = 0 ⇔ measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0)

⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ ∫⁺ m (𝟙 s) = measure m s

⊢ ∀m f.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    f ∈ Borel_measurable (measurable_space m) ∧ ∫⁺ m f ≠ +∞ ⇒
    null_set m {x | x ∈ m_space m ∧ f x = +∞}

⊢ ∀m f.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    ∫⁺ m (λx. max 0 (f x)) = ∫⁺ m f

⊢ ∀m f g.
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
    ∫⁺ m f ≤ ∫⁺ m g

⊢ ∀m u v.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (AE x::m. u x ≤ v x) ⇒
    ∫⁺ m u ≤ ∫⁺ m v

⊢ ∀m f.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    ∫⁺ m f = ∫⁺ m (λx. f x * 𝟙 (m_space m) x)

⊢ ∀m f N.
    measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ N ∈ null_set m ⇒
    ∫⁺ m (λx. f x * 𝟙 N x) = 0

⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ 0 ≤ ∫⁺ m f

⊢ ∀m f s a x.
    measure_space m ∧ pos_simple_fn m f s a x ⇒
    ∫⁺ m f = pos_simple_fn_integral m s a x

⊢ ∀m f s.
    measure_space m ∧ s ∈ measurable_sets m ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
    f ∈ Borel_measurable (measurable_space m) ⇒
    ∫⁺ m f =
    ∫⁺ m (λx. f x * 𝟙 s x) + ∫⁺ m (λx. f x * 𝟙 (m_space m DIFF s) x)

⊢ ∀m f g.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    g ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ∧ (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧
    (∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧ ∫⁺ m g ≠ +∞ ⇒
    ∫⁺ m (λx. f x − g x) = ∫⁺ m f − ∫⁺ m g

⊢ ∀m f s.
    FINITE s ∧ measure_space m ∧
    (∀i. i ∈ s ⇒ ∀x. x ∈ m_space m ⇒ 0 ≤ f i x) ∧
    (∀i. i ∈ s ⇒ f i ∈ Borel_measurable (measurable_space m)) ⇒
    ∫⁺ m (λx. ∑ (λi. f i x) s) = ∑ (λi. ∫⁺ m (f i)) s

⊢ ∀m s a x.
    measure_space m ∧ FINITE s ∧ (∀i. i ∈ s ⇒ 0 ≤ x i) ∧
    (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ⇒
    ∫⁺ m (λt. ∑ (λi. Normal (x i) * 𝟙 (a i) t) s) =
    ∑ (λi. Normal (x i) * measure m (a i)) s

⊢ ∀m f.
    measure_space m ∧ (∀i x. x ∈ m_space m ⇒ 0 ≤ f i x) ∧
    (∀i. f i ∈ Borel_measurable (measurable_space m)) ⇒
    ∫⁺ m (λx. suminf (λi. f i x)) = suminf (λi. ∫⁺ m (f i))

⊢ ∀m. measure_space m ⇒ ∫⁺ m (λx. 0) = 0

⊢ ∀m f g s a x s' a' x'.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s' a' x' ⇒
    ∃s'' a'' x''. pos_simple_fn m (λt. f t + g t) s'' a'' x''

⊢ ∀m f g s a x y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s a y ⇒
    pos_simple_fn m (λt. f t + g t) s a (λi. x i + y i)

⊢ ∀m f z s a x.
    measure_space m ∧ pos_simple_fn m f s a x ∧ 0 ≤ z ⇒
    ∃s' a' x'. pos_simple_fn m (λt. Normal z * f t) s' a' x'

⊢ ∀m f s a x z.
    measure_space m ∧ 0 ≤ z ∧ pos_simple_fn m f s a x ⇒
    pos_simple_fn m (λt. Normal z * f t) s a (λi. z * x i)

⊢ ∀m A.
    measure_space m ∧ A ∈ measurable_sets m ⇒
    ∃s a x. pos_simple_fn m (𝟙 A) s a x

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    pos_simple_fn m (𝟙 s) {0; 1}
      (λi. if i = 0 then m_space m DIFF s else s)
      (λi. if i = 0 then 0 else 1)

⊢ ∀m f s a x g s' b y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s' b y ⇒
    ∃s'' c z.
      pos_simple_fn m (λx. f x + g x) s'' c z ∧
      pos_simple_fn_integral m s a x + pos_simple_fn_integral m s' b y =
      pos_simple_fn_integral m s'' c z

⊢ ∀m f s a x g y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s a y ⇒
    pos_simple_fn_integral m s a x + pos_simple_fn_integral m s a y =
    pos_simple_fn_integral m s a (λi. x i + y i)

⊢ ∀m f s a x z.
    measure_space m ∧ pos_simple_fn m f s a x ∧ 0 ≤ z ⇒
    pos_simple_fn m (λx. Normal z * f x) s a (λi. z * x i) ∧
    pos_simple_fn_integral m s a (λi. z * x i) =
    Normal z * pos_simple_fn_integral m s a x

⊢ ∀m f s a x z.
    measure_space m ∧ 0 ≤ z ∧ pos_simple_fn m f s a x ⇒
    ∃s' a' x'.
      pos_simple_fn m (λt. Normal z * f t) s' a' x' ∧
      pos_simple_fn_integral m s' a' x' =
      Normal z * pos_simple_fn_integral m s a x

⊢ ∀m A.
    measure_space m ∧ A ∈ measurable_sets m ⇒
    ∃s a x.
      pos_simple_fn m (𝟙 A) s a x ∧
      pos_simple_fn_integral m s a x = measure m A

⊢ ∀m f s a x g s' b y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s' b y ∧
    (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
    pos_simple_fn_integral m s a x ≤ pos_simple_fn_integral m s' b y

⊢ ∀m f s a x.
    measure_space m ∧ pos_simple_fn m f s a x ⇒
    pos_simple_fn_integral m s a x ≠ −∞

⊢ ∀m f s a x g s' b y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s' b y ⇒
    ∃z z' c k.
      (∀t. t ∈ m_space m ⇒ f t = ∑ (λi. Normal (z i) * 𝟙 (c i) t) k) ∧
      (∀t. t ∈ m_space m ⇒ g t = ∑ (λi. Normal (z' i) * 𝟙 (c i) t) k) ∧
      pos_simple_fn_integral m s a x = pos_simple_fn_integral m k c z ∧
      pos_simple_fn_integral m s' b y = pos_simple_fn_integral m k c z' ∧
      FINITE k ∧ (∀i. i ∈ k ⇒ 0 ≤ z i) ∧ (∀i. i ∈ k ⇒ 0 ≤ z' i) ∧
      (∀i j. i ∈ k ∧ j ∈ k ∧ i ≠ j ⇒ DISJOINT (c i) (c j)) ∧
      (∀i. i ∈ k ⇒ c i ∈ measurable_sets m) ∧
      BIGUNION (IMAGE c k) = m_space m

⊢ ∀m f s a x g s' b y.
    measure_space m ∧ measure m (m_space m) ≠ +∞ ∧
    (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧
    pos_simple_fn m f s a x ∧ pos_simple_fn m g s' b y ⇒
    ∃s'' c z.
      pos_simple_fn m (λx. f x − g x) s'' c z ∧
      pos_simple_fn_integral m s a x − pos_simple_fn_integral m s' b y =
      pos_simple_fn_integral m s'' c z

⊢ ∀m f s a x P.
    measure_space m ∧ (∀i. i ∈ P ⇒ pos_simple_fn m (f i) s a (x i)) ∧
    (∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ∧ P ≠ ∅ ⇒
    pos_simple_fn m (λt. ∑ (λi. f i t) P) s a (λi. ∑ (λj. x j i) P) ∧
    pos_simple_fn_integral m s a (λj. ∑ (λi. x i j) P) =
    ∑ (λi. pos_simple_fn_integral m s a (x i)) P

⊢ ∀m f s a x P.
    measure_space m ∧
    (∀i. i ∈ P ⇒ pos_simple_fn m (f i) (s i) (a i) (x i)) ∧
    (∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ∧ P ≠ ∅ ⇒
    ∃c k z.
      pos_simple_fn m (λt. ∑ (λi. f i t) P) k c z ∧
      pos_simple_fn_integral m k c z =
      ∑ (λi. pos_simple_fn_integral m (s i) (a i) (x i)) P

⊢ ∀m f s a x s' b y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m f s' b y ⇒
    pos_simple_fn_integral m s a x = pos_simple_fn_integral m s' b y

⊢ ∀m s a x.
    measure_space m ∧ pos_simple_fn m (λt. 0) s a x ⇒
    pos_simple_fn_integral m s a x = 0

⊢ ∀m g s a x.
    measure_space m ∧ pos_simple_fn m g s a x ∧
    (∀x. x ∈ m_space m ⇒ g x = 0) ⇒
    pos_simple_fn_integral m s a x = 0

⊢ ∀m f g s a x x' i.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s a x' ∧
    (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧ i ∈ s ∧ a i ≠ ∅ ⇒
    Normal (x' i) ≤ Normal (x i)

⊢ ∀m f s a x g s' b y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ pos_simple_fn m g s' b y ⇒
    ∃s'' a'' x''. pos_simple_fn m (λx. max (f x) (g x)) s'' a'' x''

⊢ ∀m f s a x.
    pos_simple_fn m f s a x ⇒ ∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞

⊢ ∀m f s a x i y.
    measure_space m ∧ pos_simple_fn m f s a x ∧ i ∈ s ∧ y ∈ a i ⇒
    f y = Normal (x i)

⊢ ∀m f g a b.
    measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
    a + b ∈ psfis m (λx. f x + g x)

⊢ ∀m f a z.
    measure_space m ∧ a ∈ psfis m f ∧ 0 ≤ z ⇒
    Normal z * a ∈ psfis m (λx. Normal z * f x)

⊢ ∀m A.
    measure_space m ∧ A ∈ measurable_sets m ⇒ measure m A ∈ psfis m (𝟙 A)

⊢ ∀m a x P.
    measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ measurable_sets m) ∧
    (∀i. i ∈ P ⇒ 0 ≤ x i) ∧ FINITE P ⇒
    ∑ (λi. Normal (x i) * measure m (a i)) P ∈
    psfis m (λt. ∑ (λi. Normal (x i) * 𝟙 (a i) t) P)

⊢ ∀m f g a b.
    measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ∧
    (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
    a ≤ b

⊢ ∀m f a. measure_space m ∧ a ∈ psfis m f ⇒ a ≠ −∞

⊢ ∀m f a. measure_space m ∧ a ∈ psfis m f ⇒ ∀x. x ∈ m_space m ⇒ 0 ≤ f x

⊢ ∀m f g a b.
    measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
    ∃z z' c k.
      (∀t. t ∈ m_space m ⇒ f t = ∑ (λi. Normal (z i) * 𝟙 (c i) t) k) ∧
      (∀t. t ∈ m_space m ⇒ g t = ∑ (λi. Normal (z' i) * 𝟙 (c i) t) k) ∧
      a = pos_simple_fn_integral m k c z ∧
      b = pos_simple_fn_integral m k c z' ∧ FINITE k ∧
      (∀i. i ∈ k ⇒ 0 ≤ z i) ∧ (∀i. i ∈ k ⇒ 0 ≤ z' i) ∧
      (∀i j. i ∈ k ∧ j ∈ k ∧ i ≠ j ⇒ DISJOINT (c i) (c j)) ∧
      (∀i. i ∈ k ⇒ c i ∈ measurable_sets m) ∧
      BIGUNION (IMAGE c k) = m_space m

⊢ ∀m f g a b.
    measure_space m ∧ measure m (m_space m) ≠ +∞ ∧
    (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧
    a ∈ psfis m f ∧ b ∈ psfis m g ⇒
    a − b ∈ psfis m (λx. f x − g x)

⊢ ∀m f a P.
    measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ psfis m (f i)) ∧
    (∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ⇒
    ∑ a P ∈ psfis m (λt. ∑ (λi. f i t) P)

⊢ ∀m f a b. measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m f ⇒ a = b

⊢ ∀m a. measure_space m ⇒ (a ∈ psfis m (λx. 0) ⇔ a = 0)