Structure sigma_algebraTheory

signature sigma_algebraTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val algebra_def : thm
    val dynkin_def : thm
    val dynkin_system_def : thm
    val measurable_def : thm
    val prod_sigma_def : thm
    val ring_def : thm
    val semiring_def : thm
    val sigma_algebra_def : thm
    val sigma_def : thm
    val sigma_function_def : thm
    val sigma_functions_def : thm
    val sigma_sets_def : thm
    val smallest_ring_def : thm
    val space_def : thm
    val subset_class_def : thm
    val subsets_def : thm
  
  (*  Theorems  *)
    val ALGEBRA_ALT_INTER : thm
    val ALGEBRA_COMPL : thm
    val ALGEBRA_COMPL_SETS : thm
    val ALGEBRA_DIFF : thm
    val ALGEBRA_EMPTY : thm
    val ALGEBRA_FINITE_UNION : thm
    val ALGEBRA_IMP_RING : thm
    val ALGEBRA_IMP_SEMIRING : thm
    val ALGEBRA_INTER : thm
    val ALGEBRA_INTER_SPACE : thm
    val ALGEBRA_RESTRICT : thm
    val ALGEBRA_SETS_COLLECT_CONST : thm
    val ALGEBRA_SETS_COLLECT_IMP : thm
    val ALGEBRA_SETS_COLLECT_NEG : thm
    val ALGEBRA_SINGLE_SET : thm
    val ALGEBRA_SPACE : thm
    val ALGEBRA_UNION : thm
    val DYNKIN : thm
    val DYNKIN_LEMMA : thm
    val DYNKIN_MONOTONE : thm
    val DYNKIN_SMALLEST : thm
    val DYNKIN_STABLE : thm
    val DYNKIN_STABLE_LEMMA : thm
    val DYNKIN_SUBSET : thm
    val DYNKIN_SUBSET_SIGMA : thm
    val DYNKIN_SUBSET_SUBSETS : thm
    val DYNKIN_SYSTEM_ALT : thm
    val DYNKIN_SYSTEM_ALT_MONO : thm
    val DYNKIN_SYSTEM_COMPL : thm
    val DYNKIN_SYSTEM_COUNTABLY_DUNION : thm
    val DYNKIN_SYSTEM_DUNION : thm
    val DYNKIN_SYSTEM_EMPTY : thm
    val DYNKIN_SYSTEM_INCREASING : thm
    val DYNKIN_SYSTEM_SPACE : thm
    val DYNKIN_THM : thm
    val INTER_SPACE_EQ1 : thm
    val INTER_SPACE_REDUCE : thm
    val IN_DYNKIN : thm
    val IN_MEASURABLE : thm
    val IN_SIGMA : thm
    val MEASUBABLE_BIGUNION_LEMMA : thm
    val MEASURABLE_BIGUNION_PROPERTY : 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_PROD_SIGMA : thm
    val MEASURABLE_PROD_SIGMA' : 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 POW_ALGEBRA : thm
    val POW_SIGMA_ALGEBRA : thm
    val PREIMAGE_SIGMA : thm
    val PREIMAGE_SIGMA_ALGEBRA : thm
    val RING_BIGUNION : thm
    val RING_DIFF : thm
    val RING_DIFF_ALT : thm
    val RING_EMPTY : thm
    val RING_FINITE_BIGUNION1 : thm
    val RING_FINITE_BIGUNION2 : thm
    val RING_FINITE_INTER : thm
    val RING_FINITE_UNION : thm
    val RING_FINITE_UNION_ALT : thm
    val RING_IMP_SEMIRING : thm
    val RING_INSERT : thm
    val RING_INTER : thm
    val RING_SETS_COLLECT_FINITE : thm
    val RING_SPACE_IMP_ALGEBRA : thm
    val RING_UNION : thm
    val SEMIRING_DIFF : thm
    val SEMIRING_DIFF_ALT : thm
    val SEMIRING_EMPTY : thm
    val SEMIRING_INTER : thm
    val SEMIRING_PROD_SETS : thm
    val SEMIRING_PROD_SETS' : thm
    val SEMIRING_SETS_COLLECT : 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_ALT_SPACE : thm
    val SIGMA_ALGEBRA_COMPL : thm
    val SIGMA_ALGEBRA_COUNTABLE_INT : thm
    val SIGMA_ALGEBRA_COUNTABLE_INT' : thm
    val SIGMA_ALGEBRA_COUNTABLE_UN : thm
    val SIGMA_ALGEBRA_COUNTABLE_UN' : thm
    val SIGMA_ALGEBRA_COUNTABLE_UNION : thm
    val SIGMA_ALGEBRA_DIFF : thm
    val SIGMA_ALGEBRA_EMPTY : 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_IMP_DYNKIN_SYSTEM : thm
    val SIGMA_ALGEBRA_INTER : thm
    val SIGMA_ALGEBRA_PROD_SIGMA : thm
    val SIGMA_ALGEBRA_PROD_SIGMA' : thm
    val SIGMA_ALGEBRA_RESTRICT : thm
    val SIGMA_ALGEBRA_RESTRICT_SUBSET : thm
    val SIGMA_ALGEBRA_SIGMA : thm
    val SIGMA_ALGEBRA_SPACE : thm
    val SIGMA_ALGEBRA_UNION : thm
    val SIGMA_CONG : thm
    val SIGMA_MEASURABLE : thm
    val SIGMA_MONOTONE : 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_PROPERTY_DISJOINT_WEAK_ALT : thm
    val SIGMA_REDUCE : thm
    val SIGMA_SIMULTANEOUSLY_MEASURABLE : thm
    val SIGMA_SMALLEST : thm
    val SIGMA_STABLE : thm
    val SIGMA_STABLE_LEMMA : thm
    val SIGMA_SUBSET : thm
    val SIGMA_SUBSET_SUBSETS : thm
    val SMALLEST_RING : thm
    val SMALLEST_RING_OF_SEMIRING : thm
    val SMALLEST_RING_SUBSET_SUBSETS : thm
    val SPACE : thm
    val SPACE_DYNKIN : thm
    val SPACE_PROD_SIGMA : thm
    val SPACE_SIGMA : thm
    val SPACE_SMALLEST_RING : thm
    val UNIV_SIGMA_ALGEBRA : thm
    val algebra_alt : thm
    val algebra_alt_inter : thm
    val algebra_alt_union : thm
    val prod_sigma_alt_sigma_functions : thm
    val ring_alt : thm
    val ring_alt_pow : thm
    val ring_alt_pow_imp : thm
    val ring_and_semiring : thm
    val ring_disjointed_sets : thm
    val semiring_alt : thm
    val sigma_algebra_alt : thm
    val sigma_algebra_alt_pow : thm
    val sigma_algebra_sigma_sets : thm
    val sigma_sets_BIGINTER : thm
    val sigma_sets_BIGINTER2 : thm
    val sigma_sets_BIGUNION : thm
    val sigma_sets_basic : thm
    val sigma_sets_cases : thm
    val sigma_sets_compl : thm
    val sigma_sets_empty : thm
    val sigma_sets_fixpoint : thm
    val sigma_sets_ind : thm
    val sigma_sets_into_sp : thm
    val sigma_sets_least_sigma_algebra : thm
    val sigma_sets_rules : thm
    val sigma_sets_strongind : thm
    val sigma_sets_subset : thm
    val sigma_sets_superset_generator : thm
    val sigma_sets_top : thm
    val sigma_sets_union : thm
    val subset_class_POW : thm
  
  val sigma_algebra_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [util_prob] Parent theory of "sigma_algebra"
   
   [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
   
   [dynkin_def]  Definition
      
      ⊢ ∀sp sts.
          dynkin sp sts =
          (sp,BIGINTER {d | sts ⊆ d ∧ dynkin_system (sp,d)})
   
   [dynkin_system_def]  Definition
      
      ⊢ ∀d. dynkin_system d ⇔
            subset_class (space d) (subsets d) ∧ space d ∈ subsets d ∧
            (∀s. s ∈ subsets d ⇒ space d DIFF s ∈ subsets d) ∧
            ∀f. f ∈ (𝕌(:num) → subsets d) ∧
                (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
                BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d
   
   [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}
   
   [prod_sigma_def]  Definition
      
      ⊢ ∀a b.
          a × b =
          sigma (space a × space b) (prod_sets (subsets a) (subsets b))
   
   [ring_def]  Definition
      
      ⊢ ∀r. ring r ⇔
            subset_class (space r) (subsets r) ∧ ∅ ∈ subsets r ∧
            (∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∪ t ∈ subsets r) ∧
            ∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s DIFF t ∈ subsets r
   
   [semiring_def]  Definition
      
      ⊢ ∀r. semiring r ⇔
            subset_class (space r) (subsets r) ∧ ∅ ∈ subsets r ∧
            (∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∩ t ∈ subsets r) ∧
            ∀s t.
              s ∈ subsets r ∧ t ∈ subsets r ⇒
              ∃c. c ⊆ subsets r ∧ FINITE c ∧ disjoint c ∧
                  s DIFF t = BIGUNION c
   
   [sigma_algebra_def]  Definition
      
      ⊢ ∀a. sigma_algebra a ⇔
            algebra a ∧
            ∀c. countable c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a
   
   [sigma_def]  Definition
      
      ⊢ ∀sp sts.
          sigma sp sts = (sp,BIGINTER {s | sts ⊆ s ∧ sigma_algebra (sp,s)})
   
   [sigma_function_def]  Definition
      
      ⊢ ∀sp A f.
          sigma sp A f = (sp,IMAGE (λs. PREIMAGE f s ∩ sp) (subsets A))
   
   [sigma_functions_def]  Definition
      
      ⊢ ∀sp A f J.
          sigma sp A f J =
          sigma sp
            (BIGUNION
               (IMAGE
                  (λi. IMAGE (λs. PREIMAGE (f i) s ∩ sp) (subsets (A i))) J))
   
   [sigma_sets_def]  Definition
      
      ⊢ sigma_sets =
        (λsp st a0.
             ∀sigma_sets'.
               (∀a0.
                  a0 = ∅ ∨ st a0 ∨ (∃a. a0 = sp DIFF a ∧ sigma_sets' a) ∨
                  (∃A. a0 = BIGUNION {A i | i ∈ 𝕌(:num)} ∧
                       ∀i. sigma_sets' (A i)) ⇒
                  sigma_sets' a0) ⇒
               sigma_sets' a0)
   
   [smallest_ring_def]  Definition
      
      ⊢ ∀sp sts.
          smallest_ring sp sts = (sp,BIGINTER {s | sts ⊆ s ∧ ring (sp,s)})
   
   [space_def]  Definition
      
      ⊢ ∀x y. space (x,y) = x
   
   [subset_class_def]  Definition
      
      ⊢ ∀sp sts. subset_class sp sts ⇔ ∀x. x ∈ sts ⇒ x ⊆ sp
   
   [subsets_def]  Definition
      
      ⊢ ∀x y. subsets (x,y) = y
   
   [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_COMPL_SETS]  Theorem
      
      ⊢ ∀sp sts a. algebra (sp,sts) ∧ a ∈ sts ⇒ sp DIFF a ∈ sts
   
   [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_IMP_RING]  Theorem
      
      ⊢ ∀a. algebra a ⇒ ring a
   
   [ALGEBRA_IMP_SEMIRING]  Theorem
      
      ⊢ ∀a. algebra a ⇒ semiring 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_RESTRICT]  Theorem
      
      ⊢ ∀sp sts a.
          algebra (sp,sts) ∧ a ∈ sts ⇒ algebra (a,IMAGE (λs. s ∩ a) sts)
   
   [ALGEBRA_SETS_COLLECT_CONST]  Theorem
      
      ⊢ ∀sp sts P. algebra (sp,sts) ⇒ {x | x ∈ sp ∧ P} ∈ sts
   
   [ALGEBRA_SETS_COLLECT_IMP]  Theorem
      
      ⊢ ∀sp sts P Q.
          algebra (sp,sts) ∧ {x | x ∈ sp ∧ P x} ∈ sts ⇒
          {x | x ∈ sp ∧ Q x} ∈ sts ⇒
          {x | x ∈ sp ∧ (Q x ⇒ P x)} ∈ sts
   
   [ALGEBRA_SETS_COLLECT_NEG]  Theorem
      
      ⊢ ∀sp sts P.
          algebra (sp,sts) ∧ {x | x ∈ sp ∧ P x} ∈ sts ⇒
          {x | x ∈ sp ∧ ¬P x} ∈ sts
   
   [ALGEBRA_SINGLE_SET]  Theorem
      
      ⊢ ∀X S. X ⊆ S ⇒ algebra (S,{∅; X; S DIFF X; S})
   
   [ALGEBRA_SPACE]  Theorem
      
      ⊢ ∀a. algebra a ⇒ space a ∈ subsets a
   
   [ALGEBRA_UNION]  Theorem
      
      ⊢ ∀a s t.
          algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a
   
   [DYNKIN]  Theorem
      
      ⊢ ∀sp sts.
          subset_class sp sts ⇒
          sts ⊆ subsets (dynkin sp sts) ∧ dynkin_system (dynkin sp sts) ∧
          subset_class sp (subsets (dynkin sp sts))
   
   [DYNKIN_LEMMA]  Theorem
      
      ⊢ ∀d. dynkin_system d ∧
            (∀s t. s ∈ subsets d ∧ t ∈ subsets d ⇒ s ∩ t ∈ subsets d) ⇔
            sigma_algebra d
   
   [DYNKIN_MONOTONE]  Theorem
      
      ⊢ ∀sp a b. a ⊆ b ⇒ subsets (dynkin sp a) ⊆ subsets (dynkin sp b)
   
   [DYNKIN_SMALLEST]  Theorem
      
      ⊢ ∀sp sts D.
          sts ⊆ D ∧ D ⊆ subsets (dynkin sp sts) ∧ dynkin_system (sp,D) ⇒
          D = subsets (dynkin sp sts)
   
   [DYNKIN_STABLE]  Theorem
      
      ⊢ ∀d. dynkin_system d ⇒ dynkin (space d) (subsets d) = d
   
   [DYNKIN_STABLE_LEMMA]  Theorem
      
      ⊢ ∀sp sts. dynkin_system (sp,sts) ⇒ dynkin sp sts = (sp,sts)
   
   [DYNKIN_SUBSET]  Theorem
      
      ⊢ ∀a b.
          dynkin_system b ∧ a ⊆ subsets b ⇒
          subsets (dynkin (space b) a) ⊆ subsets b
   
   [DYNKIN_SUBSET_SIGMA]  Theorem
      
      ⊢ ∀sp sts.
          subset_class sp sts ⇒
          subsets (dynkin sp sts) ⊆ subsets (sigma sp sts)
   
   [DYNKIN_SUBSET_SUBSETS]  Theorem
      
      ⊢ ∀sp a. a ⊆ subsets (dynkin sp a)
   
   [DYNKIN_SYSTEM_ALT]  Theorem
      
      ⊢ ∀d. dynkin_system d ⇔
            subset_class (space d) (subsets d) ∧ space d ∈ subsets d ∧
            (∀s. s ∈ subsets d ⇒ space d DIFF s ∈ subsets d) ∧
            (∀f. f ∈ (𝕌(:num) → subsets d) ∧ f 0 = ∅ ∧
                 (∀n. f n ⊆ f (SUC n)) ⇒
                 BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d) ∧
            ∀f. f ∈ (𝕌(:num) → subsets d) ∧
                (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
                BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d
   
   [DYNKIN_SYSTEM_ALT_MONO]  Theorem
      
      ⊢ ∀d. dynkin_system d ⇔
            subset_class (space d) (subsets d) ∧ space d ∈ subsets d ∧
            (∀s t.
               s ∈ subsets d ∧ t ∈ subsets d ∧ s ⊆ t ⇒ t DIFF s ∈ subsets d) ∧
            ∀f. f ∈ (𝕌(:num) → subsets d) ∧ f 0 = ∅ ∧ (∀n. f n ⊆ f (SUC n)) ⇒
                BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d
   
   [DYNKIN_SYSTEM_COMPL]  Theorem
      
      ⊢ ∀d s. dynkin_system d ∧ s ∈ subsets d ⇒ space d DIFF s ∈ subsets d
   
   [DYNKIN_SYSTEM_COUNTABLY_DUNION]  Theorem
      
      ⊢ ∀d f.
          dynkin_system d ∧ f ∈ (𝕌(:num) → subsets d) ∧
          (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d
   
   [DYNKIN_SYSTEM_DUNION]  Theorem
      
      ⊢ ∀d s t.
          dynkin_system d ∧ s ∈ subsets d ∧ t ∈ subsets d ∧ DISJOINT s t ⇒
          s ∪ t ∈ subsets d
   
   [DYNKIN_SYSTEM_EMPTY]  Theorem
      
      ⊢ ∀d. dynkin_system d ⇒ ∅ ∈ subsets d
   
   [DYNKIN_SYSTEM_INCREASING]  Theorem
      
      ⊢ ∀p f.
          dynkin_system p ∧ f ∈ (𝕌(:num) → subsets p) ∧ f 0 = ∅ ∧
          (∀n. f n ⊆ f (SUC n)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets p
   
   [DYNKIN_SYSTEM_SPACE]  Theorem
      
      ⊢ ∀d. dynkin_system d ⇒ space d ∈ subsets d
   
   [DYNKIN_THM]  Theorem
      
      ⊢ ∀sp sts.
          subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ⇒
          dynkin sp sts = sigma sp sts
   
   [INTER_SPACE_EQ1]  Theorem
      
      ⊢ ∀sp sts. subset_class sp sts ⇒ ∀x. x ∈ sts ⇒ sp ∩ x = x
   
   [INTER_SPACE_REDUCE]  Theorem
      
      ⊢ ∀sp sts. subset_class sp sts ⇒ ∀x. x ∈ sts ⇒ x ∩ sp = x
   
   [IN_DYNKIN]  Theorem
      
      ⊢ ∀sp a x. x ∈ a ⇒ x ∈ subsets (dynkin sp a)
   
   [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_SIGMA]  Theorem
      
      ⊢ ∀sp a x. x ∈ a ⇒ x ∈ subsets (sigma sp a)
   
   [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_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_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_PROD_SIGMA']  Theorem
      
      ⊢ ∀a a1 a2 f.
          sigma_algebra a ∧ FST ∘ f ∈ measurable a a1 ∧
          SND ∘ f ∈ measurable a a2 ⇒
          f ∈ measurable a (a1 × a2)
   
   [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
   
   [POW_ALGEBRA]  Theorem
      
      ⊢ ∀sp. algebra (sp,POW sp)
   
   [POW_SIGMA_ALGEBRA]  Theorem
      
      ⊢ ∀sp. sigma_algebra (sp,POW sp)
   
   [PREIMAGE_SIGMA]  Theorem
      
      ⊢ ∀Z sp sts f.
          subset_class sp sts ∧ f ∈ (Z → sp) ⇒
          IMAGE (λs. PREIMAGE f s ∩ Z) (subsets (sigma sp sts)) =
          subsets (sigma Z (IMAGE (λs. PREIMAGE f s ∩ Z) sts))
   
   [PREIMAGE_SIGMA_ALGEBRA]  Theorem
      
      ⊢ ∀sp A f.
          sigma_algebra A ∧ f ∈ (sp → space A) ⇒
          sigma_algebra (sp,IMAGE (λs. PREIMAGE f s ∩ sp) (subsets A))
   
   [RING_BIGUNION]  Theorem
      
      ⊢ ∀sp sts A n.
          ring (sp,sts) ∧ IMAGE A 𝕌(:num) ⊆ sts ⇒
          BIGUNION {A i | i < n} ∈ sts
   
   [RING_DIFF]  Theorem
      
      ⊢ ∀r s t.
          ring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s DIFF t ∈ subsets r
   
   [RING_DIFF_ALT]  Theorem
      
      ⊢ ∀a b sp sts. ring (sp,sts) ∧ a ∈ sts ∧ b ∈ sts ⇒ a DIFF b ∈ sts
   
   [RING_EMPTY]  Theorem
      
      ⊢ ∀r. ring r ⇒ ∅ ∈ subsets r
   
   [RING_FINITE_BIGUNION1]  Theorem
      
      ⊢ ∀X sp sts. ring (sp,sts) ∧ FINITE X ⇒ X ⊆ sts ⇒ BIGUNION X ∈ sts
   
   [RING_FINITE_BIGUNION2]  Theorem
      
      ⊢ ∀A N sp sts.
          ring (sp,sts) ∧ FINITE N ∧ (∀i. i ∈ N ⇒ A i ∈ sts) ⇒
          BIGUNION {A i | i ∈ N} ∈ sts
   
   [RING_FINITE_INTER]  Theorem
      
      ⊢ ∀r f n.
          ring r ∧ 0 < n ∧ (∀i. i < n ⇒ f i ∈ subsets r) ⇒
          BIGINTER (IMAGE f (count n)) ∈ subsets r
   
   [RING_FINITE_UNION]  Theorem
      
      ⊢ ∀r c. ring r ∧ c ⊆ subsets r ∧ FINITE c ⇒ BIGUNION c ∈ subsets r
   
   [RING_FINITE_UNION_ALT]  Theorem
      
      ⊢ ∀r f n.
          ring r ∧ (∀i. i < n ⇒ f i ∈ subsets r) ⇒
          BIGUNION (IMAGE f (count n)) ∈ subsets r
   
   [RING_IMP_SEMIRING]  Theorem
      
      ⊢ ∀r. ring r ⇒ semiring r
   
   [RING_INSERT]  Theorem
      
      ⊢ ∀x A sp sts. ring (sp,sts) ∧ {x} ∈ sts ∧ A ∈ sts ⇒ x INSERT A ∈ sts
   
   [RING_INTER]  Theorem
      
      ⊢ ∀r s t. ring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∩ t ∈ subsets r
   
   [RING_SETS_COLLECT_FINITE]  Theorem
      
      ⊢ ∀sp sts s P.
          ring (sp,sts) ∧ (∀i. i ∈ s ⇒ {x | x ∈ sp ∧ P i x} ∈ sts) ∧
          FINITE s ⇒
          {x | x ∈ sp ∧ ∃i. i ∈ s ∧ P i x} ∈ sts
   
   [RING_SPACE_IMP_ALGEBRA]  Theorem
      
      ⊢ ∀r. ring r ∧ space r ∈ subsets r ⇒ algebra r
   
   [RING_UNION]  Theorem
      
      ⊢ ∀r s t. ring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∪ t ∈ subsets r
   
   [SEMIRING_DIFF]  Theorem
      
      ⊢ ∀r s t.
          semiring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒
          ∃c. c ⊆ subsets r ∧ FINITE c ∧ disjoint c ∧ s DIFF t = BIGUNION c
   
   [SEMIRING_DIFF_ALT]  Theorem
      
      ⊢ ∀r s t.
          semiring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒
          ∃f n.
            (∀i. i < n ⇒ f i ∈ subsets r) ∧
            (∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
            s DIFF t = BIGUNION (IMAGE f (count n))
   
   [SEMIRING_EMPTY]  Theorem
      
      ⊢ ∀r. semiring r ⇒ ∅ ∈ subsets r
   
   [SEMIRING_INTER]  Theorem
      
      ⊢ ∀r s t.
          semiring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∩ t ∈ subsets r
   
   [SEMIRING_PROD_SETS]  Theorem
      
      ⊢ ∀a b.
          semiring a ∧ semiring b ⇒
          semiring (space a × space b,prod_sets (subsets a) (subsets b))
   
   [SEMIRING_PROD_SETS']  Theorem
      
      ⊢ ∀a b.
          sigma_algebra a ∧ sigma_algebra b ⇒
          semiring (space a × space b,prod_sets (subsets a) (subsets b))
   
   [SEMIRING_SETS_COLLECT]  Theorem
      
      ⊢ ∀sp sts P Q.
          semiring (sp,sts) ∧ {x | x ∈ sp ∧ P x} ∈ sts ∧
          {x | x ∈ sp ∧ Q x} ∈ sts ⇒
          {x | x ∈ sp ∧ P x ∧ Q x} ∈ sts
   
   [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_ALT_SPACE]  Theorem
      
      ⊢ ∀a. sigma_algebra a ⇔
            subset_class (space a) (subsets a) ∧ space 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_COMPL]  Theorem
      
      ⊢ ∀a s. sigma_algebra a ∧ s ∈ subsets a ⇒ space a DIFF s ∈ subsets a
   
   [SIGMA_ALGEBRA_COUNTABLE_INT]  Theorem
      
      ⊢ ∀sp sts A X.
          sigma_algebra (sp,sts) ∧ IMAGE A X ⊆ sts ∧ X ≠ ∅ ⇒
          BIGINTER {A x | x ∈ X} ∈ sts
   
   [SIGMA_ALGEBRA_COUNTABLE_INT']  Theorem
      
      ⊢ ∀sp sts A X.
          sigma_algebra (sp,sts) ∧ countable X ∧ X ≠ ∅ ∧ IMAGE A X ⊆ sts ⇒
          BIGINTER {A x | x ∈ X} ∈ sts
   
   [SIGMA_ALGEBRA_COUNTABLE_UN]  Theorem
      
      ⊢ ∀sp sts A X.
          sigma_algebra (sp,sts) ∧ IMAGE A X ⊆ sts ⇒
          BIGUNION {A x | x ∈ X} ∈ sts
   
   [SIGMA_ALGEBRA_COUNTABLE_UN']  Theorem
      
      ⊢ ∀sp sts A X.
          sigma_algebra (sp,sts) ∧ IMAGE A X ⊆ sts ∧ countable X ⇒
          BIGUNION {A x | x ∈ X} ∈ sts
   
   [SIGMA_ALGEBRA_COUNTABLE_UNION]  Theorem
      
      ⊢ ∀a c.
          sigma_algebra a ∧ countable c ∧ c ⊆ subsets a ⇒
          BIGUNION c ∈ subsets a
   
   [SIGMA_ALGEBRA_DIFF]  Theorem
      
      ⊢ ∀a s t.
          sigma_algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒
          s DIFF t ∈ subsets a
   
   [SIGMA_ALGEBRA_EMPTY]  Theorem
      
      ⊢ ∀a. sigma_algebra a ⇒ ∅ ∈ 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_IMP_DYNKIN_SYSTEM]  Theorem
      
      ⊢ ∀a. sigma_algebra a ⇒ dynkin_system a
   
   [SIGMA_ALGEBRA_INTER]  Theorem
      
      ⊢ ∀a s t.
          sigma_algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒
          s ∩ t ∈ subsets a
   
   [SIGMA_ALGEBRA_PROD_SIGMA]  Theorem
      
      ⊢ ∀a b.
          subset_class (space a) (subsets a) ∧
          subset_class (space b) (subsets b) ⇒
          sigma_algebra (a × b)
   
   [SIGMA_ALGEBRA_PROD_SIGMA']  Theorem
      
      ⊢ ∀X Y A B.
          subset_class X A ∧ subset_class Y B ⇒
          sigma_algebra ((X,A) × (Y,B))
   
   [SIGMA_ALGEBRA_RESTRICT]  Theorem
      
      ⊢ ∀sp sts a.
          sigma_algebra (sp,sts) ∧ a ∈ sts ⇒
          sigma_algebra (a,IMAGE (λs. s ∩ a) sts)
   
   [SIGMA_ALGEBRA_RESTRICT_SUBSET]  Theorem
      
      ⊢ ∀sp sts a.
          sigma_algebra (sp,sts) ∧ a ∈ sts ⇒ IMAGE (λs. s ∩ a) sts ⊆ sts
   
   [SIGMA_ALGEBRA_SIGMA]  Theorem
      
      ⊢ ∀sp sts. subset_class sp sts ⇒ sigma_algebra (sigma sp sts)
   
   [SIGMA_ALGEBRA_SPACE]  Theorem
      
      ⊢ ∀a. sigma_algebra a ⇒ space a ∈ subsets a
   
   [SIGMA_ALGEBRA_UNION]  Theorem
      
      ⊢ ∀a s t.
          sigma_algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒
          s ∪ t ∈ subsets a
   
   [SIGMA_CONG]  Theorem
      
      ⊢ ∀sp a b.
          subsets (sigma sp a) = subsets (sigma sp b) ⇒
          sigma sp a = sigma sp b
   
   [SIGMA_MEASURABLE]  Theorem
      
      ⊢ ∀sp A f.
          sigma_algebra A ∧ f ∈ (sp → space A) ⇒
          f ∈ measurable (sigma sp A f) A
   
   [SIGMA_MONOTONE]  Theorem
      
      ⊢ ∀sp a b. a ⊆ b ⇒ subsets (sigma sp a) ⊆ subsets (sigma sp b)
   
   [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)) ∧
               (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
               BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
          subsets (sigma sp a) ⊆ p
   
   [SIGMA_PROPERTY_DISJOINT_LEMMA]  Theorem
      
      ⊢ ∀sp a d.
          algebra (sp,a) ∧ a ⊆ d ∧ dynkin_system (sp,d) ⇒
          subsets (sigma sp a) ⊆ d
   
   [SIGMA_PROPERTY_DISJOINT_LEMMA1]  Theorem
      
      ⊢ ∀sp sts.
          algebra (sp,sts) ⇒
          ∀s t.
            s ∈ sts ∧ t ∈ subsets (dynkin sp sts) ⇒
            s ∩ t ∈ subsets (dynkin sp sts)
   
   [SIGMA_PROPERTY_DISJOINT_LEMMA2]  Theorem
      
      ⊢ ∀sp sts.
          algebra (sp,sts) ⇒
          ∀s t.
            s ∈ subsets (dynkin sp sts) ∧ t ∈ subsets (dynkin sp sts) ⇒
            s ∩ t ∈ subsets (dynkin sp sts)
   
   [SIGMA_PROPERTY_DISJOINT_WEAK]  Theorem
      
      ⊢ ∀sp p a.
          subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
          (∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
          (∀s t. s ∈ p ∧ t ∈ p ⇒ s ∪ t ∈ 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_WEAK_ALT]  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_SIMULTANEOUSLY_MEASURABLE]  Theorem
      
      ⊢ ∀sp A f J.
          (∀i. i ∈ J ⇒ sigma_algebra (A i)) ∧
          (∀i. f i ∈ (sp → space (A i))) ⇒
          ∀i. i ∈ J ⇒ f i ∈ measurable (sigma sp A f J) (A i)
   
   [SIGMA_SMALLEST]  Theorem
      
      ⊢ ∀sp sts A.
          sts ⊆ A ∧ A ⊆ subsets (sigma sp sts) ∧ sigma_algebra (sp,A) ⇒
          A = subsets (sigma sp sts)
   
   [SIGMA_STABLE]  Theorem
      
      ⊢ ∀a. sigma_algebra a ⇒ sigma (space a) (subsets a) = a
   
   [SIGMA_STABLE_LEMMA]  Theorem
      
      ⊢ ∀sp sts. sigma_algebra (sp,sts) ⇒ sigma sp sts = (sp,sts)
   
   [SIGMA_SUBSET]  Theorem
      
      ⊢ ∀a b.
          sigma_algebra b ∧ a ⊆ subsets b ⇒
          subsets (sigma (space b) a) ⊆ subsets b
   
   [SIGMA_SUBSET_SUBSETS]  Theorem
      
      ⊢ ∀sp a. a ⊆ subsets (sigma sp a)
   
   [SMALLEST_RING]  Theorem
      
      ⊢ ∀sp sts. subset_class sp sts ⇒ ring (smallest_ring sp sts)
   
   [SMALLEST_RING_OF_SEMIRING]  Theorem
      
      ⊢ ∀sp sts.
          semiring (sp,sts) ⇒
          subsets (smallest_ring sp sts) =
          {BIGUNION c | c ⊆ sts ∧ FINITE c ∧ disjoint c}
   
   [SMALLEST_RING_SUBSET_SUBSETS]  Theorem
      
      ⊢ ∀sp a. a ⊆ subsets (smallest_ring sp a)
   
   [SPACE]  Theorem
      
      ⊢ ∀a. (space a,subsets a) = a
   
   [SPACE_DYNKIN]  Theorem
      
      ⊢ ∀sp sts. space (dynkin sp sts) = sp
   
   [SPACE_PROD_SIGMA]  Theorem
      
      ⊢ ∀a b. space (a × b) = space a × space b
   
   [SPACE_SIGMA]  Theorem
      
      ⊢ ∀sp a. space (sigma sp a) = sp
   
   [SPACE_SMALLEST_RING]  Theorem
      
      ⊢ ∀sp sts. space (smallest_ring sp sts) = sp
   
   [UNIV_SIGMA_ALGEBRA]  Theorem
      
      ⊢ sigma_algebra (𝕌(:α),𝕌(:α -> bool))
   
   [algebra_alt]  Theorem
      
      ⊢ ∀sp sts. algebra (sp,sts) ⇔ ring (sp,sts) ∧ sp ∈ sts
   
   [algebra_alt_inter]  Theorem
      
      ⊢ ∀sp sts.
          algebra (sp,sts) ⇔
          sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀a. a ∈ sts ⇒ sp DIFF a ∈ sts) ∧
          ∀a b. a ∈ sts ∧ b ∈ sts ⇒ a ∩ b ∈ sts
   
   [algebra_alt_union]  Theorem
      
      ⊢ ∀sp sts.
          algebra (sp,sts) ⇔
          sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀a. a ∈ sts ⇒ sp DIFF a ∈ sts) ∧
          ∀a b. a ∈ sts ∧ b ∈ sts ⇒ a ∪ b ∈ sts
   
   [prod_sigma_alt_sigma_functions]  Theorem
      
      ⊢ ∀A B.
          sigma_algebra A ∧ sigma_algebra B ⇒
          A × B =
          sigma (space A × space B) (binary A B) (binary FST SND) {0; 1}
   
   [ring_alt]  Theorem
      
      ⊢ ring (sp,sts) ⇔
        subset_class sp sts ∧ ∅ ∈ sts ∧
        (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∪ t ∈ sts) ∧
        ∀s t. s ∈ sts ∧ t ∈ sts ⇒ s DIFF t ∈ sts
   
   [ring_alt_pow]  Theorem
      
      ⊢ ∀sp sts.
          ring (sp,sts) ⇔
          sts ⊆ POW sp ∧ ∅ ∈ sts ∧
          (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∪ t ∈ sts) ∧
          ∀s t. s ∈ sts ∧ t ∈ sts ⇒ s DIFF t ∈ sts
   
   [ring_alt_pow_imp]  Theorem
      
      ⊢ ∀sp sts.
          sts ⊆ POW sp ∧ ∅ ∈ sts ∧
          (∀a b. a ∈ sts ∧ b ∈ sts ⇒ a ∪ b ∈ sts) ∧
          (∀a b. a ∈ sts ∧ b ∈ sts ⇒ a DIFF b ∈ sts) ⇒
          ring (sp,sts)
   
   [ring_and_semiring]  Theorem
      
      ⊢ ∀r. ring r ⇔
            semiring r ∧
            ∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∪ t ∈ subsets r
   
   [ring_disjointed_sets]  Theorem
      
      ⊢ ∀sp sts A.
          ring (sp,sts) ∧ IMAGE A 𝕌(:num) ⊆ sts ⇒
          IMAGE (λn. disjointed A n) 𝕌(:num) ⊆ sts
   
   [semiring_alt]  Theorem
      
      ⊢ semiring (sp,sts) ⇔
        subset_class sp sts ∧ ∅ ∈ sts ∧
        (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
        ∀s t.
          s ∈ sts ∧ t ∈ sts ⇒
          ∃c. c ⊆ sts ∧ FINITE c ∧ disjoint c ∧ s DIFF t = BIGUNION c
   
   [sigma_algebra_alt]  Theorem
      
      ⊢ ∀sp sts.
          sigma_algebra (sp,sts) ⇔
          algebra (sp,sts) ∧
          ∀A. IMAGE A 𝕌(:num) ⊆ sts ⇒ BIGUNION {A i | i ∈ 𝕌(:num)} ∈ sts
   
   [sigma_algebra_alt_pow]  Theorem
      
      ⊢ ∀sp sts.
          sigma_algebra (sp,sts) ⇔
          sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀s. s ∈ sts ⇒ sp DIFF s ∈ sts) ∧
          ∀A. IMAGE A 𝕌(:num) ⊆ sts ⇒ BIGUNION {A i | i ∈ 𝕌(:num)} ∈ sts
   
   [sigma_algebra_sigma_sets]  Theorem
      
      ⊢ ∀sp st. st ⊆ POW sp ⇒ sigma_algebra (sp,sigma_sets sp st)
   
   [sigma_sets_BIGINTER]  Theorem
      
      ⊢ ∀sp st A.
          st ⊆ POW sp ⇒
          (∀i. A i ∈ sigma_sets sp st) ⇒
          BIGINTER {A i | i ∈ 𝕌(:num)} ∈ sigma_sets sp st
   
   [sigma_sets_BIGINTER2]  Theorem
      
      ⊢ ∀sp st A N.
          st ⊆ POW sp ∧ (∀i. i ∈ N ⇒ A i ∈ sigma_sets sp st) ∧ N ≠ ∅ ⇒
          BIGINTER {A i | i ∈ N} ∈ sigma_sets sp st
   
   [sigma_sets_BIGUNION]  Theorem
      
      ⊢ ∀sp st A.
          (∀i. A i ∈ sigma_sets sp st) ⇒
          BIGUNION {A i | i ∈ 𝕌(:num)} ∈ sigma_sets sp st
   
   [sigma_sets_basic]  Theorem
      
      ⊢ ∀sp st a. a ∈ st ⇒ a ∈ sigma_sets sp st
   
   [sigma_sets_cases]  Theorem
      
      ⊢ ∀sp st a0.
          sigma_sets sp st a0 ⇔
          a0 = ∅ ∨ st a0 ∨ (∃a. a0 = sp DIFF a ∧ sigma_sets sp st a) ∨
          ∃A. a0 = BIGUNION {A i | i ∈ 𝕌(:num)} ∧
              ∀i. sigma_sets sp st (A i)
   
   [sigma_sets_compl]  Theorem
      
      ⊢ ∀sp st a. a ∈ sigma_sets sp st ⇒ sp DIFF a ∈ sigma_sets sp st
   
   [sigma_sets_empty]  Theorem
      
      ⊢ ∀sp st. ∅ ∈ sigma_sets sp st
   
   [sigma_sets_fixpoint]  Theorem
      
      ⊢ ∀sp sts. sigma_algebra (sp,sts) ⇒ sigma_sets sp sts = sts
   
   [sigma_sets_ind]  Theorem
      
      ⊢ ∀sp st sigma_sets'.
          sigma_sets' ∅ ∧ (∀a. st a ⇒ sigma_sets' a) ∧
          (∀a. sigma_sets' a ⇒ sigma_sets' (sp DIFF a)) ∧
          (∀A. (∀i. sigma_sets' (A i)) ⇒
               sigma_sets' (BIGUNION {A i | i ∈ 𝕌(:num)})) ⇒
          ∀a0. sigma_sets sp st a0 ⇒ sigma_sets' a0
   
   [sigma_sets_into_sp]  Theorem
      
      ⊢ ∀sp st. st ⊆ POW sp ⇒ ∀x. x ∈ sigma_sets sp st ⇒ x ⊆ sp
   
   [sigma_sets_least_sigma_algebra]  Theorem
      
      ⊢ ∀sp A.
          A ⊆ POW sp ⇒
          sigma_sets sp A = BIGINTER {B | A ⊆ B ∧ sigma_algebra (sp,B)}
   
   [sigma_sets_rules]  Theorem
      
      ⊢ ∀sp st.
          sigma_sets sp st ∅ ∧ (∀a. st a ⇒ sigma_sets sp st a) ∧
          (∀a. sigma_sets sp st a ⇒ sigma_sets sp st (sp DIFF a)) ∧
          ∀A. (∀i. sigma_sets sp st (A i)) ⇒
              sigma_sets sp st (BIGUNION {A i | i ∈ 𝕌(:num)})
   
   [sigma_sets_strongind]  Theorem
      
      ⊢ ∀sp st sigma_sets'.
          sigma_sets' ∅ ∧ (∀a. st a ⇒ sigma_sets' a) ∧
          (∀a. sigma_sets sp st a ∧ sigma_sets' a ⇒ sigma_sets' (sp DIFF a)) ∧
          (∀A. (∀i. sigma_sets sp st (A i) ∧ sigma_sets' (A i)) ⇒
               sigma_sets' (BIGUNION {A i | i ∈ 𝕌(:num)})) ⇒
          ∀a0. sigma_sets sp st a0 ⇒ sigma_sets' a0
   
   [sigma_sets_subset]  Theorem
      
      ⊢ ∀sp sts st.
          sigma_algebra (sp,sts) ∧ st ⊆ sts ⇒ sigma_sets sp st ⊆ sts
   
   [sigma_sets_superset_generator]  Theorem
      
      ⊢ ∀X A. A ⊆ sigma_sets X A
   
   [sigma_sets_top]  Theorem
      
      ⊢ ∀sp A. sp ∈ sigma_sets sp A
   
   [sigma_sets_union]  Theorem
      
      ⊢ ∀sp st a b.
          a ∈ sigma_sets sp st ∧ b ∈ sigma_sets sp st ⇒
          a ∪ b ∈ sigma_sets sp st
   
   [subset_class_POW]  Theorem
      
      ⊢ ∀sp. subset_class sp (POW sp)
   
   
*)
end

HOL 4, Kananaskis-14