Structure measureTheory


Source File Identifier index Theory binding index

signature measureTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val Borel_def : thm
    val additive_def : thm
    val algebra_def : thm
    val closed_cdi_def : thm
    val countably_additive_def : thm
    val countably_subadditive_def : thm
    val fn_abs_def : thm
    val fn_minus_def : thm
    val fn_plus_def : thm
    val increasing_def : thm
    val indicator_fn_def : thm
    val inf_measure_def : thm
    val lambda_system_def : thm
    val m_space_def : thm
    val measurable_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_space_def : thm
    val pos_simple_fn_def : thm
    val positive_def : thm
    val sigma_algebra_def : thm
    val sigma_def : thm
    val smallest_closed_cdi_def : thm
    val space_def : thm
    val subadditive_def : thm
    val subset_class_def : thm
    val subsets_def : thm
  
  (*  Theorems  *)
    val ADDITIVE : thm
    val ADDITIVE_INCREASING : thm
    val ADDITIVE_SUM : thm
    val ALGEBRA_ALT_INTER : thm
    val ALGEBRA_COMPL : thm
    val ALGEBRA_DIFF : thm
    val ALGEBRA_EMPTY : thm
    val ALGEBRA_FINITE_UNION : thm
    val ALGEBRA_INTER : thm
    val ALGEBRA_INTER_SPACE : thm
    val ALGEBRA_SPACE : thm
    val ALGEBRA_SUBSET_LAMBDA_SYSTEM : thm
    val ALGEBRA_UNION : thm
    val BIGUNION_IMAGE_Q : thm
    val BOREL_MEASURABLE_SETS : thm
    val BOREL_MEASURABLE_SETS1 : thm
    val BOREL_MEASURABLE_SETS10 : thm
    val BOREL_MEASURABLE_SETS2 : thm
    val BOREL_MEASURABLE_SETS3 : thm
    val BOREL_MEASURABLE_SETS4 : thm
    val BOREL_MEASURABLE_SETS5 : thm
    val BOREL_MEASURABLE_SETS6 : thm
    val BOREL_MEASURABLE_SETS7 : thm
    val BOREL_MEASURABLE_SETS8 : thm
    val BOREL_MEASURABLE_SETS9 : thm
    val CARATHEODORY : thm
    val CARATHEODORY_LEMMA : thm
    val CLOSED_CDI_COMPL : thm
    val CLOSED_CDI_DISJOINT : thm
    val CLOSED_CDI_DUNION : thm
    val CLOSED_CDI_INCREASING : thm
    val COUNTABLY_ADDITIVE : thm
    val COUNTABLY_ADDITIVE_ADDITIVE : thm
    val COUNTABLY_SUBADDITIVE : thm
    val COUNTABLY_SUBADDITIVE_SUBADDITIVE : thm
    val FN_MINUS_ADD_LE : thm
    val FN_MINUS_CMUL : thm
    val FN_MINUS_POS : thm
    val FN_MINUS_POS_ZERO : thm
    val FN_PLUS_ADD_LE : thm
    val FN_PLUS_CMUL : thm
    val FN_PLUS_POS : thm
    val FN_PLUS_POS_ID : thm
    val IMAGE_SING : thm
    val INCREASING : thm
    val INCREASING_ADDITIVE_SUMMABLE : thm
    val INDICATOR_FN_MUL_INTER : thm
    val INF_MEASURE_AGREES : thm
    val INF_MEASURE_CLOSE : thm
    val INF_MEASURE_COUNTABLY_SUBADDITIVE : thm
    val INF_MEASURE_EMPTY : thm
    val INF_MEASURE_INCREASING : thm
    val INF_MEASURE_LE : thm
    val INF_MEASURE_NONEMPTY : thm
    val INF_MEASURE_OUTER : thm
    val INF_MEASURE_POS : thm
    val INF_MEASURE_POS0 : thm
    val INF_MEASURE_POSITIVE : thm
    val IN_MEASURABLE : thm
    val IN_MEASURABLE_BOREL : thm
    val IN_MEASURABLE_BOREL_ABS : thm
    val IN_MEASURABLE_BOREL_ADD : thm
    val IN_MEASURABLE_BOREL_ALL : thm
    val IN_MEASURABLE_BOREL_ALL_MEASURE : thm
    val IN_MEASURABLE_BOREL_ALT1 : thm
    val IN_MEASURABLE_BOREL_ALT2 : thm
    val IN_MEASURABLE_BOREL_ALT3 : thm
    val IN_MEASURABLE_BOREL_ALT4 : thm
    val IN_MEASURABLE_BOREL_ALT5 : thm
    val IN_MEASURABLE_BOREL_ALT6 : thm
    val IN_MEASURABLE_BOREL_ALT7 : thm
    val IN_MEASURABLE_BOREL_ALT8 : thm
    val IN_MEASURABLE_BOREL_ALT9 : thm
    val IN_MEASURABLE_BOREL_CMUL : thm
    val IN_MEASURABLE_BOREL_CMUL_INDICATOR : thm
    val IN_MEASURABLE_BOREL_CONST : thm
    val IN_MEASURABLE_BOREL_FN_MINUS : thm
    val IN_MEASURABLE_BOREL_FN_PLUS : thm
    val IN_MEASURABLE_BOREL_INDICATOR : thm
    val IN_MEASURABLE_BOREL_LE : thm
    val IN_MEASURABLE_BOREL_LT : thm
    val IN_MEASURABLE_BOREL_MAX : thm
    val IN_MEASURABLE_BOREL_MONO_SUP : thm
    val IN_MEASURABLE_BOREL_MUL : thm
    val IN_MEASURABLE_BOREL_MUL_INDICATOR : thm
    val IN_MEASURABLE_BOREL_MUL_INDICATOR_EQ : thm
    val IN_MEASURABLE_BOREL_NEGINF : thm
    val IN_MEASURABLE_BOREL_PLUS_MINUS : thm
    val IN_MEASURABLE_BOREL_POS_SIMPLE_FN : thm
    val IN_MEASURABLE_BOREL_POW : thm
    val IN_MEASURABLE_BOREL_SQR : thm
    val IN_MEASURABLE_BOREL_SUB : thm
    val IN_MEASURABLE_BOREL_SUM : thm
    val IN_MEASURE_PRESERVING : thm
    val IN_SIGMA : thm
    val LAMBDA_SYSTEM_ADDITIVE : thm
    val LAMBDA_SYSTEM_ALGEBRA : thm
    val LAMBDA_SYSTEM_CARATHEODORY : thm
    val LAMBDA_SYSTEM_COMPL : thm
    val LAMBDA_SYSTEM_EMPTY : thm
    val LAMBDA_SYSTEM_INCREASING : thm
    val LAMBDA_SYSTEM_INTER : thm
    val LAMBDA_SYSTEM_POSITIVE : thm
    val LAMBDA_SYSTEM_STRONG_ADDITIVE : thm
    val LAMBDA_SYSTEM_STRONG_SUM : thm
    val MEASUBABLE_BIGUNION_LEMMA : thm
    val MEASURABLE_BIGUNION_PROPERTY : thm
    val MEASURABLE_BOREL : thm
    val MEASURABLE_COMP : thm
    val MEASURABLE_COMP_STRONG : thm
    val MEASURABLE_COMP_STRONGER : thm
    val MEASURABLE_DIFF_PROPERTY : thm
    val MEASURABLE_I : thm
    val MEASURABLE_LIFT : thm
    val MEASURABLE_POW_TO_POW : thm
    val MEASURABLE_POW_TO_POW_IMAGE : thm
    val MEASURABLE_PROD_SIGMA : thm
    val MEASURABLE_RANGE_REDUCE : thm
    val MEASURABLE_SETS_SUBSET_SPACE : thm
    val MEASURABLE_SIGMA : thm
    val MEASURABLE_SIGMA_PREIMAGES : thm
    val MEASURABLE_SUBSET : thm
    val MEASURABLE_UP_LIFT : thm
    val MEASURABLE_UP_SIGMA : thm
    val MEASURABLE_UP_SUBSET : 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_DOWN : thm
    val MEASURE_EMPTY : 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_REAL_SUM_IMAGE : thm
    val MEASURE_SPACE_ADDITIVE : thm
    val MEASURE_SPACE_BIGINTER : thm
    val MEASURE_SPACE_BIGUNION : thm
    val MEASURE_SPACE_CMUL : thm
    val MEASURE_SPACE_DIFF : thm
    val MEASURE_SPACE_EMPTY_MEASURABLE : 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_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 OUTER_MEASURE_SPACE_POSITIVE : thm
    val POW_ALGEBRA : thm
    val POW_SIGMA_ALGEBRA : thm
    val SIGMA_ALGEBRA : thm
    val SIGMA_ALGEBRA_ALGEBRA : thm
    val SIGMA_ALGEBRA_ALT : thm
    val SIGMA_ALGEBRA_ALT_DISJOINT : thm
    val SIGMA_ALGEBRA_ALT_MONO : thm
    val SIGMA_ALGEBRA_BOREL : thm
    val SIGMA_ALGEBRA_COUNTABLE_UNION : thm
    val SIGMA_ALGEBRA_ENUM : thm
    val SIGMA_ALGEBRA_FN : thm
    val SIGMA_ALGEBRA_FN_BIGINTER : thm
    val SIGMA_ALGEBRA_FN_DISJOINT : thm
    val SIGMA_ALGEBRA_SIGMA : thm
    val SIGMA_POW : thm
    val SIGMA_PROPERTY : thm
    val SIGMA_PROPERTY_ALT : thm
    val SIGMA_PROPERTY_DISJOINT : thm
    val SIGMA_PROPERTY_DISJOINT_LEMMA : thm
    val SIGMA_PROPERTY_DISJOINT_LEMMA1 : thm
    val SIGMA_PROPERTY_DISJOINT_LEMMA2 : thm
    val SIGMA_PROPERTY_DISJOINT_WEAK : thm
    val SIGMA_REDUCE : thm
    val SIGMA_SUBSET : thm
    val SIGMA_SUBSET_MEASURABLE_SETS : thm
    val SIGMA_SUBSET_SUBSETS : thm
    val SMALLEST_CLOSED_CDI : thm
    val SPACE : thm
    val SPACE_BOREL : thm
    val SPACE_SIGMA : thm
    val SPACE_SMALLEST_CLOSED_CDI : thm
    val STRONG_MEASURE_SPACE_SUBSET : thm
    val SUBADDITIVE : thm
    val SUBSET_BIGINTER : thm
    val UNIV_SIGMA_ALGEBRA : thm
    val finite_additivity_sufficient_for_finite_spaces : thm
    val finite_additivity_sufficient_for_finite_spaces2 : thm
    val indicator_fn_split : thm
    val indicator_fn_suminf : thm
    val measure_split : thm
  
  val measure_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [extreal] Parent theory of "measure"
   
   [Borel_def]  Definition
      
      ⊒ Borel = sigma π•Œ(:extreal) (IMAGE (Ξ»a. {x | x < a}) π•Œ(:extreal))
   
   [additive_def]  Definition
      
      ⊒ βˆ€m.
            additive m ⇔
            βˆ€s t.
                s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
                DISJOINT s t β‡’
                (measure m (s βˆͺ t) = measure m s + measure m t)
   
   [algebra_def]  Definition
      
      ⊒ βˆ€a.
            algebra a ⇔
            subset_class (space a) (subsets a) ∧ βˆ… ∈ subsets a ∧
            (βˆ€s. s ∈ subsets a β‡’ space a DIFF s ∈ subsets a) ∧
            βˆ€s t. s ∈ subsets a ∧ t ∈ subsets a β‡’ s βˆͺ t ∈ subsets a
   
   [closed_cdi_def]  Definition
      
      ⊒ βˆ€p.
            closed_cdi p ⇔
            subset_class (space p) (subsets p) ∧
            (βˆ€s. s ∈ subsets p β‡’ space p DIFF s ∈ subsets p) ∧
            (βˆ€f.
                 f ∈ (π•Œ(:num) -> subsets p) ∧ (f 0 = βˆ…) ∧
                 (βˆ€n. f n βŠ† f (SUC n)) β‡’
                 BIGUNION (IMAGE f π•Œ(:num)) ∈ subsets p) ∧
            βˆ€f.
                f ∈ (π•Œ(:num) -> subsets p) ∧
                (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) β‡’
                BIGUNION (IMAGE f π•Œ(:num)) ∈ subsets p
   
   [countably_additive_def]  Definition
      
      ⊒ βˆ€m.
            countably_additive m ⇔
            βˆ€f.
                f ∈ (π•Œ(:num) -> measurable_sets m) ∧
                (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) ∧
                BIGUNION (IMAGE f π•Œ(:num)) ∈ measurable_sets m β‡’
                measure m ∘ f sums measure m (BIGUNION (IMAGE f π•Œ(:num)))
   
   [countably_subadditive_def]  Definition
      
      ⊒ βˆ€m.
            countably_subadditive m ⇔
            βˆ€f.
                f ∈ (π•Œ(:num) -> measurable_sets m) ∧
                BIGUNION (IMAGE f π•Œ(:num)) ∈ measurable_sets m ∧
                summable (measure m ∘ f) β‡’
                measure m (BIGUNION (IMAGE f π•Œ(:num))) ≀
                suminf (measure m ∘ f)
   
   [fn_abs_def]  Definition
      
      ⊒ βˆ€f. fn_abs f = (Ξ»x. abs (f x))
   
   [fn_minus_def]  Definition
      
      ⊒ βˆ€f. fn_minus f = (Ξ»x. if f x < 0 then -f x else 0)
   
   [fn_plus_def]  Definition
      
      ⊒ βˆ€f. fn_plus f = (Ξ»x. if 0 < f x then f x else 0)
   
   [increasing_def]  Definition
      
      ⊒ βˆ€m.
            increasing m ⇔
            βˆ€s t.
                s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧ s βŠ† t β‡’
                measure m s ≀ measure m t
   
   [indicator_fn_def]  Definition
      
      ⊒ βˆ€s. indicator_fn s = (Ξ»x. if x ∈ s then 1 else 0)
   
   [inf_measure_def]  Definition
      
      ⊒ βˆ€m s.
            inf_measure m s =
            inf
              {r |
               (βˆƒf.
                    f ∈ (π•Œ(:num) -> measurable_sets m) ∧
                    (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) ∧
                    s βŠ† BIGUNION (IMAGE f π•Œ(:num)) ∧ measure m ∘ f sums r)}
   
   [lambda_system_def]  Definition
      
      ⊒ βˆ€gen lam.
            lambda_system gen lam =
            {l |
             l ∈ subsets gen ∧
             βˆ€s.
                 s ∈ subsets gen β‡’
                 (lam (l ∩ s) + lam ((space gen DIFF l) ∩ s) = lam s)}
   
   [m_space_def]  Definition
      
      ⊒ βˆ€sp sts mu. m_space (sp,sts,mu) = sp
   
   [measurable_def]  Definition
      
      ⊒ βˆ€a b.
            measurable a b =
            {f |
             sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
             βˆ€s. s ∈ subsets b β‡’ PREIMAGE f s ∩ space a ∈ subsets a}
   
   [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) ∧ measure_space m1 ∧
             measure_space 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_space_def]  Definition
      
      ⊒ βˆ€m.
            outer_measure_space m ⇔
            positive m ∧ increasing m ∧ countably_subadditive m
   
   [pos_simple_fn_def]  Definition
      
      ⊒ βˆ€m f s a x.
            pos_simple_fn m f s a x ⇔
            (βˆ€t. 0 ≀ f t) ∧
            (βˆ€t.
                 t ∈ m_space m β‡’
                 (f t = SIGMA (λi. Normal (x i) * indicator_fn (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)
   
   [positive_def]  Definition
      
      ⊒ βˆ€m.
            positive m ⇔
            (measure m βˆ… = 0) ∧ βˆ€s. s ∈ measurable_sets m β‡’ 0 ≀ measure m s
   
   [sigma_algebra_def]  Definition
      
      ⊒ βˆ€a.
            sigma_algebra a ⇔
            algebra a ∧
            βˆ€c. countable c ∧ c βŠ† subsets a β‡’ BIGUNION c ∈ subsets a
   
   [sigma_def]  Definition
      
      ⊒ βˆ€sp st.
            sigma sp st = (sp,BIGINTER {s | st βŠ† s ∧ sigma_algebra (sp,s)})
   
   [smallest_closed_cdi_def]  Definition
      
      ⊒ βˆ€a.
            smallest_closed_cdi a =
            (space a,BIGINTER {b | subsets a βŠ† b ∧ closed_cdi (space a,b)})
   
   [space_def]  Definition
      
      ⊒ βˆ€x y. space (x,y) = x
   
   [subadditive_def]  Definition
      
      ⊒ βˆ€m.
            subadditive m ⇔
            βˆ€s t.
                s ∈ measurable_sets m ∧ t ∈ measurable_sets m β‡’
                measure m (s βˆͺ t) ≀ measure m s + measure m t
   
   [subset_class_def]  Definition
      
      ⊒ βˆ€sp sts. subset_class sp sts ⇔ βˆ€x. x ∈ sts β‡’ x βŠ† sp
   
   [subsets_def]  Definition
      
      ⊒ βˆ€x y. subsets (x,y) = y
   
   [ADDITIVE]  Theorem
      
      ⊒ βˆ€m s t u.
            additive m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ∧
            DISJOINT s t ∧ (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)) β‡’
            (sum (0,n) (measure m ∘ f) =
             measure m (BIGUNION (IMAGE f (count n))))
   
   [ALGEBRA_ALT_INTER]  Theorem
      
      ⊒ βˆ€a.
            algebra a ⇔
            subset_class (space a) (subsets a) ∧ βˆ… ∈ subsets a ∧
            (βˆ€s. s ∈ subsets a β‡’ space a DIFF s ∈ subsets a) ∧
            βˆ€s t. s ∈ subsets a ∧ t ∈ subsets a β‡’ s ∩ t ∈ subsets a
   
   [ALGEBRA_COMPL]  Theorem
      
      ⊒ βˆ€a s. algebra a ∧ s ∈ subsets a β‡’ space a DIFF s ∈ subsets a
   
   [ALGEBRA_DIFF]  Theorem
      
      ⊒ βˆ€a s t.
            algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a β‡’
            s DIFF t ∈ subsets a
   
   [ALGEBRA_EMPTY]  Theorem
      
      ⊒ βˆ€a. algebra a β‡’ βˆ… ∈ subsets a
   
   [ALGEBRA_FINITE_UNION]  Theorem
      
      ⊒ βˆ€a c. algebra a ∧ FINITE c ∧ c βŠ† subsets a β‡’ BIGUNION c ∈ subsets a
   
   [ALGEBRA_INTER]  Theorem
      
      ⊒ βˆ€a s t.
            algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a β‡’ s ∩ t ∈ subsets a
   
   [ALGEBRA_INTER_SPACE]  Theorem
      
      ⊒ βˆ€a s.
            algebra a ∧ s ∈ subsets a β‡’
            (space a ∩ s = s) ∧ (s ∩ space a = s)
   
   [ALGEBRA_SPACE]  Theorem
      
      ⊒ βˆ€a. algebra a β‡’ space a ∈ subsets a
   
   [ALGEBRA_SUBSET_LAMBDA_SYSTEM]  Theorem
      
      ⊒ βˆ€m.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            increasing m ∧ additive m β‡’
            measurable_sets m βŠ†
            lambda_system (m_space m,POW (m_space m)) (inf_measure m)
   
   [ALGEBRA_UNION]  Theorem
      
      ⊒ βˆ€a s t.
            algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a β‡’ s βˆͺ t ∈ subsets a
   
   [BIGUNION_IMAGE_Q]  Theorem
      
      ⊒ βˆ€a f.
            sigma_algebra a ∧ f ∈ (Q_set -> subsets a) β‡’
            BIGUNION (IMAGE f Q_set) ∈ subsets a
   
   [BOREL_MEASURABLE_SETS]  Theorem
      
      ⊒ (βˆ€c. {x | x < c} ∈ subsets Borel) ∧
        (βˆ€c. {x | c ≀ x} ∈ subsets Borel) ∧
        (βˆ€c. {x | c < x} ∈ subsets Borel) ∧
        (βˆ€c. {x | x ≀ c} ∈ subsets Borel) ∧
        (βˆ€c d. {x | c < x ∧ x < d} ∈ subsets Borel) ∧
        (βˆ€c d. {x | c ≀ x ∧ x < d} ∈ subsets Borel) ∧
        (βˆ€c d. {x | c < x ∧ x ≀ d} ∈ subsets Borel) ∧
        (βˆ€c d. {x | c ≀ x ∧ x ≀ d} ∈ subsets Borel) ∧
        (βˆ€c. {c} ∈ subsets Borel) ∧ βˆ€c. {x | x β‰  c} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS1]  Theorem
      
      ⊒ βˆ€c. {x | x < c} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS10]  Theorem
      
      ⊒ βˆ€c. {x | x β‰  c} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS2]  Theorem
      
      ⊒ βˆ€c. {x | c ≀ x} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS3]  Theorem
      
      ⊒ βˆ€c. {x | x ≀ c} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS4]  Theorem
      
      ⊒ βˆ€c. {x | c < x} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS5]  Theorem
      
      ⊒ βˆ€c d. {x | c ≀ x ∧ x < d} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS6]  Theorem
      
      ⊒ βˆ€c d. {x | c < x ∧ x ≀ d} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS7]  Theorem
      
      ⊒ βˆ€c d. {x | c ≀ x ∧ x ≀ d} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS8]  Theorem
      
      ⊒ βˆ€c d. {x | c < x ∧ x < d} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS9]  Theorem
      
      ⊒ βˆ€c. {c} ∈ subsets Borel
   
   [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_LEMMA]  Theorem
      
      ⊒ βˆ€gsig lam.
            sigma_algebra gsig ∧
            outer_measure_space (space gsig,subsets gsig,lam) β‡’
            measure_space (space gsig,lambda_system gsig lam,lam)
   
   [CLOSED_CDI_COMPL]  Theorem
      
      ⊒ βˆ€p s. closed_cdi p ∧ s ∈ subsets p β‡’ space p DIFF s ∈ subsets p
   
   [CLOSED_CDI_DISJOINT]  Theorem
      
      ⊒ βˆ€p f.
            closed_cdi p ∧ f ∈ (π•Œ(:num) -> subsets p) ∧
            (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) β‡’
            BIGUNION (IMAGE f π•Œ(:num)) ∈ subsets p
   
   [CLOSED_CDI_DUNION]  Theorem
      
      ⊒ βˆ€p s t.
            βˆ… ∈ subsets p ∧ closed_cdi p ∧ s ∈ subsets p ∧ t ∈ subsets p ∧
            DISJOINT s t β‡’
            s βˆͺ t ∈ subsets p
   
   [CLOSED_CDI_INCREASING]  Theorem
      
      ⊒ βˆ€p f.
            closed_cdi p ∧ f ∈ (π•Œ(:num) -> subsets p) ∧ (f 0 = βˆ…) ∧
            (βˆ€n. f n βŠ† f (SUC n)) β‡’
            BIGUNION (IMAGE f π•Œ(:num)) ∈ subsets p
   
   [COUNTABLY_ADDITIVE]  Theorem
      
      ⊒ βˆ€m s f.
            countably_additive m ∧ f ∈ (π•Œ(:num) -> measurable_sets m) ∧
            (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) ∧
            (s = BIGUNION (IMAGE f π•Œ(:num))) ∧ s ∈ measurable_sets m β‡’
            measure m ∘ f sums measure m s
   
   [COUNTABLY_ADDITIVE_ADDITIVE]  Theorem
      
      ⊒ βˆ€m.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            countably_additive m β‡’
            additive m
   
   [COUNTABLY_SUBADDITIVE]  Theorem
      
      ⊒ βˆ€m f s.
            countably_subadditive m ∧ f ∈ (π•Œ(:num) -> measurable_sets m) ∧
            summable (measure m ∘ f) ∧ (s = BIGUNION (IMAGE f π•Œ(:num))) ∧
            s ∈ measurable_sets m β‡’
            measure m s ≀ suminf (measure m ∘ f)
   
   [COUNTABLY_SUBADDITIVE_SUBADDITIVE]  Theorem
      
      ⊒ βˆ€m.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            countably_subadditive m β‡’
            subadditive m
   
   [FN_MINUS_ADD_LE]  Theorem
      
      ⊒ βˆ€f g x. fn_minus (Ξ»x. f x + g x) x ≀ fn_minus f x + fn_minus g x
   
   [FN_MINUS_CMUL]  Theorem
      
      ⊒ βˆ€f c.
            (0 ≀ c β‡’
             (fn_minus (λx. Normal c * f x) = (λx. Normal c * fn_minus f x))) ∧
            (c ≀ 0 β‡’
             (fn_minus (Ξ»x. Normal c * f x) = (Ξ»x. -Normal c * fn_plus f x)))
   
   [FN_MINUS_POS]  Theorem
      
      ⊒ βˆ€g x. 0 ≀ fn_minus g x
   
   [FN_MINUS_POS_ZERO]  Theorem
      
      ⊒ (βˆ€x. 0 ≀ g x) β‡’ (fn_minus g = (Ξ»x. 0))
   
   [FN_PLUS_ADD_LE]  Theorem
      
      ⊒ βˆ€f g x. fn_plus (Ξ»x. f x + g x) x ≀ fn_plus f x + fn_plus g x
   
   [FN_PLUS_CMUL]  Theorem
      
      ⊒ βˆ€f c.
            (0 ≀ c β‡’
             (fn_plus (λx. Normal c * f x) = (λx. Normal c * fn_plus f x))) ∧
            (c ≀ 0 β‡’
             (fn_plus (Ξ»x. Normal c * f x) = (Ξ»x. -Normal c * fn_minus f x)))
   
   [FN_PLUS_POS]  Theorem
      
      ⊒ βˆ€g x. 0 ≀ fn_plus g x
   
   [FN_PLUS_POS_ID]  Theorem
      
      ⊒ (βˆ€x. 0 ≀ g x) β‡’ (fn_plus g = g)
   
   [IMAGE_SING]  Theorem
      
      ⊒ βˆ€f x. IMAGE f {x} = {f x}
   
   [INCREASING]  Theorem
      
      ⊒ βˆ€m s t.
            increasing m ∧ s βŠ† t ∧ s ∈ measurable_sets m ∧
            t ∈ measurable_sets m β‡’
            measure m s ≀ measure m t
   
   [INCREASING_ADDITIVE_SUMMABLE]  Theorem
      
      ⊒ βˆ€m f.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            increasing m ∧ additive m ∧
            f ∈ (π•Œ(:num) -> measurable_sets m) ∧
            (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) β‡’
            summable (measure m ∘ f)
   
   [INDICATOR_FN_MUL_INTER]  Theorem
      
      ⊒ βˆ€A B.
            (Ξ»t. indicator_fn A t * indicator_fn B t) =
            (λt. indicator_fn (A ∩ B) t)
   
   [INF_MEASURE_AGREES]  Theorem
      
      ⊒ βˆ€m s.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            countably_additive m ∧ s ∈ measurable_sets m β‡’
            (inf_measure m s = measure m s)
   
   [INF_MEASURE_CLOSE]  Theorem
      
      ⊒ βˆ€m s e.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧ 0 < e ∧
            s βŠ† m_space m β‡’
            βˆƒf l.
                f ∈ (π•Œ(:num) -> measurable_sets m) ∧
                s βŠ† BIGUNION (IMAGE f π•Œ(:num)) ∧
                (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) ∧
                measure m ∘ f sums l ∧ l ≀ inf_measure m s + e
   
   [INF_MEASURE_COUNTABLY_SUBADDITIVE]  Theorem
      
      ⊒ βˆ€m.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            increasing m β‡’
            countably_subadditive (m_space m,POW (m_space m),inf_measure m)
   
   [INF_MEASURE_EMPTY]  Theorem
      
      ⊒ βˆ€m.
            algebra (m_space m,measurable_sets m) ∧ positive m β‡’
            (inf_measure m βˆ… = 0)
   
   [INF_MEASURE_INCREASING]  Theorem
      
      ⊒ βˆ€m.
            algebra (m_space m,measurable_sets m) ∧ positive m β‡’
            increasing (m_space m,POW (m_space m),inf_measure m)
   
   [INF_MEASURE_LE]  Theorem
      
      ⊒ βˆ€m s x.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            increasing m ∧
            x ∈
            {r |
             βˆƒf.
                 f ∈ (π•Œ(:num) -> measurable_sets m) ∧
                 s βŠ† BIGUNION (IMAGE f π•Œ(:num)) ∧ measure m ∘ f sums r} β‡’
            inf_measure m s ≀ x
   
   [INF_MEASURE_NONEMPTY]  Theorem
      
      ⊒ βˆ€m g s.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            s ∈ measurable_sets m ∧ g βŠ† s β‡’
            measure m s ∈
            {r |
             βˆƒf.
                 f ∈ (π•Œ(:num) -> measurable_sets m) ∧
                 (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) ∧
                 g βŠ† BIGUNION (IMAGE f π•Œ(:num)) ∧ measure m ∘ f sums r}
   
   [INF_MEASURE_OUTER]  Theorem
      
      ⊒ βˆ€m.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            increasing m β‡’
            outer_measure_space (m_space m,POW (m_space m),inf_measure m)
   
   [INF_MEASURE_POS]  Theorem
      
      ⊒ βˆ€m g.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            g βŠ† m_space m β‡’
            0 ≀ inf_measure m g
   
   [INF_MEASURE_POS0]  Theorem
      
      ⊒ βˆ€m g x.
            algebra (m_space m,measurable_sets m) ∧ positive m ∧
            x ∈
            {r |
             βˆƒf.
                 f ∈ (π•Œ(:num) -> measurable_sets m) ∧
                 (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) ∧
                 g βŠ† BIGUNION (IMAGE f π•Œ(:num)) ∧ measure m ∘ f sums r} β‡’
            0 ≀ x
   
   [INF_MEASURE_POSITIVE]  Theorem
      
      ⊒ βˆ€m.
            algebra (m_space m,measurable_sets m) ∧ positive m β‡’
            positive (m_space m,POW (m_space m),inf_measure m)
   
   [IN_MEASURABLE]  Theorem
      
      ⊒ βˆ€a b f.
            f ∈ measurable a b ⇔
            sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
            βˆ€s. s ∈ subsets b β‡’ PREIMAGE f s ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel ⇔
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c. {x | f x < c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ABS]  Theorem
      
      ⊒ βˆ€a f g.
            sigma_algebra a ∧ f ∈ measurable a Borel ∧
            (βˆ€x. x ∈ space a β‡’ (g x = abs (f x))) β‡’
            g ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_ADD]  Theorem
      
      ⊒ βˆ€a f g h.
            sigma_algebra a ∧ f ∈ measurable a Borel ∧
            g ∈ measurable a Borel ∧ (βˆ€x. x ∈ space a β‡’ (h x = f x + g x)) β‡’
            h ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_ALL]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel β‡’
            (βˆ€c. {x | f x < c} ∩ space a ∈ subsets a) ∧
            (βˆ€c. {x | c ≀ f x} ∩ space a ∈ subsets a) ∧
            (βˆ€c. {x | f x ≀ c} ∩ space a ∈ subsets a) ∧
            (βˆ€c. {x | c < f x} ∩ space a ∈ subsets a) ∧
            (βˆ€c d. {x | c < f x ∧ f x < d} ∩ space a ∈ subsets a) ∧
            (βˆ€c d. {x | c ≀ f x ∧ f x < d} ∩ space a ∈ subsets a) ∧
            (βˆ€c d. {x | c < f x ∧ f x ≀ d} ∩ space a ∈ subsets a) ∧
            (βˆ€c d. {x | c ≀ f x ∧ f x ≀ d} ∩ space a ∈ subsets a) ∧
            (βˆ€c. {x | f x β‰  c} ∩ space a ∈ subsets a) ∧
            βˆ€c. {x | f x = c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALL_MEASURE]  Theorem
      
      ⊒ βˆ€f m.
            f ∈ measurable (m_space m,measurable_sets m) Borel β‡’
            (βˆ€c. {x | f x < c} ∩ m_space m ∈ measurable_sets m) ∧
            (βˆ€c. {x | c ≀ f x} ∩ m_space m ∈ measurable_sets m) ∧
            (βˆ€c. {x | f x ≀ c} ∩ m_space m ∈ measurable_sets m) ∧
            (βˆ€c. {x | c < f x} ∩ m_space m ∈ measurable_sets m) ∧
            (βˆ€c d. {x | c < f x ∧ f x < d} ∩ m_space m ∈ measurable_sets m) ∧
            (βˆ€c d. {x | c ≀ f x ∧ f x < d} ∩ m_space m ∈ measurable_sets m) ∧
            (βˆ€c d. {x | c < f x ∧ f x ≀ d} ∩ m_space m ∈ measurable_sets m) ∧
            (βˆ€c d. {x | c ≀ f x ∧ f x ≀ d} ∩ m_space m ∈ measurable_sets m) ∧
            (βˆ€c. {x | f x = c} ∩ m_space m ∈ measurable_sets m) ∧
            βˆ€c. {x | f x β‰  c} ∩ m_space m ∈ measurable_sets m
   
   [IN_MEASURABLE_BOREL_ALT1]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel ⇔
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c. {x | c ≀ f x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT2]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel ⇔
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c. {x | f x ≀ c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT3]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel ⇔
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c. {x | c < f x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT4]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel ⇔
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c d. {x | c ≀ f x ∧ f x < d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT5]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel ⇔
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c d. {x | c < f x ∧ f x ≀ d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT6]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel ⇔
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c d. {x | c ≀ f x ∧ f x ≀ d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT7]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel β‡’
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c d. {x | c < f x ∧ f x < d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT8]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel β‡’
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c. {x | f x = c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT9]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel β‡’
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c. {x | f x β‰  c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_CMUL]  Theorem
      
      ⊒ βˆ€a f g z.
            sigma_algebra a ∧ f ∈ measurable a Borel ∧
            (βˆ€x. x ∈ space a β‡’ (g x = Normal z * f x)) β‡’
            g ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_CMUL_INDICATOR]  Theorem
      
      ⊒ βˆ€a z s.
            sigma_algebra a ∧ s ∈ subsets a β‡’
            (λx. Normal z * indicator_fn s x) ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_CONST]  Theorem
      
      ⊒ βˆ€a k f.
            sigma_algebra a ∧ (βˆ€x. x ∈ space a β‡’ (f x = k)) β‡’
            f ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_FN_MINUS]  Theorem
      
      ⊒ βˆ€a f. f ∈ measurable a Borel β‡’ fn_minus f ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_FN_PLUS]  Theorem
      
      ⊒ βˆ€a f. f ∈ measurable a Borel β‡’ fn_plus f ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_INDICATOR]  Theorem
      
      ⊒ βˆ€a A f.
            sigma_algebra a ∧ A ∈ subsets a ∧
            (βˆ€x. x ∈ space a β‡’ (f x = indicator_fn A x)) β‡’
            f ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_LE]  Theorem
      
      ⊒ βˆ€f g a.
            f ∈ measurable a Borel ∧ g ∈ measurable a Borel β‡’
            {x | f x ≀ g x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_LT]  Theorem
      
      ⊒ βˆ€f g a.
            f ∈ measurable a Borel ∧ g ∈ measurable a Borel β‡’
            {x | f x < g x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_MAX]  Theorem
      
      ⊒ βˆ€a f g.
            sigma_algebra a ∧ f ∈ measurable a Borel ∧
            g ∈ measurable a Borel β‡’
            (λx. max (f x) (g x)) ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_MONO_SUP]  Theorem
      
      ⊒ βˆ€fn f a.
            sigma_algebra a ∧ (βˆ€n. fn n ∈ measurable a Borel) ∧
            (βˆ€n x. x ∈ space a β‡’ fn n x ≀ fn (SUC n) x) ∧
            (βˆ€x. x ∈ space a β‡’ (f x = sup (IMAGE (Ξ»n. fn n x) π•Œ(:num)))) β‡’
            f ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_MUL]  Theorem
      
      ⊒ βˆ€a f g h.
            sigma_algebra a ∧ f ∈ measurable a Borel ∧
            (βˆ€x.
                 x ∈ space a β‡’
                 f x β‰  NegInf ∧ f x β‰  PosInf ∧ g x β‰  NegInf ∧ g x β‰  PosInf) ∧
            g ∈ measurable a Borel ∧ (βˆ€x. x ∈ space a β‡’ (h x = f x * g x)) β‡’
            h ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_MUL_INDICATOR]  Theorem
      
      ⊒ βˆ€a f s.
            sigma_algebra a ∧ f ∈ measurable a Borel ∧ s ∈ subsets a β‡’
            (λx. f x * indicator_fn s x) ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_MUL_INDICATOR_EQ]  Theorem
      
      ⊒ βˆ€a f.
            sigma_algebra a β‡’
            (f ∈ measurable a Borel ⇔
             (λx. f x * indicator_fn (space a) x) ∈ measurable a Borel)
   
   [IN_MEASURABLE_BOREL_NEGINF]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel β‡’
            {x | f x = NegInf} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_PLUS_MINUS]  Theorem
      
      ⊒ βˆ€a f.
            f ∈ measurable a Borel ⇔
            fn_plus f ∈ measurable a Borel ∧
            fn_minus f ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_POS_SIMPLE_FN]  Theorem
      
      ⊒ βˆ€m f.
            measure_space m ∧ (βˆƒs a x. pos_simple_fn m f s a x) β‡’
            f ∈ measurable (m_space m,measurable_sets m) Borel
   
   [IN_MEASURABLE_BOREL_POW]  Theorem
      
      ⊒ βˆ€n a f.
            sigma_algebra a ∧ f ∈ measurable a Borel ∧
            (βˆ€x. x ∈ space a β‡’ f x β‰  NegInf ∧ f x β‰  PosInf) β‡’
            (λx. f x pow n) ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_SQR]  Theorem
      
      ⊒ βˆ€a f g.
            sigma_algebra a ∧ f ∈ measurable a Borel ∧
            (βˆ€x. x ∈ space a β‡’ (g x = f x pow 2)) β‡’
            g ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_SUB]  Theorem
      
      ⊒ βˆ€a f g h.
            sigma_algebra a ∧ f ∈ measurable a Borel ∧
            g ∈ measurable a Borel ∧ (βˆ€x. x ∈ space a β‡’ (h x = f x βˆ’ g x)) β‡’
            h ∈ measurable a Borel
   
   [IN_MEASURABLE_BOREL_SUM]  Theorem
      
      ⊒ βˆ€a f g s.
            FINITE s ∧ sigma_algebra a ∧
            (βˆ€i. i ∈ s β‡’ f i ∈ measurable a Borel) ∧
            (βˆ€x. x ∈ space a β‡’ (g x = SIGMA (Ξ»i. f i x) s)) β‡’
            g ∈ measurable a Borel
   
   [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) ∧ measure_space m1 ∧
            measure_space m2 ∧
            βˆ€s.
                s ∈ measurable_sets m2 β‡’
                (measure m1 (PREIMAGE f s ∩ m_space m1) = measure m2 s)
   
   [IN_SIGMA]  Theorem
      
      ⊒ βˆ€sp a x. x ∈ a β‡’ x ∈ subsets (sigma sp a)
   
   [LAMBDA_SYSTEM_ADDITIVE]  Theorem
      
      ⊒ βˆ€g0 lam l1 l2.
            algebra g0 ∧ positive (space g0,subsets g0,lam) β‡’
            additive (space g0,lambda_system g0 lam,lam)
   
   [LAMBDA_SYSTEM_ALGEBRA]  Theorem
      
      ⊒ βˆ€g0 lam.
            algebra g0 ∧ positive (space g0,subsets g0,lam) β‡’
            algebra (space g0,lambda_system g0 lam)
   
   [LAMBDA_SYSTEM_CARATHEODORY]  Theorem
      
      ⊒ βˆ€gsig lam.
            sigma_algebra gsig ∧
            outer_measure_space (space gsig,subsets gsig,lam) β‡’
            βˆ€f.
                f ∈ (π•Œ(:num) -> lambda_system gsig lam) ∧
                (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) β‡’
                BIGUNION (IMAGE f π•Œ(:num)) ∈ lambda_system gsig lam ∧
                lam ∘ f sums lam (BIGUNION (IMAGE f π•Œ(:num)))
   
   [LAMBDA_SYSTEM_COMPL]  Theorem
      
      ⊒ βˆ€g0 lam l.
            algebra g0 ∧ positive (space g0,subsets g0,lam) ∧
            l ∈ lambda_system g0 lam β‡’
            space g0 DIFF l ∈ lambda_system g0 lam
   
   [LAMBDA_SYSTEM_EMPTY]  Theorem
      
      ⊒ βˆ€g0 lam.
            algebra g0 ∧ positive (space g0,subsets g0,lam) β‡’
            βˆ… ∈ lambda_system g0 lam
   
   [LAMBDA_SYSTEM_INCREASING]  Theorem
      
      ⊒ βˆ€g0 lam.
            increasing (space g0,subsets g0,lam) β‡’
            increasing (space g0,lambda_system g0 lam,lam)
   
   [LAMBDA_SYSTEM_INTER]  Theorem
      
      ⊒ βˆ€g0 lam l1 l2.
            algebra g0 ∧ positive (space g0,subsets g0,lam) ∧
            l1 ∈ lambda_system g0 lam ∧ l2 ∈ lambda_system g0 lam β‡’
            l1 ∩ l2 ∈ lambda_system g0 lam
   
   [LAMBDA_SYSTEM_POSITIVE]  Theorem
      
      ⊒ βˆ€g0 lam.
            positive (space g0,subsets g0,lam) β‡’
            positive (space g0,lambda_system g0 lam,lam)
   
   [LAMBDA_SYSTEM_STRONG_ADDITIVE]  Theorem
      
      ⊒ βˆ€g0 lam g l1 l2.
            algebra g0 ∧ positive (space g0,subsets g0,lam) ∧
            g ∈ subsets g0 ∧ DISJOINT l1 l2 ∧ l1 ∈ lambda_system g0 lam ∧
            l2 ∈ lambda_system g0 lam β‡’
            (lam ((l1 βˆͺ l2) ∩ g) = lam (l1 ∩ g) + lam (l2 ∩ g))
   
   [LAMBDA_SYSTEM_STRONG_SUM]  Theorem
      
      ⊒ βˆ€g0 lam g f n.
            algebra g0 ∧ positive (space g0,subsets g0,lam) ∧
            g ∈ subsets g0 ∧ f ∈ (π•Œ(:num) -> lambda_system g0 lam) ∧
            (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) β‡’
            (sum (0,n) (lam ∘ (λs. s ∩ g) ∘ f) =
             lam (BIGUNION (IMAGE f (count n)) ∩ g))
   
   [MEASUBABLE_BIGUNION_LEMMA]  Theorem
      
      ⊒ βˆ€a b f.
            sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
            (βˆ€s. s ∈ subsets b β‡’ PREIMAGE f s ∈ subsets a) β‡’
            βˆ€c.
                countable c ∧ c βŠ† IMAGE (PREIMAGE f) (subsets b) β‡’
                BIGUNION c ∈ IMAGE (PREIMAGE f) (subsets b)
   
   [MEASURABLE_BIGUNION_PROPERTY]  Theorem
      
      ⊒ βˆ€a b f.
            sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
            (βˆ€s. s ∈ subsets b β‡’ PREIMAGE f s ∈ subsets a) β‡’
            βˆ€c.
                c βŠ† subsets b β‡’
                (PREIMAGE f (BIGUNION c) = BIGUNION (IMAGE (PREIMAGE f) c))
   
   [MEASURABLE_BOREL]  Theorem
      
      ⊒ βˆ€f a.
            f ∈ measurable a Borel ⇔
            sigma_algebra a ∧ f ∈ (space a -> π•Œ(:extreal)) ∧
            βˆ€c. PREIMAGE f {x | x < c} ∩ space a ∈ subsets a
   
   [MEASURABLE_COMP]  Theorem
      
      ⊒ βˆ€f g a b c.
            f ∈ measurable a b ∧ g ∈ measurable b c β‡’
            g ∘ f ∈ measurable a c
   
   [MEASURABLE_COMP_STRONG]  Theorem
      
      ⊒ βˆ€f g a b c.
            f ∈ measurable a b ∧ sigma_algebra c ∧
            g ∈ (space b -> space c) ∧
            (βˆ€x.
                 x ∈ subsets c β‡’
                 PREIMAGE g x ∩ IMAGE f (space a) ∈ subsets b) β‡’
            g ∘ f ∈ measurable a c
   
   [MEASURABLE_COMP_STRONGER]  Theorem
      
      ⊒ βˆ€f g a b c t.
            f ∈ measurable a b ∧ sigma_algebra c ∧
            g ∈ (space b -> space c) ∧ IMAGE f (space a) βŠ† t ∧
            (βˆ€s. s ∈ subsets c β‡’ PREIMAGE g s ∩ t ∈ subsets b) β‡’
            g ∘ f ∈ measurable a c
   
   [MEASURABLE_DIFF_PROPERTY]  Theorem
      
      ⊒ βˆ€a b f.
            sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
            (βˆ€s. s ∈ subsets b β‡’ PREIMAGE f s ∈ subsets a) β‡’
            βˆ€s.
                s ∈ subsets b β‡’
                (PREIMAGE f (space b DIFF s) = space a DIFF PREIMAGE f s)
   
   [MEASURABLE_I]  Theorem
      
      ⊒ βˆ€a. sigma_algebra a β‡’ I ∈ measurable a a
   
   [MEASURABLE_LIFT]  Theorem
      
      ⊒ βˆ€f a b.
            f ∈ measurable a b β‡’
            f ∈ measurable a (sigma (space b) (subsets b))
   
   [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_PROD_SIGMA]  Theorem
      
      ⊒ βˆ€a a1 a2 f.
            sigma_algebra a ∧ FST ∘ f ∈ measurable a a1 ∧
            SND ∘ f ∈ measurable a a2 β‡’
            f ∈
            measurable a
              (sigma (space a1 Γ— space a2)
                 (prod_sets (subsets a1) (subsets a2)))
   
   [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
   
   [MEASURABLE_SIGMA]  Theorem
      
      ⊒ βˆ€f a b sp.
            sigma_algebra a ∧ subset_class sp b ∧ f ∈ (space a -> sp) ∧
            (βˆ€s. s ∈ b β‡’ PREIMAGE f s ∩ space a ∈ subsets a) β‡’
            f ∈ measurable a (sigma sp b)
   
   [MEASURABLE_SIGMA_PREIMAGES]  Theorem
      
      ⊒ βˆ€a b f.
            sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a -> space b) ∧
            (βˆ€s. s ∈ subsets b β‡’ PREIMAGE f s ∈ subsets a) β‡’
            sigma_algebra (space a,IMAGE (PREIMAGE f) (subsets b))
   
   [MEASURABLE_SUBSET]  Theorem
      
      ⊒ βˆ€a b. measurable a b βŠ† measurable a (sigma (space b) (subsets b))
   
   [MEASURABLE_UP_LIFT]  Theorem
      
      ⊒ βˆ€sp a b c f.
            f ∈ measurable (sp,a) c ∧ sigma_algebra (sp,b) ∧ a βŠ† b β‡’
            f ∈ measurable (sp,b) c
   
   [MEASURABLE_UP_SIGMA]  Theorem
      
      ⊒ βˆ€a b. measurable a b βŠ† measurable (sigma (space a) (subsets a)) b
   
   [MEASURABLE_UP_SUBSET]  Theorem
      
      ⊒ βˆ€sp a b c.
            a βŠ† b ∧ sigma_algebra (sp,b) β‡’
            measurable (sp,a) c βŠ† measurable (sp,b) c
   
   [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 (m_space m DIFF s) =
             measure m (m_space m) βˆ’ measure m s)
   
   [MEASURE_COMPL_SUBSET]  Theorem
      
      ⊒ βˆ€m s.
            measure_space m ∧ s ∈ measurable_sets m ∧
            t ∈ measurable_sets m ∧ t βŠ† s β‡’
            (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))) β‡’
            measure m ∘ f --> 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))) β‡’
            measure m ∘ f sums measure m s
   
   [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_PRESERVING_LIFT]  Theorem
      
      ⊒ βˆ€m1 m2 a f.
            measure_space m1 ∧ measure_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 ∧
            (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.
            measure_space m1 ∧
            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.
            measure_space m1 ∧
            (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.
            measure_space m1 ∧ 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_REAL_SUM_IMAGE]  Theorem
      
      ⊒ βˆ€m s.
            measure_space m ∧ s ∈ measurable_sets m ∧
            (βˆ€x. x ∈ s β‡’ {x} ∈ measurable_sets m) ∧ FINITE s β‡’
            (measure m s = SIGMA (Ξ»x. measure m {x}) s)
   
   [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. c * measure m a))
   
   [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_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_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))) β‡’
            measure m ∘ f --> measure m s
   
   [MONOTONE_CONVERGENCE2]  Theorem
      
      ⊒ βˆ€m f.
            measure_space m ∧ f ∈ (π•Œ(:num) -> measurable_sets m) ∧
            (βˆ€n. f n βŠ† f (SUC n)) β‡’
            measure m ∘ f --> measure m (BIGUNION (IMAGE f π•Œ(:num)))
   
   [MONOTONE_CONVERGENCE_BIGINTER]  Theorem
      
      ⊒ βˆ€m s f.
            measure_space m ∧ f ∈ (π•Œ(:num) -> measurable_sets m) ∧
            (βˆ€n. f (SUC n) βŠ† f n) ∧ (s = BIGINTER (IMAGE f π•Œ(:num))) β‡’
            measure m ∘ f --> measure m s
   
   [MONOTONE_CONVERGENCE_BIGINTER2]  Theorem
      
      ⊒ βˆ€m f.
            measure_space m ∧ f ∈ (π•Œ(:num) -> measurable_sets m) ∧
            (βˆ€n. f (SUC n) βŠ† f n) β‡’
            measure m ∘ f --> measure m (BIGINTER (IMAGE f π•Œ(:num)))
   
   [OUTER_MEASURE_SPACE_POSITIVE]  Theorem
      
      ⊒ βˆ€m. outer_measure_space m β‡’ positive m
   
   [POW_ALGEBRA]  Theorem
      
      ⊒ algebra (sp,POW sp)
   
   [POW_SIGMA_ALGEBRA]  Theorem
      
      ⊒ sigma_algebra (sp,POW sp)
   
   [SIGMA_ALGEBRA]  Theorem
      
      ⊒ βˆ€p.
            sigma_algebra p ⇔
            subset_class (space p) (subsets p) ∧ βˆ… ∈ subsets p ∧
            (βˆ€s. s ∈ subsets p β‡’ space p DIFF s ∈ subsets p) ∧
            βˆ€c. countable c ∧ c βŠ† subsets p β‡’ BIGUNION c ∈ subsets p
   
   [SIGMA_ALGEBRA_ALGEBRA]  Theorem
      
      ⊒ βˆ€a. sigma_algebra a β‡’ algebra a
   
   [SIGMA_ALGEBRA_ALT]  Theorem
      
      ⊒ βˆ€a.
            sigma_algebra a ⇔
            algebra a ∧
            βˆ€f.
                f ∈ (π•Œ(:num) -> subsets a) β‡’
                BIGUNION (IMAGE f π•Œ(:num)) ∈ subsets a
   
   [SIGMA_ALGEBRA_ALT_DISJOINT]  Theorem
      
      ⊒ βˆ€a.
            sigma_algebra a ⇔
            algebra a ∧
            βˆ€f.
                f ∈ (π•Œ(:num) -> subsets a) ∧
                (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) β‡’
                BIGUNION (IMAGE f π•Œ(:num)) ∈ subsets a
   
   [SIGMA_ALGEBRA_ALT_MONO]  Theorem
      
      ⊒ βˆ€a.
            sigma_algebra a ⇔
            algebra a ∧
            βˆ€f.
                f ∈ (π•Œ(:num) -> subsets a) ∧ (f 0 = βˆ…) ∧
                (βˆ€n. f n βŠ† f (SUC n)) β‡’
                BIGUNION (IMAGE f π•Œ(:num)) ∈ subsets a
   
   [SIGMA_ALGEBRA_BOREL]  Theorem
      
      ⊒ sigma_algebra Borel
   
   [SIGMA_ALGEBRA_COUNTABLE_UNION]  Theorem
      
      ⊒ βˆ€a c.
            sigma_algebra a ∧ countable c ∧ c βŠ† subsets a β‡’
            BIGUNION c ∈ subsets a
   
   [SIGMA_ALGEBRA_ENUM]  Theorem
      
      ⊒ βˆ€a f.
            sigma_algebra a ∧ f ∈ (π•Œ(:num) -> subsets a) β‡’
            BIGUNION (IMAGE f π•Œ(:num)) ∈ subsets a
   
   [SIGMA_ALGEBRA_FN]  Theorem
      
      ⊒ βˆ€a.
            sigma_algebra a ⇔
            subset_class (space a) (subsets a) ∧ βˆ… ∈ subsets a ∧
            (βˆ€s. s ∈ subsets a β‡’ space a DIFF s ∈ subsets a) ∧
            βˆ€f.
                f ∈ (π•Œ(:num) -> subsets a) β‡’
                BIGUNION (IMAGE f π•Œ(:num)) ∈ subsets a
   
   [SIGMA_ALGEBRA_FN_BIGINTER]  Theorem
      
      ⊒ βˆ€a.
            sigma_algebra a β‡’
            subset_class (space a) (subsets a) ∧ βˆ… ∈ subsets a ∧
            (βˆ€s. s ∈ subsets a β‡’ space a DIFF s ∈ subsets a) ∧
            βˆ€f.
                f ∈ (π•Œ(:num) -> subsets a) β‡’
                BIGINTER (IMAGE f π•Œ(:num)) ∈ subsets a
   
   [SIGMA_ALGEBRA_FN_DISJOINT]  Theorem
      
      ⊒ βˆ€a.
            sigma_algebra a ⇔
            subset_class (space a) (subsets a) ∧ βˆ… ∈ subsets a ∧
            (βˆ€s. s ∈ subsets a β‡’ space a DIFF s ∈ subsets a) ∧
            (βˆ€s t. s ∈ subsets a ∧ t ∈ subsets a β‡’ s βˆͺ t ∈ subsets a) ∧
            βˆ€f.
                f ∈ (π•Œ(:num) -> subsets a) ∧
                (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) β‡’
                BIGUNION (IMAGE f π•Œ(:num)) ∈ subsets a
   
   [SIGMA_ALGEBRA_SIGMA]  Theorem
      
      ⊒ βˆ€sp sts. subset_class sp sts β‡’ sigma_algebra (sigma sp sts)
   
   [SIGMA_POW]  Theorem
      
      ⊒ βˆ€s. sigma s (POW s) = (s,POW s)
   
   [SIGMA_PROPERTY]  Theorem
      
      ⊒ βˆ€sp p a.
            subset_class sp p ∧ βˆ… ∈ p ∧ a βŠ† p ∧
            (βˆ€s. s ∈ p ∩ subsets (sigma sp a) β‡’ sp DIFF s ∈ p) ∧
            (βˆ€c.
                 countable c ∧ c βŠ† p ∩ subsets (sigma sp a) β‡’
                 BIGUNION c ∈ p) β‡’
            subsets (sigma sp a) βŠ† p
   
   [SIGMA_PROPERTY_ALT]  Theorem
      
      ⊒ βˆ€sp p a.
            subset_class sp p ∧ βˆ… ∈ p ∧ a βŠ† p ∧
            (βˆ€s. s ∈ p ∩ subsets (sigma sp a) β‡’ sp DIFF s ∈ p) ∧
            (βˆ€f.
                 f ∈ (π•Œ(:num) -> p ∩ subsets (sigma sp a)) β‡’
                 BIGUNION (IMAGE f π•Œ(:num)) ∈ p) β‡’
            subsets (sigma sp a) βŠ† p
   
   [SIGMA_PROPERTY_DISJOINT]  Theorem
      
      ⊒ βˆ€sp p a.
            algebra (sp,a) ∧ a βŠ† p ∧
            (βˆ€s. s ∈ p ∩ subsets (sigma sp a) β‡’ sp DIFF s ∈ p) ∧
            (βˆ€f.
                 f ∈ (π•Œ(:num) -> p ∩ subsets (sigma sp a)) ∧ (f 0 = βˆ…) ∧
                 (βˆ€n. f n βŠ† f (SUC n)) β‡’
                 BIGUNION (IMAGE f π•Œ(:num)) ∈ p) ∧
            (βˆ€f.
                 f ∈ (π•Œ(:num) -> p ∩ subsets (sigma sp a)) ∧
                 (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) β‡’
                 BIGUNION (IMAGE f π•Œ(:num)) ∈ p) β‡’
            subsets (sigma sp a) βŠ† p
   
   [SIGMA_PROPERTY_DISJOINT_LEMMA]  Theorem
      
      ⊒ βˆ€sp a p.
            algebra (sp,a) ∧ a βŠ† p ∧ closed_cdi (sp,p) β‡’
            subsets (sigma sp a) βŠ† p
   
   [SIGMA_PROPERTY_DISJOINT_LEMMA1]  Theorem
      
      ⊒ βˆ€a.
            algebra a β‡’
            βˆ€s t.
                s ∈ subsets a ∧ t ∈ subsets (smallest_closed_cdi a) β‡’
                s ∩ t ∈ subsets (smallest_closed_cdi a)
   
   [SIGMA_PROPERTY_DISJOINT_LEMMA2]  Theorem
      
      ⊒ βˆ€a.
            algebra a β‡’
            βˆ€s t.
                s ∈ subsets (smallest_closed_cdi a) ∧
                t ∈ subsets (smallest_closed_cdi a) β‡’
                s ∩ t ∈ subsets (smallest_closed_cdi a)
   
   [SIGMA_PROPERTY_DISJOINT_WEAK]  Theorem
      
      ⊒ βˆ€sp p a.
            algebra (sp,a) ∧ a βŠ† p ∧ subset_class sp p ∧
            (βˆ€s. s ∈ p β‡’ sp DIFF s ∈ p) ∧
            (βˆ€f.
                 f ∈ (π•Œ(:num) -> p) ∧ (f 0 = βˆ…) ∧ (βˆ€n. f n βŠ† f (SUC n)) β‡’
                 BIGUNION (IMAGE f π•Œ(:num)) ∈ p) ∧
            (βˆ€f.
                 f ∈ (π•Œ(:num) -> p) ∧ (βˆ€m n. m β‰  n β‡’ DISJOINT (f m) (f n)) β‡’
                 BIGUNION (IMAGE f π•Œ(:num)) ∈ p) β‡’
            subsets (sigma sp a) βŠ† p
   
   [SIGMA_REDUCE]  Theorem
      
      ⊒ βˆ€sp a. (sp,subsets (sigma sp a)) = sigma sp a
   
   [SIGMA_SUBSET]  Theorem
      
      ⊒ βˆ€a b.
            sigma_algebra b ∧ a βŠ† subsets b β‡’
            subsets (sigma (space b) a) βŠ† subsets b
   
   [SIGMA_SUBSET_MEASURABLE_SETS]  Theorem
      
      ⊒ βˆ€a m.
            measure_space m ∧ a βŠ† measurable_sets m β‡’
            subsets (sigma (m_space m) a) βŠ† measurable_sets m
   
   [SIGMA_SUBSET_SUBSETS]  Theorem
      
      ⊒ βˆ€sp a. a βŠ† subsets (sigma sp a)
   
   [SMALLEST_CLOSED_CDI]  Theorem
      
      ⊒ βˆ€a.
            algebra a β‡’
            subsets a βŠ† subsets (smallest_closed_cdi a) ∧
            closed_cdi (smallest_closed_cdi a) ∧
            subset_class (space a) (subsets (smallest_closed_cdi a))
   
   [SPACE]  Theorem
      
      ⊒ βˆ€a. (space a,subsets a) = a
   
   [SPACE_BOREL]  Theorem
      
      ⊒ space Borel = π•Œ(:extreal)
   
   [SPACE_SIGMA]  Theorem
      
      ⊒ βˆ€sp a. space (sigma sp a) = sp
   
   [SPACE_SMALLEST_CLOSED_CDI]  Theorem
      
      ⊒ βˆ€a. space (smallest_closed_cdi a) = space a
   
   [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 = s βˆͺ t) β‡’
            measure m u ≀ measure m s + measure m t
   
   [SUBSET_BIGINTER]  Theorem
      
      ⊒ βˆ€X P. X βŠ† BIGINTER P ⇔ βˆ€Y. Y ∈ P β‡’ X βŠ† Y
   
   [UNIV_SIGMA_ALGEBRA]  Theorem
      
      ⊒ sigma_algebra (π•Œ(:Ξ±),π•Œ(:Ξ± -> bool))
   
   [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
   
   [indicator_fn_split]  Theorem
      
      ⊒ βˆ€r s b.
            FINITE r ∧ (BIGUNION (IMAGE b r) = s) ∧
            (βˆ€i j. i ∈ r ∧ j ∈ r ∧ i β‰  j β‡’ DISJOINT (b i) (b j)) β‡’
            βˆ€a.
                a βŠ† s β‡’
                (indicator_fn a =
                 (λx. SIGMA (λi. indicator_fn (a ∩ b i) x) r))
   
   [indicator_fn_suminf]  Theorem
      
      ⊒ βˆ€a x.
            (βˆ€m n. m β‰  n β‡’ DISJOINT (a m) (a n)) β‡’
            (suminf (Ξ»i. indicator_fn (a i) x) =
             indicator_fn (BIGUNION (IMAGE a π•Œ(:num))) x)
   
   [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 = SIGMA (λi. measure m (a ∩ b i)) r)
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13