Structure measureTheory

signature measureTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val additive_def : thm
    val caratheodory_sets_def : thm
    val complete_measure_space_def : thm
    val complete_of_def : thm
    val countable_covers_def : thm
    val countably_additive_def : thm
    val countably_subadditive_def : thm
    val finite_additive_def : thm
    val finite_subadditive_def : thm
    val increasing_def : thm
    val m_space_def : thm
    val measurable_sets_def : thm
    val measure_def : thm
    val measure_preserving_def : thm
    val measure_space_def : thm
    val null_set_def : thm
    val outer_measure_def : thm
    val outer_measure_space_def : thm
    val positive_def : thm
    val premeasure_def : thm
    val sigma_finite_def : thm
    val sigma_finite_measure_space_def : thm
    val subadditive_def : thm
  
  (*  Theorems  *)
    val ADDITIVE : thm
    val ADDITIVE_INCREASING : thm
    val ADDITIVE_SUM : thm
    val ALGEBRA_COUNTABLY_ADDITIVE_ADDITIVE : thm
    val ALGEBRA_PREMEASURE_ADDITIVE : thm
    val ALGEBRA_PREMEASURE_COMPL : thm
    val ALGEBRA_PREMEASURE_COUNTABLE_INCREASING : thm
    val ALGEBRA_PREMEASURE_COUNTABLY_SUBADDITIVE : thm
    val ALGEBRA_PREMEASURE_DIFF_SUBSET : thm
    val ALGEBRA_PREMEASURE_FINITE_ADDITIVE : thm
    val ALGEBRA_PREMEASURE_FINITE_SUBADDITIVE : thm
    val ALGEBRA_PREMEASURE_INCREASING : thm
    val ALGEBRA_PREMEASURE_STRONG_ADDITIVE : thm
    val ALGEBRA_PREMEASURE_SUBADDITIVE : thm
    val BIGUNION_IMAGE_Q : thm
    val CARATHEODORY : thm
    val CARATHEODORY_RING : thm
    val CARATHEODORY_SEMIRING : thm
    val COMPLETE_MEASURE_THM : thm
    val COUNTABLY_ADDITIVE : thm
    val COUNTABLY_ADDITIVE_ADDITIVE : thm
    val COUNTABLY_ADDITIVE_FINITE_ADDITIVE : thm
    val COUNTABLY_SUBADDITIVE : thm
    val COUNTABLY_SUBADDITIVE_FINITE_SUBADDITIVE : thm
    val COUNTABLY_SUBADDITIVE_SUBADDITIVE : thm
    val DYNKIN_SYSTEM_DIFF_SUBSET : thm
    val DYNKIN_SYSTEM_PREMEASURE_ADDITIVE : thm
    val DYNKIN_SYSTEM_PREMEASURE_FINITE_ADDITIVE : thm
    val DYNKIN_SYSTEM_PREMEASURE_INCREASING : thm
    val FINITE_ADDITIVE : thm
    val FINITE_ADDITIVE_ALT : thm
    val FINITE_IMP_SIGMA_FINITE : thm
    val FINITE_SUBADDITIVE : thm
    val FINITE_SUBADDITIVE_ALT : thm
    val INCREASING : thm
    val IN_MEASURE_PRESERVING : thm
    val IN_NULL_SET : thm
    val MEASURABLE_IF : thm
    val MEASURABLE_IF_SET : thm
    val MEASURABLE_POW_TO_POW : thm
    val MEASURABLE_POW_TO_POW_IMAGE : thm
    val MEASURABLE_RANGE_REDUCE : thm
    val MEASURABLE_SETS_SUBSET_SPACE : thm
    val MEASURE_ADDITIVE : thm
    val MEASURE_COMPL : thm
    val MEASURE_COMPL_SUBSET : thm
    val MEASURE_COUNTABLE_INCREASING : thm
    val MEASURE_COUNTABLY_ADDITIVE : thm
    val MEASURE_DIFF_SUBSET : thm
    val MEASURE_DOWN : thm
    val MEASURE_EMPTY : thm
    val MEASURE_EXTREAL_SUM_IMAGE : thm
    val MEASURE_FINITE_ADDITIVE : thm
    val MEASURE_PRESERVING_LIFT : thm
    val MEASURE_PRESERVING_SUBSET : thm
    val MEASURE_PRESERVING_UP_LIFT : thm
    val MEASURE_PRESERVING_UP_SIGMA : thm
    val MEASURE_PRESERVING_UP_SUBSET : thm
    val MEASURE_SPACE_ADDITIVE : thm
    val MEASURE_SPACE_BIGINTER : thm
    val MEASURE_SPACE_BIGUNION : thm
    val MEASURE_SPACE_CMUL : thm
    val MEASURE_SPACE_COMPL : thm
    val MEASURE_SPACE_COUNTABLY_SUBADDITIVE : thm
    val MEASURE_SPACE_DIFF : thm
    val MEASURE_SPACE_EMPTY_MEASURABLE : thm
    val MEASURE_SPACE_FINITE_DIFF : thm
    val MEASURE_SPACE_FINITE_DIFF_SUBSET : thm
    val MEASURE_SPACE_FINITE_MEASURE : thm
    val MEASURE_SPACE_FINITE_SUBADDITIVE : thm
    val MEASURE_SPACE_INCREASING : thm
    val MEASURE_SPACE_INTER : thm
    val MEASURE_SPACE_IN_MSPACE : thm
    val MEASURE_SPACE_MSPACE_MEASURABLE : thm
    val MEASURE_SPACE_POSITIVE : thm
    val MEASURE_SPACE_REDUCE : thm
    val MEASURE_SPACE_RESTRICTED : thm
    val MEASURE_SPACE_RESTRICTED_MEASURE : thm
    val MEASURE_SPACE_RESTRICTION : thm
    val MEASURE_SPACE_SPACE : thm
    val MEASURE_SPACE_STRONG_ADDITIVE : thm
    val MEASURE_SPACE_SUBADDITIVE : thm
    val MEASURE_SPACE_SUBSET : thm
    val MEASURE_SPACE_SUBSET_MSPACE : thm
    val MEASURE_SPACE_UNION : thm
    val MONOTONE_CONVERGENCE : thm
    val MONOTONE_CONVERGENCE2 : thm
    val MONOTONE_CONVERGENCE_BIGINTER : thm
    val MONOTONE_CONVERGENCE_BIGINTER2 : thm
    val NULL_SET_EMPTY : thm
    val NULL_SET_INTER : thm
    val NULL_SET_THM : thm
    val NULL_SET_UNION : thm
    val OUTER_MEASURE_CONSTRUCTION : thm
    val OUTER_MEASURE_SPACE_FINITE_SUBADDITIVE : thm
    val OUTER_MEASURE_SPACE_POSITIVE : thm
    val OUTER_MEASURE_SPACE_SUBADDITIVE : thm
    val RING_ADDITIVE_EVERYTHING : thm
    val RING_ADDITIVE_FINITE_ADDITIVE : thm
    val RING_ADDITIVE_INCREASING : thm
    val RING_ADDITIVE_STRONG_ADDITIVE : thm
    val RING_ADDITIVE_SUBADDITIVE : thm
    val RING_PREMEASURE_ADDITIVE : thm
    val RING_PREMEASURE_COUNTABLE_INCREASING : thm
    val RING_PREMEASURE_COUNTABLY_SUBADDITIVE : thm
    val RING_PREMEASURE_DIFF_SUBSET : thm
    val RING_PREMEASURE_FINITE_ADDITIVE : thm
    val RING_PREMEASURE_FINITE_SUBADDITIVE : thm
    val RING_PREMEASURE_INCREASING : thm
    val RING_PREMEASURE_STRONG_ADDITIVE : thm
    val RING_PREMEASURE_SUBADDITIVE : thm
    val RING_SUBADDITIVE_FINITE_SUBADDITIVE : thm
    val SEMIRING_FINITE_ADDITIVE_EXTENSION : thm
    val SEMIRING_PREMEASURE_ADDITIVE : thm
    val SEMIRING_PREMEASURE_EXTENSION : thm
    val SEMIRING_PREMEASURE_FINITE_ADDITIVE : thm
    val SEMIRING_PREMEASURE_INCREASING : thm
    val SIGMA_FINITE_ALT : thm
    val SIGMA_FINITE_ALT2 : thm
    val SIGMA_SUBSET_MEASURABLE_SETS : thm
    val STRONG_MEASURE_SPACE_SUBSET : thm
    val SUBADDITIVE : thm
    val UNIQUENESS_OF_MEASURE : thm
    val UNIQUENESS_OF_MEASURE_FINITE : thm
    val countably_additive_alt_eq : thm
    val finite_additivity_sufficient_for_finite_spaces : thm
    val finite_additivity_sufficient_for_finite_spaces2 : thm
    val measure_space_eq : thm
    val measure_space_trivial : thm
    val measure_split : thm
    val null_sets : thm
    val positive_not_infty : thm
    val sets_eq_imp_space_eq : thm
    val sigma_finite : thm
    val sigma_finite_disjoint : thm
  
  val measure_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [extreal] Parent theory of "measure"
   
   [sigma_algebra] Parent theory of "measure"
   
   [additive_def]  Definition
      
      ⊢ ∀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
   
   [caratheodory_sets_def]  Definition
      
      ⊢ ∀sp m.
          caratheodory_sets sp m =
          {a | a ⊆ sp ∧ ∀q. q ⊆ sp ⇒ m q = m (q ∩ a) + m (q DIFF a)}
   
   [complete_measure_space_def]  Definition
      
      ⊢ ∀m. complete_measure_space m ⇔
            measure_space m ∧
            ∀s. null_set m s ⇒ ∀t. t ⊆ s ⇒ t ∈ measurable_sets m
   
   [complete_of_def]  Definition
      
      ⊢ ∀m. complete_of m =
            (m_space m,
             {s ∪ n | s ∈ measurable_sets m ∧ ∃t. n ⊆ t ∧ null_set m t},
             measure m)
   
   [countable_covers_def]  Definition
      
      ⊢ ∀sts.
          countable_covers sts =
          (λa. {f | f ∈ (𝕌(:num) → sts) ∧ a ⊆ BIGUNION (IMAGE f 𝕌(:num))})
   
   [countably_additive_def]  Definition
      
      ⊢ ∀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)
   
   [countably_subadditive_def]  Definition
      
      ⊢ ∀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)
   
   [finite_additive_def]  Definition
      
      ⊢ ∀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)
   
   [finite_subadditive_def]  Definition
      
      ⊢ ∀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)
   
   [increasing_def]  Definition
      
      ⊢ ∀m. increasing m ⇔
            ∀s t.
              s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ s ⊆ t ⇒
              measure m s ≤ measure m t
   
   [m_space_def]  Definition
      
      ⊢ ∀sp sts mu. m_space (sp,sts,mu) = sp
   
   [measurable_sets_def]  Definition
      
      ⊢ ∀sp sts mu. measurable_sets (sp,sts,mu) = sts
   
   [measure_def]  Definition
      
      ⊢ ∀sp sts mu. measure (sp,sts,mu) = mu
   
   [measure_preserving_def]  Definition
      
      ⊢ ∀m1 m2.
          measure_preserving m1 m2 =
          {f |
           f ∈
           measurable (m_space m1,measurable_sets m1)
             (m_space m2,measurable_sets m2) ∧
           ∀s. s ∈ measurable_sets m2 ⇒
               measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s}
   
   [measure_space_def]  Definition
      
      ⊢ ∀m. measure_space m ⇔
            sigma_algebra (m_space m,measurable_sets m) ∧ positive m ∧
            countably_additive m
   
   [null_set_def]  Definition
      
      ⊢ ∀m s. null_set m s ⇔ s ∈ measurable_sets m ∧ measure m s = 0
   
   [outer_measure_def]  Definition
      
      ⊢ ∀m C.
          outer_measure m C =
          (λa. inf {r | (∃f. f ∈ C a ∧ suminf (m ∘ f) = r)})
   
   [outer_measure_space_def]  Definition
      
      ⊢ ∀m. outer_measure_space m ⇔
            subset_class (m_space m) (measurable_sets m) ∧
            ∅ ∈ measurable_sets m ∧ positive m ∧ increasing m ∧
            countably_subadditive m
   
   [positive_def]  Definition
      
      ⊢ ∀m. positive m ⇔
            measure m ∅ = 0 ∧ ∀s. s ∈ measurable_sets m ⇒ 0 ≤ measure m s
   
   [premeasure_def]  Definition
      
      ⊢ ∀m. premeasure m ⇔ positive m ∧ countably_additive m
   
   [sigma_finite_def]  Definition
      
      ⊢ ∀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) < +∞
   
   [sigma_finite_measure_space_def]  Definition
      
      ⊢ ∀m. sigma_finite_measure_space m ⇔ measure_space m ∧ sigma_finite m
   
   [subadditive_def]  Definition
      
      ⊢ ∀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
   
   [ADDITIVE]  Theorem
      
      ⊢ ∀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
   
   [ADDITIVE_INCREASING]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
            increasing m
   
   [ADDITIVE_SUM]  Theorem
      
      ⊢ ∀m f n.
          algebra (m_space m,measurable_sets 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)))
   
   [ALGEBRA_COUNTABLY_ADDITIVE_ADDITIVE]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ positive m ∧
            countably_additive m ⇒
            additive m
   
   [ALGEBRA_PREMEASURE_ADDITIVE]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ premeasure m ⇒
            additive m
   
   [ALGEBRA_PREMEASURE_COMPL]  Theorem
      
      ⊢ ∀m s.
          algebra (m_space m,measurable_sets 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
   
   [ALGEBRA_PREMEASURE_COUNTABLE_INCREASING]  Theorem
      
      ⊢ ∀m s f.
          algebra (m_space m,measurable_sets 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
   
   [ALGEBRA_PREMEASURE_COUNTABLY_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ premeasure m ⇒
            countably_subadditive m
   
   [ALGEBRA_PREMEASURE_DIFF_SUBSET]  Theorem
      
      ⊢ ∀m s t.
          algebra (m_space m,measurable_sets 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
   
   [ALGEBRA_PREMEASURE_FINITE_ADDITIVE]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ premeasure m ⇒
            finite_additive m
   
   [ALGEBRA_PREMEASURE_FINITE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ premeasure m ⇒
            finite_subadditive m
   
   [ALGEBRA_PREMEASURE_INCREASING]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ premeasure m ⇒
            increasing m
   
   [ALGEBRA_PREMEASURE_STRONG_ADDITIVE]  Theorem
      
      ⊢ ∀m s t.
          algebra (m_space m,measurable_sets 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
   
   [ALGEBRA_PREMEASURE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. algebra (m_space m,measurable_sets m) ∧ premeasure m ⇒
            subadditive m
   
   [BIGUNION_IMAGE_Q]  Theorem
      
      ⊢ ∀a f.
          sigma_algebra a ∧ f ∈ (ℚ → subsets a) ⇒
          BIGUNION (IMAGE f ℚ) ∈ subsets a
   
   [CARATHEODORY]  Theorem
      
      ⊢ ∀m0.
          algebra (m_space m0,measurable_sets m0) ∧ positive m0 ∧
          countably_additive m0 ⇒
          ∃m. (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
              (m_space m,measurable_sets m) =
              sigma (m_space m0) (measurable_sets m0) ∧ measure_space m
   
   [CARATHEODORY_RING]  Theorem
      
      ⊢ ∀m0.
          ring (m_space m0,measurable_sets m0) ∧ positive m0 ∧
          countably_additive m0 ⇒
          ∃m. (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
              (m_space m,measurable_sets m) =
              sigma (m_space m0) (measurable_sets m0) ∧ measure_space m
   
   [CARATHEODORY_SEMIRING]  Theorem
      
      ⊢ ∀m0.
          semiring (m_space m0,measurable_sets m0) ∧ premeasure m0 ⇒
          ∃m. (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
              (m_space m,measurable_sets m) =
              sigma (m_space m0) (measurable_sets m0) ∧ measure_space m
   
   [COMPLETE_MEASURE_THM]  Theorem
      
      ⊢ ∀m s t.
          complete_measure_space m ∧ t ∈ null_set m ∧ s ⊆ t ⇒
          s ∈ null_set m
   
   [COUNTABLY_ADDITIVE]  Theorem
      
      ⊢ ∀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
   
   [COUNTABLY_ADDITIVE_ADDITIVE]  Theorem
      
      ⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_additive m ⇒
            additive m
   
   [COUNTABLY_ADDITIVE_FINITE_ADDITIVE]  Theorem
      
      ⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_additive m ⇒
            finite_additive m
   
   [COUNTABLY_SUBADDITIVE]  Theorem
      
      ⊢ ∀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)
   
   [COUNTABLY_SUBADDITIVE_FINITE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_subadditive m ⇒
            finite_subadditive m
   
   [COUNTABLY_SUBADDITIVE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. ∅ ∈ measurable_sets m ∧ positive m ∧ countably_subadditive m ⇒
            subadditive m
   
   [DYNKIN_SYSTEM_DIFF_SUBSET]  Theorem
      
      ⊢ ∀d s t.
          dynkin_system d ∧ s ∈ subsets d ∧ t ∈ subsets d ∧ s ⊆ t ⇒
          t DIFF s ∈ subsets d
   
   [DYNKIN_SYSTEM_PREMEASURE_ADDITIVE]  Theorem
      
      ⊢ ∀m. dynkin_system (m_space m,measurable_sets m) ∧ premeasure m ⇒
            additive m
   
   [DYNKIN_SYSTEM_PREMEASURE_FINITE_ADDITIVE]  Theorem
      
      ⊢ ∀m. dynkin_system (m_space m,measurable_sets m) ∧ premeasure m ⇒
            finite_additive m
   
   [DYNKIN_SYSTEM_PREMEASURE_INCREASING]  Theorem
      
      ⊢ ∀m. dynkin_system (m_space m,measurable_sets m) ∧ premeasure m ⇒
            increasing m
   
   [FINITE_ADDITIVE]  Theorem
      
      ⊢ ∀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
   
   [FINITE_ADDITIVE_ALT]  Theorem
      
      ⊢ ∀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)
   
   [FINITE_IMP_SIGMA_FINITE]  Theorem
      
      ⊢ ∀m. measure_space m ∧ measure m (m_space m) ≠ +∞ ⇒ sigma_finite m
   
   [FINITE_SUBADDITIVE]  Theorem
      
      ⊢ ∀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)
   
   [FINITE_SUBADDITIVE_ALT]  Theorem
      
      ⊢ ∀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
   
   [INCREASING]  Theorem
      
      ⊢ ∀m s t.
          increasing m ∧ s ⊆ t ∧ s ∈ measurable_sets m ∧
          t ∈ measurable_sets m ⇒
          measure m s ≤ measure m t
   
   [IN_MEASURE_PRESERVING]  Theorem
      
      ⊢ ∀m1 m2 f.
          f ∈ measure_preserving m1 m2 ⇔
          f ∈
          measurable (m_space m1,measurable_sets m1)
            (m_space m2,measurable_sets m2) ∧
          ∀s. s ∈ measurable_sets m2 ⇒
              measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s
   
   [IN_NULL_SET]  Theorem
      
      ⊢ ∀m s. s ∈ null_set m ⇔ null_set m s
   
   [MEASURABLE_IF]  Theorem
      
      ⊢ ∀f g M N P.
          f ∈
          measurable (m_space M,measurable_sets M)
            (m_space N,measurable_sets N) ∧
          g ∈
          measurable (m_space M,measurable_sets M)
            (m_space N,measurable_sets N) ∧
          {x | x ∈ m_space M ∧ P x} ∈ measurable_sets M ∧ measure_space M ⇒
          (λx. if P x then f x else g x) ∈
          measurable (m_space M,measurable_sets M)
            (m_space N,measurable_sets N)
   
   [MEASURABLE_IF_SET]  Theorem
      
      ⊢ ∀f g M N A.
          f ∈
          measurable (m_space M,measurable_sets M)
            (m_space N,measurable_sets N) ∧
          g ∈
          measurable (m_space M,measurable_sets M)
            (m_space N,measurable_sets N) ∧
          A ∩ m_space M ∈ measurable_sets M ∧ measure_space M ⇒
          (λx. if x ∈ A then f x else g x) ∈
          measurable (m_space M,measurable_sets M)
            (m_space N,measurable_sets N)
   
   [MEASURABLE_POW_TO_POW]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ measurable_sets m = POW (m_space m) ⇒
          f ∈ measurable (m_space m,measurable_sets m) (𝕌(:β),POW 𝕌(:β))
   
   [MEASURABLE_POW_TO_POW_IMAGE]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧ measurable_sets m = POW (m_space m) ⇒
          f ∈
          measurable (m_space m,measurable_sets m)
            (IMAGE f (m_space m),POW (IMAGE f (m_space m)))
   
   [MEASURABLE_RANGE_REDUCE]  Theorem
      
      ⊢ ∀m f s.
          measure_space m ∧
          f ∈ measurable (m_space m,measurable_sets m) (s,POW s) ∧ s ≠ ∅ ⇒
          f ∈
          measurable (m_space m,measurable_sets m)
            (s ∩ IMAGE f (m_space m),POW (s ∩ IMAGE f (m_space m)))
   
   [MEASURABLE_SETS_SUBSET_SPACE]  Theorem
      
      ⊢ ∀m s. measure_space m ∧ s ∈ measurable_sets m ⇒ s ⊆ m_space m
   
   [MEASURE_ADDITIVE]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_COMPL]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_COMPL_SUBSET]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_COUNTABLE_INCREASING]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_COUNTABLY_ADDITIVE]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_DIFF_SUBSET]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_DOWN]  Theorem
      
      ⊢ ∀m0 m1.
          sigma_algebra (m_space m0,measurable_sets m0) ∧
          measurable_sets m0 ⊆ measurable_sets m1 ∧
          measure m0 = measure m1 ∧ measure_space m1 ⇒
          measure_space m0
   
   [MEASURE_EMPTY]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ measure m ∅ = 0
   
   [MEASURE_EXTREAL_SUM_IMAGE]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_FINITE_ADDITIVE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ finite_additive m
   
   [MEASURE_PRESERVING_LIFT]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_PRESERVING_SUBSET]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_PRESERVING_UP_LIFT]  Theorem
      
      ⊢ ∀m1 m2 f a.
          f ∈ measure_preserving (m_space m1,a,measure m1) m2 ∧
          sigma_algebra (m_space m1,measurable_sets m1) ∧
          a ⊆ measurable_sets m1 ⇒
          f ∈ measure_preserving m1 m2
   
   [MEASURE_PRESERVING_UP_SIGMA]  Theorem
      
      ⊢ ∀m1 m2 a.
          measurable_sets m1 = subsets (sigma (m_space m1) a) ⇒
          measure_preserving (m_space m1,a,measure m1) m2 ⊆
          measure_preserving m1 m2
   
   [MEASURE_PRESERVING_UP_SUBSET]  Theorem
      
      ⊢ ∀m1 m2 a.
          a ⊆ measurable_sets m1 ∧
          sigma_algebra (m_space m1,measurable_sets m1) ⇒
          measure_preserving (m_space m1,a,measure m1) m2 ⊆
          measure_preserving m1 m2
   
   [MEASURE_SPACE_ADDITIVE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ additive m
   
   [MEASURE_SPACE_BIGINTER]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
          BIGINTER (IMAGE s 𝕌(:num)) ∈ measurable_sets m
   
   [MEASURE_SPACE_BIGUNION]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ (∀n. s n ∈ measurable_sets m) ⇒
          BIGUNION (IMAGE s 𝕌(:num)) ∈ measurable_sets m
   
   [MEASURE_SPACE_CMUL]  Theorem
      
      ⊢ ∀m c.
          measure_space m ∧ 0 ≤ c ⇒
          measure_space
            (m_space m,measurable_sets m,(λa. Normal c * measure m a))
   
   [MEASURE_SPACE_COMPL]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ⇒
          m_space m DIFF s ∈ measurable_sets m
   
   [MEASURE_SPACE_COUNTABLY_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ countably_subadditive m
   
   [MEASURE_SPACE_DIFF]  Theorem
      
      ⊢ ∀m s t.
          measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
          s DIFF t ∈ measurable_sets m
   
   [MEASURE_SPACE_EMPTY_MEASURABLE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ ∅ ∈ measurable_sets m
   
   [MEASURE_SPACE_FINITE_DIFF]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_SPACE_FINITE_DIFF_SUBSET]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_SPACE_FINITE_MEASURE]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ∧
          measure m (m_space m) ≠ +∞ ⇒
          measure m s ≠ +∞
   
   [MEASURE_SPACE_FINITE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ finite_subadditive m
   
   [MEASURE_SPACE_INCREASING]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ increasing m
   
   [MEASURE_SPACE_INTER]  Theorem
      
      ⊢ ∀m s t.
          measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
          s ∩ t ∈ measurable_sets m
   
   [MEASURE_SPACE_IN_MSPACE]  Theorem
      
      ⊢ ∀m A.
          measure_space m ∧ A ∈ measurable_sets m ⇒
          ∀x. x ∈ A ⇒ x ∈ m_space m
   
   [MEASURE_SPACE_MSPACE_MEASURABLE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ m_space m ∈ measurable_sets m
   
   [MEASURE_SPACE_POSITIVE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ positive m
   
   [MEASURE_SPACE_REDUCE]  Theorem
      
      ⊢ ∀m. (m_space m,measurable_sets m,measure m) = m
   
   [MEASURE_SPACE_RESTRICTED]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ⇒
          measure_space (s,IMAGE (λt. s ∩ t) (measurable_sets m),measure m)
   
   [MEASURE_SPACE_RESTRICTED_MEASURE]  Theorem
      
      ⊢ ∀m s.
          measure_space m ∧ s ∈ measurable_sets m ⇒
          measure_space
            (m_space m,measurable_sets m,(λa. measure m (s ∩ a)))
   
   [MEASURE_SPACE_RESTRICTION]  Theorem
      
      ⊢ ∀sp sts m sub.
          measure_space (sp,sts,m) ∧ sub ⊆ sts ∧ sigma_algebra (sp,sub) ⇒
          measure_space (sp,sub,m)
   
   [MEASURE_SPACE_SPACE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ m_space m ∈ measurable_sets m
   
   [MEASURE_SPACE_STRONG_ADDITIVE]  Theorem
      
      ⊢ ∀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
   
   [MEASURE_SPACE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ subadditive m
   
   [MEASURE_SPACE_SUBSET]  Theorem
      
      ⊢ ∀s s' m.
          s' ⊆ s ∧ measure_space (s,POW s,m) ⇒ measure_space (s',POW s',m)
   
   [MEASURE_SPACE_SUBSET_MSPACE]  Theorem
      
      ⊢ ∀A m. measure_space m ∧ A ∈ measurable_sets m ⇒ A ⊆ m_space m
   
   [MEASURE_SPACE_UNION]  Theorem
      
      ⊢ ∀m s t.
          measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
          s ∪ t ∈ measurable_sets m
   
   [MONOTONE_CONVERGENCE]  Theorem
      
      ⊢ ∀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
   
   [MONOTONE_CONVERGENCE2]  Theorem
      
      ⊢ ∀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)))
   
   [MONOTONE_CONVERGENCE_BIGINTER]  Theorem
      
      ⊢ ∀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
   
   [MONOTONE_CONVERGENCE_BIGINTER2]  Theorem
      
      ⊢ ∀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)))
   
   [NULL_SET_EMPTY]  Theorem
      
      ⊢ ∀m. measure_space m ⇒ null_set m ∅
   
   [NULL_SET_INTER]  Theorem
      
      ⊢ ∀m N1 N2.
          measure_space m ∧ N1 ∈ null_set m ∧ N2 ∈ null_set m ⇒
          N1 ∩ N2 ∈ null_set m
   
   [NULL_SET_THM]  Theorem
      
      ⊢ ∀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
   
   [NULL_SET_UNION]  Theorem
      
      ⊢ ∀m N1 N2.
          measure_space m ∧ N1 ∈ null_set m ∧ N2 ∈ null_set m ⇒
          N1 ∪ N2 ∈ null_set m
   
   [OUTER_MEASURE_CONSTRUCTION]  Theorem
      
      ⊢ ∀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
   
   [OUTER_MEASURE_SPACE_FINITE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. outer_measure_space m ⇒ finite_subadditive m
   
   [OUTER_MEASURE_SPACE_POSITIVE]  Theorem
      
      ⊢ ∀m. outer_measure_space m ⇒ positive m
   
   [OUTER_MEASURE_SPACE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. outer_measure_space m ⇒ subadditive m
   
   [RING_ADDITIVE_EVERYTHING]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
            finite_additive m ∧ increasing m ∧ subadditive m ∧
            finite_subadditive m
   
   [RING_ADDITIVE_FINITE_ADDITIVE]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
            finite_additive m
   
   [RING_ADDITIVE_INCREASING]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
            increasing m
   
   [RING_ADDITIVE_STRONG_ADDITIVE]  Theorem
      
      ⊢ ∀m s t.
          ring (m_space m,measurable_sets 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
   
   [RING_ADDITIVE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ positive m ∧ additive m ⇒
            subadditive m
   
   [RING_PREMEASURE_ADDITIVE]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒ additive m
   
   [RING_PREMEASURE_COUNTABLE_INCREASING]  Theorem
      
      ⊢ ∀m s f.
          ring (m_space m,measurable_sets 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
   
   [RING_PREMEASURE_COUNTABLY_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒
            countably_subadditive m
   
   [RING_PREMEASURE_DIFF_SUBSET]  Theorem
      
      ⊢ ∀m s t.
          ring (m_space m,measurable_sets 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
   
   [RING_PREMEASURE_FINITE_ADDITIVE]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒
            finite_additive m
   
   [RING_PREMEASURE_FINITE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒
            finite_subadditive m
   
   [RING_PREMEASURE_INCREASING]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒
            increasing m
   
   [RING_PREMEASURE_STRONG_ADDITIVE]  Theorem
      
      ⊢ ∀m s t.
          ring (m_space m,measurable_sets 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
   
   [RING_PREMEASURE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ premeasure m ⇒
            subadditive m
   
   [RING_SUBADDITIVE_FINITE_SUBADDITIVE]  Theorem
      
      ⊢ ∀m. ring (m_space m,measurable_sets m) ∧ positive m ∧ subadditive m ⇒
            finite_subadditive m
   
   [SEMIRING_FINITE_ADDITIVE_EXTENSION]  Theorem
      
      ⊢ ∀m0.
          semiring (m_space m0,measurable_sets m0) ∧ positive m0 ∧
          finite_additive m0 ⇒
          ∃m. (m_space m,measurable_sets m) =
              smallest_ring (m_space m0) (measurable_sets m0) ∧
              (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
              positive m ∧ additive m
   
   [SEMIRING_PREMEASURE_ADDITIVE]  Theorem
      
      ⊢ ∀m. semiring (m_space m,measurable_sets m) ∧ premeasure m ⇒
            additive m
   
   [SEMIRING_PREMEASURE_EXTENSION]  Theorem
      
      ⊢ ∀m0.
          semiring (m_space m0,measurable_sets m0) ∧ premeasure m0 ⇒
          ∃m. (m_space m,measurable_sets m) =
              smallest_ring (m_space m0) (measurable_sets m0) ∧
              (∀s. s ∈ measurable_sets m0 ⇒ measure m s = measure m0 s) ∧
              premeasure m
   
   [SEMIRING_PREMEASURE_FINITE_ADDITIVE]  Theorem
      
      ⊢ ∀m. semiring (m_space m,measurable_sets m) ∧ premeasure m ⇒
            finite_additive m
   
   [SEMIRING_PREMEASURE_INCREASING]  Theorem
      
      ⊢ ∀m. semiring (m_space m,measurable_sets m) ∧ premeasure m ⇒
            increasing m
   
   [SIGMA_FINITE_ALT]  Theorem
      
      ⊢ ∀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) < +∞)
   
   [SIGMA_FINITE_ALT2]  Theorem
      
      ⊢ ∀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 ≠ +∞)
   
   [SIGMA_SUBSET_MEASURABLE_SETS]  Theorem
      
      ⊢ ∀a m.
          measure_space m ∧ a ⊆ measurable_sets m ⇒
          subsets (sigma (m_space m) a) ⊆ measurable_sets m
   
   [STRONG_MEASURE_SPACE_SUBSET]  Theorem
      
      ⊢ ∀s s'.
          s' ⊆ m_space s ∧ measure_space s ∧ POW s' ⊆ measurable_sets s ⇒
          measure_space (s',POW s',measure s)
   
   [SUBADDITIVE]  Theorem
      
      ⊢ ∀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
   
   [UNIQUENESS_OF_MEASURE]  Theorem
      
      ⊢ ∀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
   
   [UNIQUENESS_OF_MEASURE_FINITE]  Theorem
      
      ⊢ ∀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
   
   [countably_additive_alt_eq]  Theorem
      
      ⊢ ∀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)
   
   [finite_additivity_sufficient_for_finite_spaces]  Theorem
      
      ⊢ ∀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)
   
   [finite_additivity_sufficient_for_finite_spaces2]  Theorem
      
      ⊢ ∀m. sigma_algebra (m_space m,measurable_sets m) ∧
            FINITE (m_space m) ∧ positive m ∧ additive m ⇒
            measure_space m
   
   [measure_space_eq]  Theorem
      
      ⊢ ∀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
   
   [measure_space_trivial]  Theorem
      
      ⊢ ∀a. sigma_algebra a ⇒
            sigma_finite_measure_space (space a,subsets a,(λs. 0))
   
   [measure_split]  Theorem
      
      ⊢ ∀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
   
   [null_sets]  Theorem
      
      ⊢ null_set M = {N | N ∈ measurable_sets M ∧ measure M N = 0}
   
   [positive_not_infty]  Theorem
      
      ⊢ ∀m. positive m ⇒ ∀s. s ∈ measurable_sets m ⇒ measure m s ≠ −∞
   
   [sets_eq_imp_space_eq]  Theorem
      
      ⊢ ∀M M'.
          measure_space M ∧ measure_space M' ∧
          measurable_sets M = measurable_sets M' ⇒
          m_space M = m_space M'
   
   [sigma_finite]  Theorem
      
      ⊢ ∀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) ≠ +∞
   
   [sigma_finite_disjoint]  Theorem
      
      ⊢ ∀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
   
   
*)
end

HOL 4, Kananaskis-14