Theory measure

⊢ ∀m. additive m ⇔
      ∀s t.
        s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ DISJOINT s t ∧
        s ∪ t ∈ measurable_sets m ⇒
        measure m (s ∪ t) = measure m s + measure m t

⊢ ∀sp m.
    caratheodory_sets sp m =
    {a | a ⊆ sp ∧ ∀q. q ⊆ sp ⇒ m q = m (q ∩ a) + m (q DIFF a)}

⊢ ∀m. complete_measure_space m ⇔
      measure_space m ∧
      ∀s. null_set m s ⇒ ∀t. t ⊆ s ⇒ t ∈ measurable_sets m

⊢ ∀m. completion m =
      (m_space m,{s ∪ n | s ∈ measurable_sets m ∧ ∃t. n ⊆ t ∧ null_set m t})

⊢ ∀M u.
    countably_additive_alt M u ⇔
    ∀A. IMAGE A 𝕌(:num) ⊆ M ⇒
        disjoint_family A ⇒
        BIGUNION {A i | i ∈ 𝕌(:num)} ∈ M ⇒
        u (BIGUNION {A i | i ∈ 𝕌(:num)}) = suminf (u ∘ A)

⊢ ∀m. countably_additive m ⇔
      ∀f. f ∈ (𝕌(:num) → measurable_sets m) ∧
          (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
          BIGUNION (IMAGE f 𝕌(:num)) ∈ measurable_sets m ⇒
          measure m (BIGUNION (IMAGE f 𝕌(:num))) = suminf (measure m ∘ f)

⊢ ∀m. countably_subadditive m ⇔
      ∀f. f ∈ (𝕌(:num) → measurable_sets m) ∧
          BIGUNION (IMAGE f 𝕌(:num)) ∈ measurable_sets m ⇒
          measure m (BIGUNION (IMAGE f 𝕌(:num))) ≤ suminf (measure m ∘ f)

⊢ ∀m. finite_additive m ⇔
      ∀f n.
        (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
        (∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
        BIGUNION (IMAGE f (count n)) ∈ measurable_sets m ⇒
        measure m (BIGUNION (IMAGE f (count n))) =
        ∑ (measure m ∘ f) (count n)

⊢ ∀m. finite_measure_space m ⇔ measure_space m ∧ measure m (m_space m) ≠ +∞

⊢ ∀m. finite_subadditive m ⇔
      ∀f n.
        (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
        BIGUNION (IMAGE f (count n)) ∈ measurable_sets m ⇒
        measure m (BIGUNION (IMAGE f (count n))) ≤
        ∑ (measure m ∘ f) (count n)

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

⊢ ∀m. increasing m ⇔
      ∀s t.
        s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ s ⊆ t ⇒
        measure m s ≤ measure m t

⊢ ∀sp sts mu. m_space (sp,sts,mu) = sp

⊢ ∀sp sts mu. measurable_sets (sp,sts,mu) = sts

⊢ ∀v m. v ≪ m ⇔ ∀s. s ∈ measurable_sets m ∧ measure m s = 0 ⇒ v s = 0

⊢ ∀sp sts mu. measure (sp,sts,mu) = mu

⊢ ∀sp A u.
    measure_of (sp,A,u) =
    (sp,if A ⊆ POW sp then sigma_sets sp A else {∅; sp},
     (λa.
          if
            a ∈ sigma_sets sp A ∧ measure_space (sp,sigma_sets sp A,u)
          then
            u a
          else 0))

⊢ ∀m1 m2.
    measure_preserving m1 m2 =
    {f |
     f ∈ measurable (measurable_space m1) (measurable_space m2) ∧
     ∀s. s ∈ measurable_sets m2 ⇒
         measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s}

⊢ ∀sp A u.
    measure_space_alt sp A u ⇔
    sigma_algebra_alt sp A ∧ positive_alt A u ∧ countably_additive_alt A u

⊢ ∀m. measure_space m ⇔
      sigma_algebra (measurable_space m) ∧ positive m ∧
      countably_additive m

⊢ ∀m1 m2.
    measure_space_eq m1 m2 ⇔
    m_space m1 = m_space m2 ∧ measurable_sets m1 = measurable_sets m2 ∧
    ∀s. s ∈ measurable_sets m1 ⇒ measure m1 s = measure m2 s

⊢ ∀d e sts.
    metric_countable_covers d e sts =
    (λa.
         {f |
          f ∈ (𝕌(:num) → sts) ∧ a ⊆ BIGUNION (IMAGE f 𝕌(:num)) ∧
          ∀i. Normal (set_diameter d (f i)) ≤ e})

⊢ ∀m s. null_set m s ⇔ s ∈ measurable_sets m ∧ measure m s = 0

⊢ ∀m C.
    outer_measure m C = (λa. inf {r | (∃f. f ∈ C a ∧ suminf (m ∘ f) = r)})

⊢ ∀m. outer_measure_space m ⇔
      subset_class (m_space m) (measurable_sets m) ∧
      ∅ ∈ measurable_sets m ∧ positive m ∧ increasing m ∧
      countably_subadditive m

⊢ ∀M u. positive_alt M u ⇔ u ∅ = 0 ∧ ∀a. a ∈ M ⇒ 0 ≤ u a

⊢ ∀m. positive m ⇔
      measure m ∅ = 0 ∧ ∀s. s ∈ measurable_sets m ⇒ 0 ≤ measure m s

⊢ ∀m. premeasure m ⇔ positive m ∧ countably_additive m

⊢ ∀M sp.
    restrict_space M sp =
    (sp ∩ m_space M,IMAGE (λa. a ∩ sp) (measurable_sets M),measure M)

⊢ ∀m. sigma_finite m ⇔
      ∃f. exhausting_sequence (measurable_space m) f ∧
          ∀n. measure m (f n) < +∞

⊢ ∀m. sigma_finite_measure_space m ⇔ measure_space m ∧ sigma_finite m

⊢ ∀m. subadditive m ⇔
      ∀s t.
        s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
        s ∪ t ∈ measurable_sets m ⇒
        measure m (s ∪ t) ≤ measure m s + measure m t

⊢ ∀m s t u.
    additive m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
    DISJOINT s t ∧ u ∈ measurable_sets m ∧ u = s ∪ t ⇒
    measure m u = measure m s + measure m t

⊢ ∀m. algebra (measurable_space m) ∧ positive m ∧ additive m ⇒ increasing m

⊢ ∀m f n.
    algebra (measurable_space m) ∧ positive m ∧ additive m ∧
    f ∈ (𝕌(:num) → measurable_sets m) ∧
    (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
    ∑ (measure m ∘ f) (count n) = measure m (BIGUNION (IMAGE f (count n)))

⊢ ∀m. algebra (measurable_space m) ∧ positive m ∧ countably_additive m ⇒
      additive m

⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒ additive m

⊢ ∀m s.
    algebra (measurable_space m) ∧ premeasure m ∧ s ∈ measurable_sets m ∧
    measure m s < +∞ ⇒
    measure m (m_space m DIFF s) = measure m (m_space m) − measure m s

⊢ ∀m s f.
    algebra (measurable_space m) ∧ premeasure m ∧
    f ∈ (𝕌(:num) → measurable_sets m) ∧ f 0 = ∅ ∧ (∀n. f n ⊆ f (SUC n)) ∧
    s = BIGUNION (IMAGE f 𝕌(:num)) ∧ s ∈ measurable_sets m ⇒
    sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s

⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒ countably_subadditive m

⊢ ∀m s t.
    algebra (measurable_space m) ∧ premeasure m ∧ s ∈ measurable_sets m ∧
    t ∈ measurable_sets m ∧ s ⊆ t ∧ measure m s < +∞ ⇒
    measure m (t DIFF s) = measure m t − measure m s

⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒ finite_additive m

⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒ finite_subadditive m

⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒ increasing m

⊢ ∀m s t.
    algebra (measurable_space m) ∧ premeasure m ∧ s ∈ measurable_sets m ∧
    t ∈ measurable_sets m ⇒
    measure m (s ∪ t) + measure m (s ∩ t) = measure m s + measure m t

⊢ ∀m. algebra (measurable_space m) ∧ premeasure m ⇒ subadditive m

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ (ℚ꙳ → subsets a) ⇒
    BIGUNION (IMAGE f ℚ꙳) ∈ subsets a

⊢ ∀m0.
    algebra (measurable_space m0) ∧ positive m0 ∧ countably_additive m0 ⇒
    ∃m. (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
        measurable_space m = sigma (m_space m0) (measurable_sets m0) ∧
        measure_space m

⊢ ∀m0.
    ring (measurable_space m0) ∧ positive m0 ∧ countably_additive m0 ⇒
    ∃m. (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
        measurable_space m = sigma (m_space m0) (measurable_sets m0) ∧
        measure_space m

⊢ ∀m0.
    semiring (measurable_space m0) ∧ premeasure m0 ⇒
    ∃m. (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
        measurable_space m = sigma (m_space m0) (measurable_sets m0) ∧
        measure_space m

⊢ ∀m s t.
    complete_measure_space m ∧ t ∈ null_set m ∧ s ⊆ t ⇒ s ∈ null_set m

⊢ ∀m. complete_measure_space m ⇒
      space (completion m) = m_space m ∧
      subsets (completion m) = measurable_sets m

⊢ ∀m. complete_measure_space m ⇒ completion m = measurable_space m

⊢ ∀m. measure_space m ⇒ measurable_sets m ⊆ subsets (completion m)

⊢ ∀m s f.
    countably_additive m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ∧ s = BIGUNION (IMAGE f 𝕌(:num)) ∧
    s ∈ measurable_sets m ⇒
    suminf (measure m ∘ f) = measure m s

⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_additive m ⇒
      additive m

⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_additive m ⇒
      finite_additive m

⊢ ∀m f s.
    countably_subadditive m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    s = BIGUNION (IMAGE f 𝕌(:num)) ∧ s ∈ measurable_sets m ⇒
    measure m s ≤ suminf (measure m ∘ f)

⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_subadditive m ⇒
      finite_subadditive m

⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_subadditive m ⇒
      subadditive m

⊢ ∀d s t.
    dynkin_system d ∧ s ∈ subsets d ∧ t ∈ subsets d ∧ s ⊆ t ⇒
    t DIFF s ∈ subsets d

⊢ ∀m. dynkin_system (measurable_space m) ∧ premeasure m ⇒ additive m

⊢ ∀m. dynkin_system (measurable_space m) ∧ premeasure m ⇒ finite_additive m

⊢ ∀m. dynkin_system (measurable_space m) ∧ premeasure m ⇒ increasing m

⊢ ∀m s f n.
    finite_additive m ∧ (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
    (∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
    s = BIGUNION (IMAGE f (count n)) ∧ s ∈ measurable_sets m ⇒
    ∑ (measure m ∘ f) (count n) = measure m s

⊢ ∀m s c.
    positive m ∧ finite_additive m ∧ c ⊆ measurable_sets m ∧ FINITE c ∧
    disjoint c ∧ BIGUNION c ∈ measurable_sets m ⇒
    ∑ (measure m) c = measure m (BIGUNION c)

⊢ ∀m. measure_space m ∧ measure m (m_space m) ≠ +∞ ⇒ sigma_finite m

⊢ ∀m s f n.
    finite_subadditive m ∧ (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧
    s = BIGUNION (IMAGE f (count n)) ∧ s ∈ measurable_sets m ⇒
    measure m s ≤ ∑ (measure m ∘ f) (count n)

⊢ ∀m c.
    positive m ∧ finite_subadditive m ∧ c ⊆ measurable_sets m ∧ FINITE c ∧
    disjoint c ∧ BIGUNION c ∈ measurable_sets m ⇒
    measure m (BIGUNION c) ≤ ∑ (measure m) c

⊢ ∀m s t.
    increasing m ∧ s ⊆ t ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    measure m s ≤ measure m t

⊢ ∀m1 m2 f.
    f ∈ measure_preserving m1 m2 ⇔
    f ∈ measurable (measurable_space m1) (measurable_space m2) ∧
    ∀s. s ∈ measurable_sets m2 ⇒
        measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s

⊢ ∀m s. s ∈ null_set m ⇔ null_set m s

⊢ ∀f g M N P.
    f ∈ measurable (measurable_space M) (measurable_space N) ∧
    g ∈ measurable (measurable_space M) (measurable_space N) ∧
    {x | x ∈ m_space M ∧ P x} ∈ measurable_sets M ∧ measure_space M ∧
    sigma_algebra (measurable_space N) ⇒
    (λx. if P x then f x else g x) ∈
    measurable (measurable_space M) (measurable_space N)

⊢ ∀f g M N A.
    f ∈ measurable (measurable_space M) (measurable_space N) ∧
    g ∈ measurable (measurable_space M) (measurable_space N) ∧
    A ∩ m_space M ∈ measurable_sets M ∧ measure_space M ∧
    sigma_algebra (measurable_space N) ⇒
    (λx. if x ∈ A then f x else g x) ∈
    measurable (measurable_space M) (measurable_space N)

⊢ ∀m f.
    measure_space m ∧ measurable_sets m = POW (m_space m) ⇒
    f ∈ measurable (measurable_space m) (𝕌(:β),POW 𝕌(:β))

⊢ ∀m f.
    measure_space m ∧ measurable_sets m = POW (m_space m) ⇒
    f ∈
    measurable (measurable_space m)
      (IMAGE f (m_space m),POW (IMAGE f (m_space m)))

⊢ ∀m f s.
    measure_space m ∧ f ∈ measurable (measurable_space m) (s,POW s) ∧ s ≠ ∅ ⇒
    f ∈
    measurable (measurable_space m)
      (s ∩ IMAGE f (m_space m),POW (s ∩ IMAGE f (m_space m)))

⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ s ⊆ m_space m

⊢ ∀m s t u.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
    DISJOINT s t ∧ u = s ∪ t ⇒
    measure m u = measure m s + measure m t

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
    measure m t = 0 ⇒
    measure m (s ∪ t) = measure m s

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
    measure m (m_space m DIFF s) = measure m (m_space m) − measure m s

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
    t ⊆ s ∧ measure m t < +∞ ⇒
    measure m (s DIFF t) = measure m s − measure m t

⊢ ∀m s f.
    measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧ f 0 = ∅ ∧
    (∀n. f n ⊆ f (SUC n)) ∧ s = BIGUNION (IMAGE f 𝕌(:num)) ⇒
    sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s

⊢ ∀m s f.
    measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧ s = BIGUNION (IMAGE f 𝕌(:num)) ⇒
    suminf (measure m ∘ f) = measure m s

⊢ ∀m f s.
    measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    s = BIGUNION (IMAGE f 𝕌(:num)) ⇒
    measure m s ≤ suminf (measure m ∘ f)

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
    t ⊆ s ∧ measure m t < +∞ ⇒
    measure m (s DIFF t) = measure m s − measure m t

⊢ ∀m0 m1.
    sigma_algebra (measurable_space m0) ∧
    measurable_sets m0 ⊆ measurable_sets m1 ∧ measure m0 = measure m1 ∧
    measure_space m1 ⇒
    measure_space m0

⊢ ∀m. measure_space m ⇒ measure m ∅ = 0

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ∧
    (∀x. x ∈ s ⇒ {x} ∈ measurable_sets m) ∧ FINITE s ⇒
    measure m s = ∑ (λx. measure m {x}) s

⊢ ∀m. measure_space m ⇒ finite_additive m

⊢ ∀m s t.
    measure_space m ∧ s ⊆ t ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    measure m s ≤ measure m t

⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ 0 ≤ measure m s

⊢ ∀m1 m2 a f.
    measure_space m1 ∧ measure_space m2 ∧
    measure_space (m_space m2,a,measure m2) ∧
    measure m1 (m_space m1) ≠ +∞ ∧ measure m2 (m_space m2) ≠ +∞ ∧
    measurable_sets m2 = subsets (sigma (m_space m2) a) ∧
    f ∈ measure_preserving m1 (m_space m2,a,measure m2) ⇒
    f ∈ measure_preserving m1 m2

⊢ ∀m1 m2 a.
    measure_space m1 ∧ measure_space m2 ∧
    measure_space (m_space m2,a,measure m2) ∧
    measure m1 (m_space m1) ≠ +∞ ∧ measure m2 (m_space m2) ≠ +∞ ∧
    measurable_sets m2 = subsets (sigma (m_space m2) a) ⇒
    measure_preserving m1 (m_space m2,a,measure m2) ⊆
    measure_preserving m1 m2

⊢ ∀m1 m2 f a.
    f ∈ measure_preserving (m_space m1,a,measure m1) m2 ∧
    sigma_algebra (measurable_space m1) ∧ a ⊆ measurable_sets m1 ⇒
    f ∈ measure_preserving m1 m2

⊢ ∀m1 m2 a.
    subset_class (m_space m1) a ∧
    measurable_sets m1 = subsets (sigma (m_space m1) a) ⇒
    measure_preserving (m_space m1,a,measure m1) m2 ⊆
    measure_preserving m1 m2

⊢ ∀m1 m2 a.
    a ⊆ measurable_sets m1 ∧ sigma_algebra (measurable_space m1) ⇒
    measure_preserving (m_space m1,a,measure m1) m2 ⊆
    measure_preserving m1 m2

⊢ ∀m. measure_space m ⇒ additive m

⊢ ∀m s.
    measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
    BIGINTER (IMAGE s 𝕌(:num)) ∈ measurable_sets m

⊢ ∀m s.
    measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
    BIGUNION (IMAGE s 𝕌(:num)) ∈ measurable_sets m

⊢ ∀m c.
    measure_space m ∧ 0 ≤ c ⇒
    measure_space
      (m_space m,measurable_sets m,(λa. Normal c * measure m a))

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    m_space m DIFF s ∈ measurable_sets m

⊢ ∀m. measure_space m ⇒ countably_additive m

⊢ ∀m. measure_space m ⇒ countably_subadditive m

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    s DIFF t ∈ measurable_sets m

⊢ ∀m. measure_space m ⇒ ∅ ∈ measurable_sets m

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m s ≠ +∞ ⇒
    measure m (m_space m DIFF s) = measure m (m_space m) − measure m s

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
    t ⊆ s ∧ measure m s ≠ +∞ ⇒
    measure m (s DIFF t) = measure m s − measure m t

⊢ ∀m f n.
    measure_space m ∧ (∀i. i < n ⇒ f i ∈ measurable_sets m) ∧ 0 < n ⇒
    BIGINTER (IMAGE f (count n)) ∈ measurable_sets m

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ∧ measure m (m_space m) ≠ +∞ ⇒
    measure m s ≠ +∞

⊢ ∀m. measure_space m ⇒ finite_subadditive m

⊢ ∀m f n.
    measure_space m ∧ (∀i. i < n ⇒ f i ∈ measurable_sets m) ⇒
    BIGUNION (IMAGE f (count n)) ∈ measurable_sets m

⊢ ∀m. measure_space m ⇒ increasing m

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    s ∩ t ∈ measurable_sets m

⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ ∀x. x ∈ s ⇒ x ∈ m_space m

⊢ ∀m. measure_space m ⇒ m_space m ∈ measurable_sets m

⊢ ∀m. measure_space m ⇒ positive m

⊢ ∀m. (m_space m,measurable_sets m,measure m) = m

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    measure_space (s,IMAGE (λt. s ∩ t) (measurable_sets m),measure m)

⊢ ∀m s.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    measure_space (m_space m,measurable_sets m,(λa. measure m (s ∩ a)))

⊢ ∀sp sts m sub.
    measure_space (sp,sts,m) ∧ sub ⊆ sts ∧ sigma_algebra (sp,sub) ⇒
    measure_space (sp,sub,m)

⊢ ∀m sts.
    measure_space m ∧ sts ⊆ measurable_sets m ∧
    sigma_algebra (m_space m,sts) ⇒
    measure_space (m_space m,sts,measure m)

⊢ ∀m. measure_space m ⇒ sigma_algebra (measurable_space m)

⊢ ∀m. measure_space m ⇒ m_space m ∈ measurable_sets m

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

⊢ ∀m. measure_space m ⇒ subadditive m

⊢ ∀s s' m. s' ⊆ s ∧ measure_space (s,POW s,m) ⇒ measure_space (s',POW s',m)

⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ s ⊆ m_space m

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    s ∪ t ∈ measurable_sets m

⊢ ∀m s t u.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
    u = s ∪ t ⇒
    measure m u ≤ measure m s + measure m t

⊢ ∀m s t.
    measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
    measure m t = 0 ⇒
    measure m (s DIFF t) = measure m s

⊢ ∀m s f.
    measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    (∀n. f n ⊆ f (SUC n)) ∧ s = BIGUNION (IMAGE f 𝕌(:num)) ⇒
    sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s

⊢ ∀m f.
    measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    (∀n. f n ⊆ f (SUC n)) ⇒
    sup (IMAGE (measure m ∘ f) 𝕌(:num)) =
    measure m (BIGUNION (IMAGE f 𝕌(:num)))

⊢ ∀m s f.
    measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    (∀n. measure m (f n) ≠ +∞) ∧ (∀n. f (SUC n) ⊆ f n) ∧
    s = BIGINTER (IMAGE f 𝕌(:num)) ⇒
    inf (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s

⊢ ∀m f.
    measure_space m ∧ f ∈ (𝕌(:num) → measurable_sets m) ∧
    (∀n. measure m (f n) ≠ +∞) ∧ (∀n. f (SUC n) ⊆ f n) ⇒
    inf (IMAGE (measure m ∘ f) 𝕌(:num)) =
    measure m (BIGINTER (IMAGE f 𝕌(:num)))

⊢ ∀m f.
    measure_space m ∧ (∀n. f n ∈ null_set m) ⇒
    BIGUNION (IMAGE f 𝕌(:num)) ∈ null_set m

⊢ ∀m f.
    measure_space m ∧ (∀n. null_set m (f n)) ⇒
    null_set m (BIGUNION (IMAGE f 𝕌(:num)))

⊢ ∀m. measure_space m ⇒ null_set m ∅

⊢ ∀m N1 N2.
    measure_space m ∧ N1 ∈ null_set m ∧ N2 ∈ null_set m ⇒
    N1 ∩ N2 ∈ null_set m

⊢ ∀m N1 N2.
    measure_space m ∧ null_set m N1 ∧ null_set m N2 ⇒ null_set m (N1 ∩ N2)

⊢ ∀m s t.
    measure_space m ⇒
    t ∈ null_set m ∧ s ∈ measurable_sets m ∧ s ⊆ t ⇒
    s ∈ null_set m

⊢ ∀m s t.
    measure_space m ⇒
    ∅ ∈ null_set m ∧
    (t ∈ null_set m ∧ s ∈ measurable_sets m ∧ s ⊆ t ⇒ s ∈ null_set m) ∧
    ∀f. f ∈ (𝕌(:num) → null_set m) ⇒
        BIGUNION (IMAGE f 𝕌(:num)) ∈ null_set m

⊢ ∀m N1 N2.
    measure_space m ∧ N1 ∈ null_set m ∧ N2 ∈ null_set m ⇒
    N1 ∪ N2 ∈ null_set m

⊢ ∀m N1 N2.
    measure_space m ∧ null_set m N1 ∧ null_set m N2 ⇒ null_set m (N1 ∪ N2)

⊢ ∀sp sts m u.
    subset_class sp sts ∧ ∅ ∈ sts ∧ positive (sp,sts,m) ∧
    u = outer_measure m (countable_covers sts) ⇒
    outer_measure_space (sp,POW sp,u) ∧ (∀x. x ∈ sts ⇒ u x ≤ m x) ∧
    measure_space (sp,caratheodory_sets sp u,u) ∧
    ∀v. outer_measure_space (sp,POW sp,v) ∧ (∀x. x ∈ sts ⇒ v x ≤ m x) ⇒
        ∀x. x ⊆ sp ⇒ v x ≤ u x

⊢ ∀m. outer_measure_space m ⇒ finite_subadditive m

⊢ ∀m. outer_measure_space m ⇒ positive m

⊢ ∀m. outer_measure_space m ⇒ subadditive m

⊢ ∀m. ring (measurable_space m) ∧ positive m ∧ additive m ⇒
      finite_additive m ∧ increasing m ∧ subadditive m ∧
      finite_subadditive m

⊢ ∀m. ring (measurable_space m) ∧ positive m ∧ additive m ⇒
      finite_additive m

⊢ ∀m. ring (measurable_space m) ∧ positive m ∧ additive m ⇒ increasing m

⊢ ∀m s t.
    ring (measurable_space m) ∧ additive m ∧ positive m ∧
    s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
    measure m (s ∪ t) + measure m (s ∩ t) = measure m s + measure m t

⊢ ∀m. ring (measurable_space m) ∧ positive m ∧ additive m ⇒ subadditive m

⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ additive m

⊢ ∀m s f.
    ring (measurable_space m) ∧ premeasure m ∧
    f ∈ (𝕌(:num) → measurable_sets m) ∧ f 0 = ∅ ∧ (∀n. f n ⊆ f (SUC n)) ∧
    s = BIGUNION (IMAGE f 𝕌(:num)) ∧ s ∈ measurable_sets m ⇒
    sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s

⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ countably_subadditive m

⊢ ∀m s t.
    ring (measurable_space m) ∧ premeasure m ∧ s ∈ measurable_sets m ∧
    t ∈ measurable_sets m ∧ s ⊆ t ∧ measure m s < +∞ ⇒
    measure m (t DIFF s) = measure m t − measure m s

⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ finite_additive m

⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ finite_subadditive m

⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ increasing m

⊢ ∀m s t.
    ring (measurable_space m) ∧ premeasure m ∧ s ∈ measurable_sets m ∧
    t ∈ measurable_sets m ⇒
    measure m (s ∪ t) + measure m (s ∩ t) = measure m s + measure m t

⊢ ∀m. ring (measurable_space m) ∧ premeasure m ⇒ subadditive m

⊢ ∀m. ring (measurable_space m) ∧ positive m ∧ subadditive m ⇒
      finite_subadditive m

⊢ ∀m0.
    semiring (measurable_space m0) ∧ positive m0 ∧ finite_additive m0 ⇒
    ∃m. measurable_space m =
        smallest_ring (m_space m0) (measurable_sets m0) ∧
        (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
        positive m ∧ additive m

⊢ ∀m. semiring (measurable_space m) ∧ premeasure m ⇒ additive m

⊢ ∀m0.
    semiring (measurable_space m0) ∧ premeasure m0 ⇒
    ∃m. measurable_space m =
        smallest_ring (m_space m0) (measurable_sets m0) ∧
        (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
        premeasure m

⊢ ∀m. semiring (measurable_space m) ∧ premeasure m ⇒ finite_additive m

⊢ ∀m. semiring (measurable_space m) ∧ premeasure m ⇒ increasing m

⊢ ∀sp sts u v.
    semiring (sp,sts) ∧ has_exhausting_sequence (sp,sts) ∧
    measure_space (sp,subsets (sigma sp sts),u) ∧
    measure_space (sp,subsets (sigma sp sts),v) ∧
    (∀s. s ∈ sts ⇒ u s ≤ v s ∧ v s < +∞) ⇒
    ∀s. s ∈ subsets (sigma sp sts) ⇒ u s ≤ v s

⊢ ∀m. measure_space m ⇒ sigma_algebra (completion m)

⊢ ∀m. measure_space m ⇒
      (sigma_finite m ⇔
       ∃f. f ∈ (𝕌(:num) → measurable_sets m) ∧
           BIGUNION (IMAGE f 𝕌(:num)) = m_space m ∧
           ∀n. measure m (f n) < +∞)

⊢ ∀m. measure_space m ⇒
      (sigma_finite m ⇔
       ∃A. countable A ∧ A ⊆ measurable_sets m ∧ BIGUNION A = m_space m ∧
           ∀a. a ∈ A ⇒ measure m a ≠ +∞)

⊢ ∀a m.
    measure_space m ∧ a ⊆ measurable_sets m ⇒
    subsets (sigma (m_space m) a) ⊆ measurable_sets m

⊢ ∀s s'.
    s' ⊆ m_space s ∧ measure_space s ∧ POW s' ⊆ measurable_sets s ⇒
    measure_space (s',POW s',measure s)

⊢ ∀m s t u.
    subadditive m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
    u ∈ measurable_sets m ∧ u = s ∪ t ⇒
    measure m u ≤ measure m s + measure m t

⊢ ∀sp sts u v.
    subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
    sigma_finite (sp,sts,u) ∧ measure_space (sp,subsets (sigma sp sts),u) ∧
    measure_space (sp,subsets (sigma sp sts),v) ∧ (∀s. s ∈ sts ⇒ u s = v s) ⇒
    ∀s. s ∈ subsets (sigma sp sts) ⇒ u s = v s

⊢ ∀sp sts u v.
    subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
    measure_space (sp,subsets (sigma sp sts),u) ∧
    measure_space (sp,subsets (sigma sp sts),v) ∧ u sp = v sp ∧ u sp < +∞ ∧
    (∀s. s ∈ sts ⇒ u s = v s) ⇒
    ∀s. s ∈ subsets (sigma sp sts) ⇒ u s = v s

⊢ ∀sts.
    countable_covers sts =
    (λa. {f | f ∈ (𝕌(:num) → sts) ∧ a ⊆ BIGUNION (IMAGE f 𝕌(:num))})

⊢ ∀sp M u.
    countably_additive (sp,M,u) ⇔
    ∀A. IMAGE A 𝕌(:num) ⊆ M ⇒
        disjoint_family A ⇒
        BIGUNION {A i | i ∈ 𝕌(:num)} ∈ M ⇒
        u (BIGUNION {A i | i ∈ 𝕌(:num)}) = suminf (u ∘ A)

⊢ ∀sp M u u'.
    (∀a. a ∈ M ⇒ u' a = u a) ⇒
    (countably_additive (sp,M,u') ⇔ countably_additive (sp,M,u))

⊢ ∀sp M u. countably_additive (sp,M,u) ⇔ countably_additive_alt M u

⊢ ∀A f x i.
    disjoint_family A ∧ x ∈ A i ∧ (∀i. 0 ≤ f i) ⇒
    suminf (λn. f n * 𝟙 (A n) x) = f i

⊢ ∀s m.
    sigma_algebra s ∧ FINITE (space s) ∧ positive (space s,subsets s,m) ∧
    additive (space s,subsets s,m) ⇒
    measure_space (space s,subsets s,m)

⊢ ∀m. sigma_algebra (measurable_space m) ∧ FINITE (m_space m) ∧
      positive m ∧ additive m ⇒
      measure_space m

⊢ ∀m. finite_measure_space m ⇔
      sigma_finite_measure_space m ∧ measure m (m_space m) ≠ +∞

⊢ ∀m. finite_measure_space m ⇔
      measure_space m ∧
      ∀s. s ∈ measurable_sets m ⇒ measure m s ≠ −∞ ∧ measure m s ≠ +∞

⊢ ∀m f n x k.
    x ∈ m_space m ∧ k ∈ count (4 ** n) ∧ &k / 2 pow n ≤ f x ∧
    f x < (&k + 1) / 2 pow n ⇒
    fn_seq m f n x = &k / 2 pow n

⊢ ∀m f n x. x ∈ m_space m ∧ 2 pow n ≤ f x ⇒ fn_seq m f n x = 2 pow n

⊢ ∀m f n x.
    x ∈ m_space m ∧ 0 ≤ f x ⇒
    2 pow n ≤ f x ∨
    ∃k. k ∈ count (4 ** n) ∧ &k / 2 pow n ≤ f x ∧ f x < (&k + 1) / 2 pow n

⊢ ∀m f n x. x ∉ m_space m ⇒ fn_seq m f n x = 0

⊢ ∀m f x. 0 ≤ f x ⇒ mono_increasing (λn. fn_seq m f n x)

⊢ ∀m f n x. 0 ≤ f x ⇒ 0 ≤ fn_seq m f n x

⊢ ∀m f n x. x ∈ m_space m ∧ 0 ≤ f x ⇒ 0 ≤ fn_seq m f n x

⊢ ∀m f x.
    x ∈ m_space m ∧ 0 ≤ f x ⇒
    sup (IMAGE (λn. fn_seq m f n x) 𝕌(:num)) = f x

⊢ ∀m f n x. 0 ≤ f x ⇒ fn_seq m f n x ≤ f x

⊢ ∀m f n x. x ∈ m_space m ∧ 0 ≤ f x ⇒ fn_seq m f n x ≤ f x

⊢ ∀a A.
    sigma_algebra a ∧ (∀n. A n ∈ subsets a) ⇒
    limsup A = {x | x ∈ space a ∧ suminf (λn. 𝟙 (A n) x) = +∞}

⊢ ∀m. measure_absolutely_continuous' m m

⊢ ∀m u v. u ≪ m ∧ v ≪ (m_space m,measurable_sets m,u) ⇒ v ≪ m

⊢ ∀p A.
    measure_space p ∧ (∀n. A n ∈ measurable_sets p) ⇒
    measure p (liminf A) =
    sup (IMAGE (λm. measure p (BIGINTER {A n | m ≤ n})) 𝕌(:num))

⊢ ∀p A.
    measure_space p ∧ measure p (BIGUNION (IMAGE A 𝕌(:num))) < +∞ ∧
    (∀n. A n ∈ measurable_sets p) ⇒
    measure p (limsup A) =
    inf (IMAGE (λm. measure p (BIGUNION {A n | m ≤ n})) 𝕌(:num))

⊢ ∀p A.
    measure_space p ∧ measure p (m_space p) < +∞ ∧
    (∀n. A n ∈ measurable_sets p) ⇒
    measure p (limsup A) =
    inf (IMAGE (λm. measure p (BIGUNION {A n | m ≤ n})) 𝕌(:num))

⊢ measure_of m =
  (m_space m,
   if measurable_sets m ⊆ POW (m_space m) then
     sigma_sets (m_space m) (measurable_sets m)
   else {∅; m_space m},
   (λa.
        if
          a ∈ sigma_sets (m_space m) (measurable_sets m) ∧
          measure_space
            (m_space m,sigma_sets (m_space m) (measurable_sets m),measure m)
        then
          measure m a
        else 0))

⊢ ∀sp A u u'.
    A ⊆ POW sp ∧ (∀a. a ∈ sigma_sets sp A ⇒ u a = u' a) ⇒
    measure_of (sp,A,u) = measure_of (sp,A,u')

⊢ ∀M N.
    measure_space M ∧ measure_space N ∧
    measurable_sets M = measurable_sets N ∧
    (∀A. A ∈ measurable_sets M ⇒ measure M A = measure N A) ⇒
    measure_of M = measure_of N

⊢ ∀m. measure_space m ⇒ measure_space (measure_of m)

⊢ ∀M. measure_of M = measure_of (m_space M,measurable_sets M,measure M)

⊢ measure (restrict_space M sp) = measure M

⊢ ∀sp sts u v.
    measure_space (sp,sts,u) ∧ measure_space (sp,sts,v) ⇒
    measure_space (sp,sts,(λs. u s + v s))

⊢ ∀a mu nu p.
    measure_space (space a,subsets a,mu) ∧
    measure_space (space a,subsets a,nu) ∧
    (∀s. s ∈ subsets a ⇒ p s = mu s + nu s) ⇒
    measure_space (space a,subsets a,p)

⊢ ∀sp M u.
    measure_space (sp,M,u) ⇔
    sigma_algebra_alt sp M ∧ positive_alt M u ∧ countably_additive_alt M u

⊢ ∀a u v c.
    measure_space (space a,subsets a,u) ∧ 0 ≤ c ∧
    (∀s. s ∈ subsets a ⇒ v s = c * u s) ⇒
    measure_space (space a,subsets a,v)

⊢ ∀sp sts u v.
    (∀s. s ∈ sts ⇒ u s = v s) ⇒
    (measure_space (sp,sts,u) ⇔ measure_space (sp,sts,v))

⊢ ∀a x. sigma_algebra a ⇒ measure_space (space a,subsets a,C 𝟙 x)

⊢ ∀m1 m2.
    measure_space m1 ∧ m_space m2 = m_space m1 ∧
    measurable_sets m2 = measurable_sets m1 ∧
    (∀s. s ∈ measurable_sets m2 ⇒ measure m2 s = measure m1 s) ⇒
    measure_space m2

⊢ ∀m1 m2. measure_space m1 ∧ measure_space_eq m1 m2 ⇒ measure_space m2

⊢ ∀m1 m2. measure_space_eq m1 m2 ⇒ measure_space_eq m2 m1

⊢ ∀m. measure_space m ⇒ measure_space_eq m (measure_of m)

⊢ ∀m. measure_space m ⇒ measure_space_eq (measure_of m) m

⊢ ∀M N. measure_space_eq M N ⇔ measure_space_eq N M

⊢ ∀m1 m2 m3.
    measure_space_eq m1 m2 ∧ measure_space_eq m2 m3 ⇒
    measure_space_eq m1 m3

⊢ ∀sp sts u v.
    measure_space (sp,sts,u) ∧ (∀s. s ∈ sts ⇒ u s = v s) ⇒
    measure_space (sp,sts,v)

⊢ ∀M sp.
    measure_space M ∧ sp ∈ measurable_sets M ⇒
    measure_space (restrict_space M sp)

⊢ ∀sp A u u'.
    A ⊆ POW sp ∧ (∀a. a ∈ sigma_sets sp A ⇒ u a = u' a) ⇒
    (measure_space (sp,sigma_sets sp A,u) ⇔
     measure_space (sp,sigma_sets sp A,u'))

⊢ ∀a f m s.
    FINITE s ∧ sigma_algebra a ∧
    (∀i. i ∈ s ⇒ measure_space (space a,subsets a,f i)) ∧
    (∀t. t ∈ subsets a ⇒ m t = ∑ (C f t) s) ⇒
    measure_space (space a,subsets a,m)

⊢ ∀a g m.
    (∀n. measure_space (space a,subsets a,g n)) ∧
    (∀s. s ∈ subsets a ⇒ m s = suminf (C g s)) ⇒
    measure_space (space a,subsets a,m)

⊢ ∀a. sigma_algebra a ⇒
      sigma_finite_measure_space (space a,subsets a,(λs. 0))

⊢ ∀a. sigma_algebra a ⇒ measure_space (space a,subsets a,(λs. 0))

⊢ ∀r b m.
    measure_space m ∧ FINITE r ∧ BIGUNION (IMAGE b r) = m_space m ∧
    (∀i j. i ∈ r ∧ j ∈ r ∧ i ≠ j ⇒ DISJOINT (b i) (b j)) ∧
    (∀i. i ∈ r ⇒ b i ∈ measurable_sets m) ⇒
    ∀a. a ∈ measurable_sets m ⇒ measure m a = ∑ (λi. measure m (a ∩ b i)) r

⊢ ∀J A M.
    measure_space M ∧ FINITE J ∧ IMAGE A J ⊆ measurable_sets M ⇒
    measure M (BIGUNION {A i | i ∈ J}) ≤ ∑ (λi. measure M (A i)) J

⊢ null_set M = {N | N ∈ measurable_sets M ∧ measure M N = 0}

⊢ ∀sp M u. positive (sp,M,u) ⇔ u ∅ = 0 ∧ ∀a. a ∈ M ⇒ 0 ≤ u a

⊢ ∀sp M u u'.
    ring (sp,M) ∧ (∀a. a ∈ M ⇒ u' a = u a) ⇒
    (positive (sp,M,u) ⇔ positive (sp,M,u'))

⊢ ∀sp M u. positive (sp,M,u) ⇔ positive_alt M u

⊢ ∀m. positive m ⇒ ∀s. s ∈ measurable_sets m ⇒ measure m s ≠ −∞

⊢ ∀M sp.
    measure_space M ∧ sp ∈ measurable_sets M ⇒
    measurable_sets (restrict_space M sp) ⊆ measurable_sets M

⊢ ∀M sp.
    restrict_space M sp =
    (space (restrict_algebra (measurable_space M) sp),
     subsets (restrict_algebra (measurable_space M) sp),measure M)

⊢ ∀M M'.
    measure_space M ∧ measure_space M' ∧
    measurable_sets M = measurable_sets M' ⇒
    m_space M = m_space M'

⊢ ∀M sp.
    measurable_sets (restrict_space M sp) =
    IMAGE (λa. a ∩ sp) (measurable_sets M)

⊢ ∀m. sigma_finite m ⇔
      ∃f. (f ∈ (𝕌(:num) → measurable_sets m) ∧ (∀m n. m ≤ n ⇒ f m ⊆ f n) ∧
           BIGUNION (IMAGE f 𝕌(:num)) = m_space m) ∧
          ∀n. measure m (f n) < +∞

⊢ ∀m. sigma_finite m ⇔
      ∃f. exhausting_sequence (measurable_space m) f ∧
          ∀n. measure m (f n) < +∞

⊢ ∀m. sigma_finite m ⇔
      ∃f. f ∈ (𝕌(:num) → measurable_sets m) ∧ (∀n. f n ⊆ f (SUC n)) ∧
          BIGUNION (IMAGE f 𝕌(:num)) = m_space m ∧ ∀n. measure m (f n) < +∞

⊢ ∀m. measure_space m ∧ sigma_finite m ⇒
      ∃A. IMAGE A 𝕌(:num) ⊆ measurable_sets m ∧
          BIGUNION {A i | i ∈ 𝕌(:num)} = m_space m ∧
          (∀i. measure m (A i) ≠ +∞) ∧ disjoint_family A

⊢ ∀sp sts u. sigma_finite (sp,sts,u) ⇒ has_exhausting_sequence (sp,sts)

⊢ ∀m. sigma_finite_measure_space m ⇒ measure_space m

⊢ ∀m. measure_space m ∧ sigma_finite m ⇒
      ∃A. IMAGE A 𝕌(:num) ⊆ measurable_sets m ∧
          BIGUNION {A i | i ∈ 𝕌(:num)} = m_space m ∧
          ∀i. measure m (A i) ≠ +∞

⊢ ∀M sp. m_space (restrict_space M sp) = sp ∩ m_space M

⊢ ∀M sp.
    measure_space M ∧ sp ∈ measurable_sets M ⇒
    m_space (restrict_space M sp) = sp

⊢ ∀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 ⇒
    ∃A0 B.
      A0 ∈ measurable_sets M ∧ disjoint_family B ∧
      IMAGE B 𝕌(:num) ⊆ measurable_sets M ∧
      A0 = m_space M DIFF BIGUNION {B i | i ∈ 𝕌(:num)} ∧
      (∀A. A ∈ measurable_sets M ∧ A ⊆ A0 ⇒
           measure M A = 0 ∧ measure N A = 0 ∨
           0 < measure M A ∧ measure N A = +∞) ∧ ∀i. measure N (B i) ≠ +∞