Structure borelTheory

signature borelTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val AE_def : thm
    val Borel : thm
    val almost_everywhere_def : thm
    val ext_lborel_def : thm
    val fn_minus_def : thm
    val fn_plus_def : thm
    val indicator_fn_def : thm
    val lambda0_def : thm
    val lborel_def : thm
    val lebesgue_def : thm
    val nonneg_def : thm
    val set_liminf_def : thm
    val set_limsup_def : thm
  
  (*  Theorems  *)
    val AE_ALT : thm
    val AE_I : thm
    val AE_IMP_MEASURABLE_SETS : thm
    val AE_NOT_IN : thm
    val AE_THM : thm
    val AE_all_S : thm
    val AE_all_countable : thm
    val AE_default : thm
    val AE_filter : thm
    val AE_iff_measurable : thm
    val AE_iff_null : thm
    val AE_iff_null_sets : thm
    val AE_impl : thm
    val AE_not_in : thm
    val BOREL_MEASURABLE_INFINITY : 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 BOREL_MEASURABLE_SETS_CC : thm
    val BOREL_MEASURABLE_SETS_CO : thm
    val BOREL_MEASURABLE_SETS_CR : thm
    val BOREL_MEASURABLE_SETS_FINITE : thm
    val BOREL_MEASURABLE_SETS_NOT_SING : thm
    val BOREL_MEASURABLE_SETS_OC : thm
    val BOREL_MEASURABLE_SETS_OO : thm
    val BOREL_MEASURABLE_SETS_OR : thm
    val BOREL_MEASURABLE_SETS_RC : thm
    val BOREL_MEASURABLE_SETS_RO : thm
    val BOREL_MEASURABLE_SETS_SING : thm
    val BOREL_MEASURABLE_SETS_SING' : thm
    val Borel_def : thm
    val Borel_eq_ge : thm
    val Borel_eq_gr : thm
    val Borel_eq_le : thm
    val FN_ABS : thm
    val FN_ABS' : thm
    val FN_DECOMP : thm
    val FN_DECOMP' : thm
    val FN_MINUS_ABS_ZERO : thm
    val FN_MINUS_ADD_LE : thm
    val FN_MINUS_ALT : thm
    val FN_MINUS_ALT' : thm
    val FN_MINUS_CMUL : thm
    val FN_MINUS_CMUL_full : thm
    val FN_MINUS_FMUL : thm
    val FN_MINUS_INFTY_IMP : thm
    val FN_MINUS_LE_ABS : thm
    val FN_MINUS_NOT_INFTY : thm
    val FN_MINUS_NOT_INFTY' : thm
    val FN_MINUS_POS : thm
    val FN_MINUS_POS_ZERO : thm
    val FN_MINUS_REDUCE : thm
    val FN_MINUS_TO_PLUS : thm
    val FN_MINUS_ZERO : thm
    val FN_PLUS_ABS_SELF : thm
    val FN_PLUS_ADD_LE : thm
    val FN_PLUS_ALT : thm
    val FN_PLUS_ALT' : thm
    val FN_PLUS_CMUL : thm
    val FN_PLUS_CMUL_full : thm
    val FN_PLUS_FMUL : thm
    val FN_PLUS_INFTY_IMP : thm
    val FN_PLUS_LE_ABS : thm
    val FN_PLUS_NEG_ZERO : thm
    val FN_PLUS_NOT_INFTY : thm
    val FN_PLUS_NOT_INFTY' : thm
    val FN_PLUS_POS : thm
    val FN_PLUS_POS_ID : thm
    val FN_PLUS_REDUCE : thm
    val FN_PLUS_TO_MINUS : thm
    val FN_PLUS_ZERO : thm
    val FORALL_IMP_AE : thm
    val INDICATOR_FN_ABS : thm
    val INDICATOR_FN_ABS_MUL : thm
    val INDICATOR_FN_CROSS : thm
    val INDICATOR_FN_DIFF : thm
    val INDICATOR_FN_DIFF_SPACE : thm
    val INDICATOR_FN_EMPTY : thm
    val INDICATOR_FN_FCP_CROSS : thm
    val INDICATOR_FN_INTER : thm
    val INDICATOR_FN_INTER_MIN : thm
    val INDICATOR_FN_LE_1 : thm
    val INDICATOR_FN_MONO : thm
    val INDICATOR_FN_MUL_INTER : thm
    val INDICATOR_FN_NOT_INFTY : thm
    val INDICATOR_FN_POS : thm
    val INDICATOR_FN_SING_0 : thm
    val INDICATOR_FN_SING_1 : thm
    val INDICATOR_FN_UNION : thm
    val INDICATOR_FN_UNION_MAX : thm
    val INDICATOR_FN_UNION_MIN : thm
    val IN_LIMINF : thm
    val IN_LIMSUP : thm
    val IN_MEASURABLE_BOREL : thm
    val IN_MEASURABLE_BOREL_2D_FUNCTION : thm
    val IN_MEASURABLE_BOREL_2D_VECTOR : thm
    val IN_MEASURABLE_BOREL_ABS : thm
    val IN_MEASURABLE_BOREL_ABS' : thm
    val IN_MEASURABLE_BOREL_ADD : thm
    val IN_MEASURABLE_BOREL_ADD' : thm
    val IN_MEASURABLE_BOREL_AE_EQ : thm
    val IN_MEASURABLE_BOREL_ALL : thm
    val IN_MEASURABLE_BOREL_ALL_MEASURE : thm
    val IN_MEASURABLE_BOREL_ALT1 : thm
    val IN_MEASURABLE_BOREL_ALT1_IMP : thm
    val IN_MEASURABLE_BOREL_ALT2 : thm
    val IN_MEASURABLE_BOREL_ALT2_IMP : thm
    val IN_MEASURABLE_BOREL_ALT3 : thm
    val IN_MEASURABLE_BOREL_ALT3_IMP : thm
    val IN_MEASURABLE_BOREL_ALT4 : thm
    val IN_MEASURABLE_BOREL_ALT4_IMP : thm
    val IN_MEASURABLE_BOREL_ALT5 : thm
    val IN_MEASURABLE_BOREL_ALT5_IMP : thm
    val IN_MEASURABLE_BOREL_ALT6 : thm
    val IN_MEASURABLE_BOREL_ALT6_IMP : thm
    val IN_MEASURABLE_BOREL_ALT7 : thm
    val IN_MEASURABLE_BOREL_ALT7_IMP : thm
    val IN_MEASURABLE_BOREL_ALT8 : thm
    val IN_MEASURABLE_BOREL_ALT9 : thm
    val IN_MEASURABLE_BOREL_BOREL_ABS : thm
    val IN_MEASURABLE_BOREL_BOREL_I : thm
    val IN_MEASURABLE_BOREL_CC : thm
    val IN_MEASURABLE_BOREL_CMUL : thm
    val IN_MEASURABLE_BOREL_CMUL_INDICATOR : thm
    val IN_MEASURABLE_BOREL_CMUL_INDICATOR' : thm
    val IN_MEASURABLE_BOREL_CO : thm
    val IN_MEASURABLE_BOREL_CONST : thm
    val IN_MEASURABLE_BOREL_CONST' : thm
    val IN_MEASURABLE_BOREL_CR : thm
    val IN_MEASURABLE_BOREL_EQ : thm
    val IN_MEASURABLE_BOREL_EQ' : thm
    val IN_MEASURABLE_BOREL_FN_MINUS : thm
    val IN_MEASURABLE_BOREL_FN_PLUS : thm
    val IN_MEASURABLE_BOREL_IMP : thm
    val IN_MEASURABLE_BOREL_IMP_BOREL : thm
    val IN_MEASURABLE_BOREL_IMP_BOREL' : 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_MAXIMAL : thm
    val IN_MEASURABLE_BOREL_MIN : thm
    val IN_MEASURABLE_BOREL_MINIMAL : thm
    val IN_MEASURABLE_BOREL_MINUS : 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_NOT_NEGINF : thm
    val IN_MEASURABLE_BOREL_NOT_POSINF : thm
    val IN_MEASURABLE_BOREL_NOT_SING : thm
    val IN_MEASURABLE_BOREL_OC : thm
    val IN_MEASURABLE_BOREL_OO : thm
    val IN_MEASURABLE_BOREL_OR : thm
    val IN_MEASURABLE_BOREL_PLUS_MINUS : thm
    val IN_MEASURABLE_BOREL_POSINF : thm
    val IN_MEASURABLE_BOREL_POW : thm
    val IN_MEASURABLE_BOREL_RC : thm
    val IN_MEASURABLE_BOREL_RO : thm
    val IN_MEASURABLE_BOREL_SING : thm
    val IN_MEASURABLE_BOREL_SQR : thm
    val IN_MEASURABLE_BOREL_SUB : thm
    val IN_MEASURABLE_BOREL_SUB' : thm
    val IN_MEASURABLE_BOREL_SUM : thm
    val IN_MEASURABLE_BOREL_SUMINF : thm
    val IN_MEASURABLE_BOREL_TIMES : thm
    val IN_MEASURABLE_BOREL_TIMES' : thm
    val MEASURABLE_BOREL : thm
    val MEASURE_SPACE_LBOREL : thm
    val SIGMA_ALGEBRA_BOREL : thm
    val SIGMA_ALGEBRA_BOREL_2D : thm
    val SIGMA_FINITE_LBOREL : thm
    val SPACE_BOREL : thm
    val SPACE_BOREL_2D : thm
    val absolutely_integrable_on_indicator : thm
    val borel_eq_real_set : thm
    val borel_imp_lebesgue_measurable : thm
    val borel_imp_lebesgue_sets : thm
    val countably_additive_lebesgue : thm
    val fn_minus : thm
    val fn_minus_mul_indicator : thm
    val fn_plus : thm
    val fn_plus_mul_indicator : thm
    val has_integral_indicator_UNIV : thm
    val has_integral_interval_cube : thm
    val in_borel_measurable_continuous_on : thm
    val in_borel_measurable_from_Borel : thm
    val in_borel_measurable_imp : thm
    val in_measurable_sigma_pow : thm
    val in_sets_lebesgue : thm
    val in_sets_lebesgue_imp : thm
    val indicator_fn_general_cross : thm
    val indicator_fn_normal : thm
    val indicator_fn_split : thm
    val indicator_fn_suminf : thm
    val integrable_indicator_UNIV : thm
    val integral_indicator_UNIV : thm
    val integral_one : thm
    val lambda0_empty : thm
    val lambda0_not_infty : thm
    val lambda_closed_interval : thm
    val lambda_closed_interval_content : thm
    val lambda_empty : thm
    val lambda_eq : thm
    val lambda_eq_lebesgue : thm
    val lambda_not_infty : thm
    val lambda_open_interval : thm
    val lambda_prop : thm
    val lambda_sing : thm
    val lborel0_additive : thm
    val lborel0_finite_additive : thm
    val lborel0_positive : thm
    val lborel0_premeasure : thm
    val lborel0_subadditive : thm
    val lborel_subset_lebesgue : thm
    val lebesgue_closed_interval : thm
    val lebesgue_closed_interval_content : thm
    val lebesgue_empty : thm
    val lebesgue_eq_lambda : thm
    val lebesgue_measure_iff_LIMSEQ : thm
    val lebesgue_of_negligible : thm
    val lebesgue_open_interval : thm
    val lebesgue_sing : thm
    val liminf_limsup : thm
    val liminf_limsup_sp : thm
    val limseq_indicator_BIGUNION : thm
    val limsup_suminf_indicator : thm
    val limsup_suminf_indicator_space : thm
    val m_space_lborel : thm
    val measure_lebesgue : thm
    val measure_liminf : thm
    val measure_limsup : thm
    val measure_limsup_finite : thm
    val measure_space_lborel : thm
    val measure_space_lebesgue : thm
    val negligible_in_lebesgue : thm
    val nonneg_abs : thm
    val nonneg_fn_abs : thm
    val nonneg_fn_minus : thm
    val nonneg_fn_plus : thm
    val positive_lebesgue : thm
    val seq_le_imp_lim_le : thm
    val seq_mono_le : thm
    val set_limsup_alt : thm
    val sets_lborel : thm
    val sets_lebesgue : thm
    val sigma_algebra_lebesgue : thm
    val sigma_finite_lborel : thm
    val space_lborel : thm
    val space_lebesgue : thm
    val sup_sequence : thm
  
  val borel_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [measure] Parent theory of "borel"
   
   [real_borel] Parent theory of "borel"
   
   [AE_def]  Definition
      
      ⊢ $AE = (λP. almost_everywhere lebesgue P)
   
   [Borel]  Definition
      
      ⊢ Borel =
        (𝕌(:extreal),
         {B' |
          ∃B S.
            B' = IMAGE Normal B ∪ S ∧ B ∈ subsets borel ∧
            S ∈ {∅; {−∞}; {+∞}; {−∞; +∞}}})
   
   [almost_everywhere_def]  Definition
      
      ⊢ ∀m P.
          almost_everywhere m P ⇔
          ∃N. null_set m N ∧ ∀x. x ∈ m_space m DIFF N ⇒ P x
   
   [ext_lborel_def]  Definition
      
      ⊢ ext_lborel = (space Borel,subsets Borel,lambda ∘ real_set)
   
   [fn_minus_def]  Definition
      
      ⊢ ∀f. f⁻ = (λx. if f x < 0 then -f x else 0)
   
   [fn_plus_def]  Definition
      
      ⊢ ∀f. f⁺ = (λx. if 0 < f x then f x else 0)
   
   [indicator_fn_def]  Definition
      
      ⊢ ∀s. 𝟙 s = (λx. if x ∈ s then 1 else 0)
   
   [lambda0_def]  Definition
      
      ⊢ ∀a b. a ≤ b ⇒ lambda0 (right_open_interval a b) = Normal (b − a)
   
   [lborel_def]  Definition
      
      ⊢ (∀s. s ∈ subsets right_open_intervals ⇒ lambda s = lambda0 s) ∧
        (m_space lborel,measurable_sets lborel) = borel ∧
        measure_space lborel
   
   [lebesgue_def]  Definition
      
      ⊢ lebesgue =
        (𝕌(:real),{A | ∀n. indicator A integrable_on line n},
         (λA. sup {Normal (integral (line n) (indicator A)) | n ∈ 𝕌(:num)}))
   
   [nonneg_def]  Definition
      
      ⊢ ∀f. nonneg f ⇔ ∀x. 0 ≤ f x
   
   [set_liminf_def]  Definition
      
      ⊢ ∀E. liminf E =
            BIGUNION (IMAGE (λm. BIGINTER {E n | m ≤ n}) 𝕌(:num))
   
   [set_limsup_def]  Definition
      
      ⊢ ∀E. limsup E =
            BIGINTER (IMAGE (λm. BIGUNION {E n | m ≤ n}) 𝕌(:num))
   
   [AE_ALT]  Theorem
      
      ⊢ ∀m P.
          (AE x::m. P x) ⇔
          ∃N. null_set m N ∧ {x | x ∈ m_space m ∧ ¬P x} ⊆ N
   
   [AE_I]  Theorem
      
      ⊢ ∀N M P.
          null_set M N ⇒ {x | x ∈ m_space M ∧ ¬P x} ⊆ N ⇒ AE x::M. P x
   
   [AE_IMP_MEASURABLE_SETS]  Theorem
      
      ⊢ ∀m P.
          complete_measure_space m ∧ (AE x::m. P x) ⇒
          {x | x ∈ m_space m ∧ P x} ∈ measurable_sets m
   
   [AE_NOT_IN]  Theorem
      
      ⊢ ∀N M. null_set M N ⇒ AE x::M. x ∉ N
   
   [AE_THM]  Theorem
      
      ⊢ ∀m P. (AE x::m. P x) ⇔ almost_everywhere m P
   
   [AE_all_S]  Theorem
      
      ⊢ ∀M S' P.
          measure_space M ⇒
          (∀i. S' i ⇒ AE x::M. (λx. P i x) x) ⇒
          ∀i'. AE x::M. (λx. S' i' ⇒ P i' x) x
   
   [AE_all_countable]  Theorem
      
      ⊢ ∀t M P.
          measure_space M ⇒
          ((∀i. COUNTABLE (t i) ⇒ AE x::M. (λx. P i x) x) ⇔
           ∀i. AE x::M. (λx. P i x) x)
   
   [AE_default]  Theorem
      
      ⊢ ∀P. (AE x. P x) ⇔ AE x::lebesgue. P x
   
   [AE_filter]  Theorem
      
      ⊢ ∀m P.
          (AE x::m. P x) ⇔
          ∃N. N ∈ null_set m ∧ {x | x ∈ m_space m ∧ x ∉ P} ⊆ N
   
   [AE_iff_measurable]  Theorem
      
      ⊢ ∀N M P.
          measure_space M ∧ N ∈ measurable_sets M ⇒
          {x | x ∈ m_space M ∧ ¬P x} = N ⇒
          ((AE x::M. P x) ⇔ measure M N = 0)
   
   [AE_iff_null]  Theorem
      
      ⊢ ∀M P.
          measure_space M ∧ {x | x ∈ m_space M ∧ ¬P x} ∈ measurable_sets M ⇒
          ((AE x::M. P x) ⇔ null_set M {x | x ∈ m_space M ∧ ¬P x})
   
   [AE_iff_null_sets]  Theorem
      
      ⊢ ∀N M.
          measure_space M ∧ N ∈ measurable_sets M ⇒
          (null_set M N ⇔ AE x::M. {x | ¬N x} x)
   
   [AE_impl]  Theorem
      
      ⊢ ∀P M Q.
          measure_space M ⇒ (P ⇒ AE x::M. Q x) ⇒ AE x::M. (λx. P ⇒ Q x) x
   
   [AE_not_in]  Theorem
      
      ⊢ ∀N M. null_set M N ⇒ AE x::M. {x | ¬N x} x
   
   [BOREL_MEASURABLE_INFINITY]  Theorem
      
      ⊢ {+∞} ∈ subsets Borel ∧ {−∞} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS]  Theorem
      
      ⊢ (∀c. {x | x < c} ∈ subsets Borel) ∧
        (∀c. {x | c < x} ∈ subsets Borel) ∧
        (∀c. {x | x ≤ c} ∈ subsets Borel) ∧
        (∀c. {x | c ≤ x} ∈ 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
   
   [BOREL_MEASURABLE_SETS_CC]  Theorem
      
      ⊢ ∀c d. {x | c ≤ x ∧ x ≤ d} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_CO]  Theorem
      
      ⊢ ∀c d. {x | c ≤ x ∧ x < d} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_CR]  Theorem
      
      ⊢ ∀c. {x | c ≤ x} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_FINITE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ s ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_NOT_SING]  Theorem
      
      ⊢ ∀c. {x | x ≠ c} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_OC]  Theorem
      
      ⊢ ∀c d. {x | c < x ∧ x ≤ d} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_OO]  Theorem
      
      ⊢ ∀c d. {x | c < x ∧ x < d} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_OR]  Theorem
      
      ⊢ ∀c. {x | c < x} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_RC]  Theorem
      
      ⊢ ∀c. {x | x ≤ c} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_RO]  Theorem
      
      ⊢ ∀c. {x | x < c} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_SING]  Theorem
      
      ⊢ ∀c. {c} ∈ subsets Borel
   
   [BOREL_MEASURABLE_SETS_SING']  Theorem
      
      ⊢ ∀c. {x | x = c} ∈ subsets Borel
   
   [Borel_def]  Theorem
      
      ⊢ Borel = sigma 𝕌(:extreal) (IMAGE (λa. {x | x < Normal a}) 𝕌(:real))
   
   [Borel_eq_ge]  Theorem
      
      ⊢ Borel = sigma 𝕌(:extreal) (IMAGE (λa. {x | Normal a ≤ x}) 𝕌(:real))
   
   [Borel_eq_gr]  Theorem
      
      ⊢ Borel = sigma 𝕌(:extreal) (IMAGE (λa. {x | Normal a < x}) 𝕌(:real))
   
   [Borel_eq_le]  Theorem
      
      ⊢ Borel = sigma 𝕌(:extreal) (IMAGE (λa. {x | x ≤ Normal a}) 𝕌(:real))
   
   [FN_ABS]  Theorem
      
      ⊢ ∀f x. (abs ∘ f) x = f⁺ x + f⁻ x
   
   [FN_ABS']  Theorem
      
      ⊢ ∀f. abs ∘ f = (λx. f⁺ x + f⁻ x)
   
   [FN_DECOMP]  Theorem
      
      ⊢ ∀f x. f x = f⁺ x − f⁻ x
   
   [FN_DECOMP']  Theorem
      
      ⊢ ∀f. f = (λx. f⁺ x − f⁻ x)
   
   [FN_MINUS_ABS_ZERO]  Theorem
      
      ⊢ ∀f. (abs ∘ f)⁻ = (λx. 0)
   
   [FN_MINUS_ADD_LE]  Theorem
      
      ⊢ ∀f g x.
          f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞ ⇒
          (λx. f x + g x)⁻ x ≤ f⁻ x + g⁻ x
   
   [FN_MINUS_ALT]  Theorem
      
      ⊢ ∀f. f⁻ = (λx. -min (f x) 0)
   
   [FN_MINUS_ALT']  Theorem
      
      ⊢ ∀f. f⁻ = (λx. -min 0 (f x))
   
   [FN_MINUS_CMUL]  Theorem
      
      ⊢ ∀f c.
          (0 ≤ c ⇒ (λx. Normal c * f x)⁻ = (λx. Normal c * f⁻ x)) ∧
          (c ≤ 0 ⇒ (λx. Normal c * f x)⁻ = (λx. -Normal c * f⁺ x))
   
   [FN_MINUS_CMUL_full]  Theorem
      
      ⊢ ∀f c.
          (0 ≤ c ⇒ (λx. c * f x)⁻ = (λx. c * f⁻ x)) ∧
          (c ≤ 0 ⇒ (λx. c * f x)⁻ = (λx. -c * f⁺ x))
   
   [FN_MINUS_FMUL]  Theorem
      
      ⊢ ∀f c. (∀x. 0 ≤ c x) ⇒ (λx. c x * f x)⁻ = (λx. c x * f⁻ x)
   
   [FN_MINUS_INFTY_IMP]  Theorem
      
      ⊢ ∀f x. f⁻ x = +∞ ⇒ f⁺ x = 0
   
   [FN_MINUS_LE_ABS]  Theorem
      
      ⊢ ∀f x. f⁻ x ≤ abs (f x)
   
   [FN_MINUS_NOT_INFTY]  Theorem
      
      ⊢ ∀f. (∀x. f x ≠ −∞) ⇒ ∀x. f⁻ x ≠ +∞
   
   [FN_MINUS_NOT_INFTY']  Theorem
      
      ⊢ ∀f x. f x ≠ −∞ ⇒ f⁻ x ≠ +∞
   
   [FN_MINUS_POS]  Theorem
      
      ⊢ ∀g x. 0 ≤ g⁻ x
   
   [FN_MINUS_POS_ZERO]  Theorem
      
      ⊢ ∀g. (∀x. 0 ≤ g x) ⇒ g⁻ = (λx. 0)
   
   [FN_MINUS_REDUCE]  Theorem
      
      ⊢ ∀f x. 0 ≤ f x ⇒ f⁻ x = 0
   
   [FN_MINUS_TO_PLUS]  Theorem
      
      ⊢ ∀f. (λx. -f x)⁻ = f⁺
   
   [FN_MINUS_ZERO]  Theorem
      
      ⊢ (λx. 0)⁻ = (λx. 0)
   
   [FN_PLUS_ABS_SELF]  Theorem
      
      ⊢ ∀f. (abs ∘ f)⁺ = abs ∘ f
   
   [FN_PLUS_ADD_LE]  Theorem
      
      ⊢ ∀f g x. (λx. f x + g x)⁺ x ≤ f⁺ x + g⁺ x
   
   [FN_PLUS_ALT]  Theorem
      
      ⊢ ∀f. f⁺ = (λx. max (f x) 0)
   
   [FN_PLUS_ALT']  Theorem
      
      ⊢ ∀f. f⁺ = (λx. max 0 (f x))
   
   [FN_PLUS_CMUL]  Theorem
      
      ⊢ ∀f c.
          (0 ≤ c ⇒ (λx. Normal c * f x)⁺ = (λx. Normal c * f⁺ x)) ∧
          (c ≤ 0 ⇒ (λx. Normal c * f x)⁺ = (λx. -Normal c * f⁻ x))
   
   [FN_PLUS_CMUL_full]  Theorem
      
      ⊢ ∀f c.
          (0 ≤ c ⇒ (λx. c * f x)⁺ = (λx. c * f⁺ x)) ∧
          (c ≤ 0 ⇒ (λx. c * f x)⁺ = (λx. -c * f⁻ x))
   
   [FN_PLUS_FMUL]  Theorem
      
      ⊢ ∀f c. (∀x. 0 ≤ c x) ⇒ (λx. c x * f x)⁺ = (λx. c x * f⁺ x)
   
   [FN_PLUS_INFTY_IMP]  Theorem
      
      ⊢ ∀f x. f⁺ x = +∞ ⇒ f⁻ x = 0
   
   [FN_PLUS_LE_ABS]  Theorem
      
      ⊢ ∀f x. f⁺ x ≤ abs (f x)
   
   [FN_PLUS_NEG_ZERO]  Theorem
      
      ⊢ ∀g. (∀x. g x ≤ 0) ⇒ g⁺ = (λx. 0)
   
   [FN_PLUS_NOT_INFTY]  Theorem
      
      ⊢ ∀f. (∀x. f x ≠ +∞) ⇒ ∀x. f⁺ x ≠ +∞
   
   [FN_PLUS_NOT_INFTY']  Theorem
      
      ⊢ ∀f x. f x ≠ +∞ ⇒ f⁺ x ≠ +∞
   
   [FN_PLUS_POS]  Theorem
      
      ⊢ ∀g x. 0 ≤ g⁺ x
   
   [FN_PLUS_POS_ID]  Theorem
      
      ⊢ ∀g. (∀x. 0 ≤ g x) ⇒ g⁺ = g
   
   [FN_PLUS_REDUCE]  Theorem
      
      ⊢ ∀f x. 0 ≤ f x ⇒ f⁺ x = f x
   
   [FN_PLUS_TO_MINUS]  Theorem
      
      ⊢ ∀f. (λx. -f x)⁺ = f⁻
   
   [FN_PLUS_ZERO]  Theorem
      
      ⊢ (λx. 0)⁺ = (λx. 0)
   
   [FORALL_IMP_AE]  Theorem
      
      ⊢ ∀m P. measure_space m ∧ (∀x. x ∈ m_space m ⇒ P x) ⇒ AE x::m. P x
   
   [INDICATOR_FN_ABS]  Theorem
      
      ⊢ ∀s. abs ∘ 𝟙 s = 𝟙 s
   
   [INDICATOR_FN_ABS_MUL]  Theorem
      
      ⊢ ∀f s. abs ∘ (λx. f x * 𝟙 s x) = (λx. (abs ∘ f) x * 𝟙 s x)
   
   [INDICATOR_FN_CROSS]  Theorem
      
      ⊢ ∀s t x y. 𝟙 (s × t) (x,y) = 𝟙 s x * 𝟙 t y
   
   [INDICATOR_FN_DIFF]  Theorem
      
      ⊢ ∀A B. 𝟙 (A DIFF B) = (λt. 𝟙 A t − 𝟙 (A ∩ B) t)
   
   [INDICATOR_FN_DIFF_SPACE]  Theorem
      
      ⊢ ∀A B sp.
          A ⊆ sp ∧ B ⊆ sp ⇒ 𝟙 (A ∩ (sp DIFF B)) = (λt. 𝟙 A t − 𝟙 (A ∩ B) t)
   
   [INDICATOR_FN_EMPTY]  Theorem
      
      ⊢ ∀x. 𝟙 ∅ x = 0
   
   [INDICATOR_FN_FCP_CROSS]  Theorem
      
      ⊢ ∀s t x y.
          FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
          𝟙 (fcp_cross s t) (FCP_CONCAT x y) = 𝟙 s x * 𝟙 t y
   
   [INDICATOR_FN_INTER]  Theorem
      
      ⊢ ∀A B. 𝟙 (A ∩ B) = (λt. 𝟙 A t * 𝟙 B t)
   
   [INDICATOR_FN_INTER_MIN]  Theorem
      
      ⊢ ∀A B. 𝟙 (A ∩ B) = (λt. min (𝟙 A t) (𝟙 B t))
   
   [INDICATOR_FN_LE_1]  Theorem
      
      ⊢ ∀s x. 𝟙 s x ≤ 1
   
   [INDICATOR_FN_MONO]  Theorem
      
      ⊢ ∀s t x. s ⊆ t ⇒ 𝟙 s x ≤ 𝟙 t x
   
   [INDICATOR_FN_MUL_INTER]  Theorem
      
      ⊢ ∀A B. (λt. 𝟙 A t * 𝟙 B t) = (λt. 𝟙 (A ∩ B) t)
   
   [INDICATOR_FN_NOT_INFTY]  Theorem
      
      ⊢ ∀s x. 𝟙 s x ≠ −∞ ∧ 𝟙 s x ≠ +∞
   
   [INDICATOR_FN_POS]  Theorem
      
      ⊢ ∀s x. 0 ≤ 𝟙 s x
   
   [INDICATOR_FN_SING_0]  Theorem
      
      ⊢ ∀x y. x ≠ y ⇒ 𝟙 {x} y = 0
   
   [INDICATOR_FN_SING_1]  Theorem
      
      ⊢ ∀x y. x = y ⇒ 𝟙 {x} y = 1
   
   [INDICATOR_FN_UNION]  Theorem
      
      ⊢ ∀A B. 𝟙 (A ∪ B) = (λt. 𝟙 A t + 𝟙 B t − 𝟙 (A ∩ B) t)
   
   [INDICATOR_FN_UNION_MAX]  Theorem
      
      ⊢ ∀A B. 𝟙 (A ∪ B) = (λt. max (𝟙 A t) (𝟙 B t))
   
   [INDICATOR_FN_UNION_MIN]  Theorem
      
      ⊢ ∀A B. 𝟙 (A ∪ B) = (λt. min (𝟙 A t + 𝟙 B t) 1)
   
   [IN_LIMINF]  Theorem
      
      ⊢ ∀A x. x ∈ liminf A ⇔ ∃m. ∀n. m ≤ n ⇒ x ∈ A n
   
   [IN_LIMSUP]  Theorem
      
      ⊢ ∀A x. x ∈ limsup A ⇔ ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ x ∈ A n
   
   [IN_MEASURABLE_BOREL]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇔
          sigma_algebra a ∧ f ∈ (space a → 𝕌(:extreal)) ∧
          ∀c. {x | f x < Normal c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_2D_FUNCTION]  Theorem
      
      ⊢ ∀a X Y f.
          sigma_algebra a ∧ X ∈ Borel_measurable a ∧
          Y ∈ Borel_measurable a ∧ f ∈ Borel_measurable (Borel × Borel) ⇒
          (λx. f (X x,Y x)) ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_2D_VECTOR]  Theorem
      
      ⊢ ∀a X Y.
          sigma_algebra a ∧ X ∈ Borel_measurable a ∧ Y ∈ Borel_measurable a ⇒
          (λx. (X x,Y x)) ∈ measurable a (Borel × Borel)
   
   [IN_MEASURABLE_BOREL_ABS]  Theorem
      
      ⊢ ∀a f g.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          (∀x. x ∈ space a ⇒ g x = abs (f x)) ⇒
          g ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_ABS']  Theorem
      
      ⊢ ∀a f.
          sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
          abs ∘ f ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_ADD]  Theorem
      
      ⊢ ∀a f g h.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          g ∈ Borel_measurable a ∧
          (∀x. x ∈ space a ⇒ f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞) ∧
          (∀x. x ∈ space a ⇒ h x = f x + g x) ⇒
          h ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_ADD']  Theorem
      
      ⊢ ∀a f g h.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          g ∈ Borel_measurable a ∧ (∀x. x ∈ space a ⇒ h x = f x + g x) ⇒
          h ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_AE_EQ]  Theorem
      
      ⊢ ∀m f g.
          complete_measure_space m ∧ (AE x::m. f x = g x) ∧
          f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
          g ∈ Borel_measurable (m_space m,measurable_sets m)
   
   [IN_MEASURABLE_BOREL_ALL]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒
          (∀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 ∈ Borel_measurable (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. {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 ∈ Borel_measurable a ⇔
          sigma_algebra a ∧ f ∈ (space a → 𝕌(:extreal)) ∧
          ∀c. {x | Normal c ≤ f x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT1_IMP]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | c ≤ f x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT2]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇔
          sigma_algebra a ∧ f ∈ (space a → 𝕌(:extreal)) ∧
          ∀c. {x | f x ≤ Normal c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT2_IMP]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | f x ≤ c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT3]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇔
          sigma_algebra a ∧ f ∈ (space a → 𝕌(:extreal)) ∧
          ∀c. {x | Normal c < f x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT3_IMP]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | c < f x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT4]  Theorem
      
      ⊢ ∀f a.
          (∀x. f x ≠ −∞) ⇒
          (f ∈ Borel_measurable a ⇔
           sigma_algebra a ∧ f ∈ (space a → 𝕌(:extreal)) ∧
           ∀c d.
             {x | Normal c ≤ f x ∧ f x < Normal d} ∩ space a ∈ subsets a)
   
   [IN_MEASURABLE_BOREL_ALT4_IMP]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒
          ∀c d. {x | c ≤ f x ∧ f x < d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT5]  Theorem
      
      ⊢ ∀f a.
          (∀x. f x ≠ −∞) ⇒
          (f ∈ Borel_measurable a ⇔
           sigma_algebra a ∧ f ∈ (space a → 𝕌(:extreal)) ∧
           ∀c d.
             {x | Normal c < f x ∧ f x ≤ Normal d} ∩ space a ∈ subsets a)
   
   [IN_MEASURABLE_BOREL_ALT5_IMP]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒
          ∀c d. {x | c < f x ∧ f x ≤ d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT6]  Theorem
      
      ⊢ ∀f a.
          (∀x. f x ≠ −∞) ⇒
          (f ∈ Borel_measurable a ⇔
           sigma_algebra a ∧ f ∈ (space a → 𝕌(:extreal)) ∧
           ∀c d.
             {x | Normal c ≤ f x ∧ f x ≤ Normal d} ∩ space a ∈ subsets a)
   
   [IN_MEASURABLE_BOREL_ALT6_IMP]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒
          ∀c d. {x | c ≤ f x ∧ f x ≤ d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT7]  Theorem
      
      ⊢ ∀f a.
          (∀x. f x ≠ −∞) ⇒
          (f ∈ Borel_measurable a ⇔
           sigma_algebra a ∧ f ∈ (space a → 𝕌(:extreal)) ∧
           ∀c d.
             {x | Normal c < f x ∧ f x < Normal d} ∩ space a ∈ subsets a)
   
   [IN_MEASURABLE_BOREL_ALT7_IMP]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒
          ∀c d. {x | c < f x ∧ f x < d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT8]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | f x = c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_ALT9]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | f x ≠ c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_BOREL_ABS]  Theorem
      
      ⊢ abs ∈ Borel_measurable Borel
   
   [IN_MEASURABLE_BOREL_BOREL_I]  Theorem
      
      ⊢ (λx. x) ∈ Borel_measurable Borel
   
   [IN_MEASURABLE_BOREL_CC]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒
          ∀c d. {x | c ≤ f x ∧ f x ≤ d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_CMUL]  Theorem
      
      ⊢ ∀a f g z.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          (∀x. x ∈ space a ⇒ g x = Normal z * f x) ⇒
          g ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_CMUL_INDICATOR]  Theorem
      
      ⊢ ∀a z s.
          sigma_algebra a ∧ s ∈ subsets a ⇒
          (λx. Normal z * 𝟙 s x) ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_CMUL_INDICATOR']  Theorem
      
      ⊢ ∀a c s.
          sigma_algebra a ∧ s ∈ subsets a ⇒
          (λx. c * 𝟙 s x) ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_CO]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒
          ∀c d. {x | c ≤ f x ∧ f x < d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_CONST]  Theorem
      
      ⊢ ∀a k f.
          sigma_algebra a ∧ (∀x. x ∈ space a ⇒ f x = k) ⇒
          f ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_CONST']  Theorem
      
      ⊢ ∀a k. sigma_algebra a ⇒ (λx. k) ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_CR]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | c ≤ f x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_EQ]  Theorem
      
      ⊢ ∀m f g.
          (∀x. x ∈ m_space m ⇒ f x = g x) ∧
          g ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
          f ∈ Borel_measurable (m_space m,measurable_sets m)
   
   [IN_MEASURABLE_BOREL_EQ']  Theorem
      
      ⊢ ∀a f g.
          (∀x. x ∈ space a ⇒ f x = g x) ∧ g ∈ Borel_measurable a ⇒
          f ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_FN_MINUS]  Theorem
      
      ⊢ ∀a f. f ∈ Borel_measurable a ⇒ f⁻ ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_FN_PLUS]  Theorem
      
      ⊢ ∀a f. f ∈ Borel_measurable a ⇒ f⁺ ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_IMP]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | f x < c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_IMP_BOREL]  Theorem
      
      ⊢ ∀f m.
          f ∈ borel_measurable (m_space m,measurable_sets m) ⇒
          Normal ∘ f ∈ Borel_measurable (m_space m,measurable_sets m)
   
   [IN_MEASURABLE_BOREL_IMP_BOREL']  Theorem
      
      ⊢ ∀a f.
          sigma_algebra a ∧ f ∈ borel_measurable a ⇒
          Normal ∘ f ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_INDICATOR]  Theorem
      
      ⊢ ∀a A f.
          sigma_algebra a ∧ A ∈ subsets a ∧ (∀x. x ∈ space a ⇒ f x = 𝟙 A x) ⇒
          f ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_LE]  Theorem
      
      ⊢ ∀a f g.
          f ∈ Borel_measurable a ∧ g ∈ Borel_measurable a ⇒
          {x | f x ≤ g x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_LT]  Theorem
      
      ⊢ ∀f g a.
          f ∈ Borel_measurable a ∧ g ∈ Borel_measurable a ⇒
          {x | f x < g x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_MAX]  Theorem
      
      ⊢ ∀a f g.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧ g ∈ Borel_measurable a ⇒
          (λx. max (f x) (g x)) ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_MAXIMAL]  Theorem
      
      ⊢ ∀N. FINITE N ⇒
            ∀g f a.
              sigma_algebra a ∧ (∀n. g n ∈ Borel_measurable a) ∧
              (∀x. f x = sup (IMAGE (λn. g n x) N)) ⇒
              f ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_MIN]  Theorem
      
      ⊢ ∀a f g.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧ g ∈ Borel_measurable a ⇒
          (λx. min (f x) (g x)) ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_MINIMAL]  Theorem
      
      ⊢ ∀N. FINITE N ⇒
            ∀g f a.
              sigma_algebra a ∧ (∀n. g n ∈ Borel_measurable a) ∧
              (∀x. f x = inf (IMAGE (λn. g n x) N)) ⇒
              f ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_MINUS]  Theorem
      
      ⊢ ∀a f g.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          (∀x. x ∈ space a ⇒ g x = -f x) ⇒
          g ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_MONO_SUP]  Theorem
      
      ⊢ ∀fn f a.
          sigma_algebra a ∧ (∀n. fn n ∈ Borel_measurable a) ∧
          (∀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 ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_MUL]  Theorem
      
      ⊢ ∀a f g h.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          g ∈ Borel_measurable a ∧ (∀x. x ∈ space a ⇒ h x = f x * g x) ∧
          (∀x. x ∈ space a ⇒ f x ≠ −∞ ∧ f x ≠ +∞ ∧ g x ≠ −∞ ∧ g x ≠ +∞) ⇒
          h ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_MUL_INDICATOR]  Theorem
      
      ⊢ ∀a f s.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧ s ∈ subsets a ⇒
          (λx. f x * 𝟙 s x) ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_MUL_INDICATOR_EQ]  Theorem
      
      ⊢ ∀a f.
          sigma_algebra a ⇒
          (f ∈ Borel_measurable a ⇔
           (λx. f x * 𝟙 (space a) x) ∈ Borel_measurable a)
   
   [IN_MEASURABLE_BOREL_NEGINF]  Theorem
      
      ⊢ ∀f a. f ∈ Borel_measurable a ⇒ {x | f x = −∞} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_NOT_NEGINF]  Theorem
      
      ⊢ ∀f a. f ∈ Borel_measurable a ⇒ {x | f x ≠ −∞} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_NOT_POSINF]  Theorem
      
      ⊢ ∀f a. f ∈ Borel_measurable a ⇒ {x | f x ≠ +∞} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_NOT_SING]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | f x ≠ c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_OC]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒
          ∀c d. {x | c < f x ∧ f x ≤ d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_OO]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒
          ∀c d. {x | c < f x ∧ f x < d} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_OR]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | c < f x} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_PLUS_MINUS]  Theorem
      
      ⊢ ∀a f.
          f ∈ Borel_measurable a ⇔
          f⁺ ∈ Borel_measurable a ∧ f⁻ ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_POSINF]  Theorem
      
      ⊢ ∀f a. f ∈ Borel_measurable a ⇒ {x | f x = +∞} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_POW]  Theorem
      
      ⊢ ∀n a f.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          (∀x. x ∈ space a ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ⇒
          (λx. f x pow n) ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_RC]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | f x ≤ c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_RO]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | f x < c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_SING]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇒ ∀c. {x | f x = c} ∩ space a ∈ subsets a
   
   [IN_MEASURABLE_BOREL_SQR]  Theorem
      
      ⊢ ∀a f g.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          (∀x. x ∈ space a ⇒ g x = (f x)²) ⇒
          g ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_SUB]  Theorem
      
      ⊢ ∀a f g h.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          g ∈ Borel_measurable a ∧
          (∀x. x ∈ space a ⇒ f x ≠ −∞ ∧ g x ≠ +∞ ∨ f x ≠ +∞ ∧ g x ≠ −∞) ∧
          (∀x. x ∈ space a ⇒ h x = f x − g x) ⇒
          h ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_SUB']  Theorem
      
      ⊢ ∀a f g h.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          g ∈ Borel_measurable a ∧ (∀x. x ∈ space a ⇒ h x = f x − g x) ⇒
          h ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_SUM]  Theorem
      
      ⊢ ∀a f g s.
          FINITE s ∧ sigma_algebra a ∧
          (∀i. i ∈ s ⇒ f i ∈ Borel_measurable a) ∧
          (∀i x. i ∈ s ∧ x ∈ space a ⇒ f i x ≠ −∞) ∧
          (∀x. x ∈ space a ⇒ g x = ∑ (λi. f i x) s) ⇒
          g ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_SUMINF]  Theorem
      
      ⊢ ∀fn f a.
          sigma_algebra a ∧ (∀n. fn n ∈ Borel_measurable a) ∧
          (∀i x. x ∈ space a ⇒ 0 ≤ fn i x) ∧
          (∀x. x ∈ space a ⇒ f x = suminf (λn. fn n x)) ⇒
          f ∈ Borel_measurable a
   
   [IN_MEASURABLE_BOREL_TIMES]  Theorem
      
      ⊢ ∀m f g h.
          measure_space m ∧
          f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
          g ∈ Borel_measurable (m_space m,measurable_sets m) ∧
          (∀x. x ∈ m_space m ⇒ h x = f x * g x) ⇒
          h ∈ Borel_measurable (m_space m,measurable_sets m)
   
   [IN_MEASURABLE_BOREL_TIMES']  Theorem
      
      ⊢ ∀a f g h.
          sigma_algebra a ∧ f ∈ Borel_measurable a ∧
          g ∈ Borel_measurable a ∧ (∀x. x ∈ space a ⇒ h x = f x * g x) ⇒
          h ∈ Borel_measurable a
   
   [MEASURABLE_BOREL]  Theorem
      
      ⊢ ∀f a.
          f ∈ Borel_measurable a ⇔
          sigma_algebra a ∧ f ∈ (space a → 𝕌(:extreal)) ∧
          ∀c. PREIMAGE f {x | x < Normal c} ∩ space a ∈ subsets a
   
   [MEASURE_SPACE_LBOREL]  Theorem
      
      ⊢ measure_space ext_lborel
   
   [SIGMA_ALGEBRA_BOREL]  Theorem
      
      ⊢ sigma_algebra Borel
   
   [SIGMA_ALGEBRA_BOREL_2D]  Theorem
      
      ⊢ sigma_algebra (Borel × Borel)
   
   [SIGMA_FINITE_LBOREL]  Theorem
      
      ⊢ sigma_finite ext_lborel
   
   [SPACE_BOREL]  Theorem
      
      ⊢ space Borel = 𝕌(:extreal)
   
   [SPACE_BOREL_2D]  Theorem
      
      ⊢ space (Borel × Borel) = 𝕌(:extreal # extreal)
   
   [absolutely_integrable_on_indicator]  Theorem
      
      ⊢ ∀A X.
          indicator A absolutely_integrable_on X ⇔
          indicator A integrable_on X
   
   [borel_eq_real_set]  Theorem
      
      ⊢ borel = (𝕌(:real),IMAGE real_set (subsets Borel))
   
   [borel_imp_lebesgue_measurable]  Theorem
      
      ⊢ ∀f. f ∈ borel_measurable (space borel,subsets borel) ⇒
            f ∈
            borel_measurable (m_space lebesgue,measurable_sets lebesgue)
   
   [borel_imp_lebesgue_sets]  Theorem
      
      ⊢ ∀s. s ∈ subsets borel ⇒ s ∈ measurable_sets lebesgue
   
   [countably_additive_lebesgue]  Theorem
      
      ⊢ countably_additive lebesgue
   
   [fn_minus]  Theorem
      
      ⊢ ∀f x. f⁻ x = -min 0 (f x)
   
   [fn_minus_mul_indicator]  Theorem
      
      ⊢ ∀f s. (λx. f x * 𝟙 s x)⁻ = (λx. f⁻ x * 𝟙 s x)
   
   [fn_plus]  Theorem
      
      ⊢ ∀f x. f⁺ x = max 0 (f x)
   
   [fn_plus_mul_indicator]  Theorem
      
      ⊢ ∀f s. (λx. f x * 𝟙 s x)⁺ = (λx. f⁺ x * 𝟙 s x)
   
   [has_integral_indicator_UNIV]  Theorem
      
      ⊢ ∀s A x.
          (indicator (s ∩ A) has_integral x) 𝕌(:real) ⇔
          (indicator s has_integral x) A
   
   [has_integral_interval_cube]  Theorem
      
      ⊢ ∀a b n.
          (indicator (interval [(a,b)]) has_integral
           content (interval [(a,b)] ∩ line n)) (line n)
   
   [in_borel_measurable_continuous_on]  Theorem
      
      ⊢ ∀f. f continuous_on 𝕌(:real) ⇒ f ∈ borel_measurable borel
   
   [in_borel_measurable_from_Borel]  Theorem
      
      ⊢ ∀a f. f ∈ Borel_measurable a ⇒ real ∘ f ∈ borel_measurable a
   
   [in_borel_measurable_imp]  Theorem
      
      ⊢ ∀m f.
          measure_space m ∧
          (∀s. open s ⇒ PREIMAGE f s ∩ m_space m ∈ measurable_sets m) ⇒
          f ∈ borel_measurable (m_space m,measurable_sets m)
   
   [in_measurable_sigma_pow]  Theorem
      
      ⊢ ∀m sp N f.
          measure_space m ∧ N ⊆ POW sp ∧ f ∈ (m_space m → sp) ∧
          (∀y. y ∈ N ⇒ PREIMAGE f y ∩ m_space m ∈ measurable_sets m) ⇒
          f ∈ measurable (m_space m,measurable_sets m) (sigma sp N)
   
   [in_sets_lebesgue]  Theorem
      
      ⊢ ∀A. (∀n. indicator A integrable_on line n) ⇒
            A ∈ measurable_sets lebesgue
   
   [in_sets_lebesgue_imp]  Theorem
      
      ⊢ ∀A n.
          A ∈ measurable_sets lebesgue ⇒ indicator A integrable_on line n
   
   [indicator_fn_general_cross]  Theorem
      
      ⊢ ∀cons car cdr s t x y.
          pair_operation cons car cdr ⇒
          𝟙 (general_cross cons s t) (cons x y) = 𝟙 s x * 𝟙 t y
   
   [indicator_fn_normal]  Theorem
      
      ⊢ ∀s x. ∃r. 𝟙 s x = Normal r ∧ 0 ≤ r ∧ r ≤ 1
   
   [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 ⇒ 𝟙 a = (λx. ∑ (λi. 𝟙 (a ∩ b i) x) r)
   
   [indicator_fn_suminf]  Theorem
      
      ⊢ ∀a x.
          (∀m n. m ≠ n ⇒ DISJOINT (a m) (a n)) ⇒
          suminf (λi. 𝟙 (a i) x) = 𝟙 (BIGUNION (IMAGE a 𝕌(:num))) x
   
   [integrable_indicator_UNIV]  Theorem
      
      ⊢ ∀s A.
          indicator (s ∩ A) integrable_on 𝕌(:real) ⇔
          indicator s integrable_on A
   
   [integral_indicator_UNIV]  Theorem
      
      ⊢ ∀s A.
          integral 𝕌(:real) (indicator (s ∩ A)) = integral A (indicator s)
   
   [integral_one]  Theorem
      
      ⊢ ∀A. integral A (λx. 1) = integral 𝕌(:real) (indicator A)
   
   [lambda0_empty]  Theorem
      
      ⊢ lambda0 ∅ = 0
   
   [lambda0_not_infty]  Theorem
      
      ⊢ ∀a b.
          lambda0 (right_open_interval a b) ≠ +∞ ∧
          lambda0 (right_open_interval a b) ≠ −∞
   
   [lambda_closed_interval]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ lambda (interval [(a,b)]) = Normal (b − a)
   
   [lambda_closed_interval_content]  Theorem
      
      ⊢ ∀a b.
          lambda (interval [(a,b)]) = Normal (content (interval [(a,b)]))
   
   [lambda_empty]  Theorem
      
      ⊢ lambda ∅ = 0
   
   [lambda_eq]  Theorem
      
      ⊢ ∀m. (∀a b.
               measure m (interval [(a,b)]) =
               Normal (content (interval [(a,b)]))) ∧ measure_space m ∧
            m_space m = space borel ∧ measurable_sets m = subsets borel ⇒
            ∀s. s ∈ subsets borel ⇒ lambda s = measure m s
   
   [lambda_eq_lebesgue]  Theorem
      
      ⊢ ∀s. s ∈ subsets borel ⇒ lambda s = measure lebesgue s
   
   [lambda_not_infty]  Theorem
      
      ⊢ ∀a b.
          lambda (right_open_interval a b) ≠ +∞ ∧
          lambda (right_open_interval a b) ≠ −∞
   
   [lambda_open_interval]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ lambda (interval (a,b)) = Normal (b − a)
   
   [lambda_prop]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ lambda (right_open_interval a b) = Normal (b − a)
   
   [lambda_sing]  Theorem
      
      ⊢ ∀c. lambda {c} = 0
   
   [lborel0_additive]  Theorem
      
      ⊢ additive lborel0
   
   [lborel0_finite_additive]  Theorem
      
      ⊢ finite_additive lborel0
   
   [lborel0_positive]  Theorem
      
      ⊢ positive lborel0
   
   [lborel0_premeasure]  Theorem
      
      ⊢ premeasure lborel0
   
   [lborel0_subadditive]  Theorem
      
      ⊢ subadditive lborel0
   
   [lborel_subset_lebesgue]  Theorem
      
      ⊢ measurable_sets lborel ⊆ measurable_sets lebesgue
   
   [lebesgue_closed_interval]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ measure lebesgue (interval [(a,b)]) = Normal (b − a)
   
   [lebesgue_closed_interval_content]  Theorem
      
      ⊢ ∀a b.
          measure lebesgue (interval [(a,b)]) =
          Normal (content (interval [(a,b)]))
   
   [lebesgue_empty]  Theorem
      
      ⊢ measure lebesgue ∅ = 0
   
   [lebesgue_eq_lambda]  Theorem
      
      ⊢ ∀s. s ∈ subsets borel ⇒ measure lebesgue s = lambda s
   
   [lebesgue_measure_iff_LIMSEQ]  Theorem
      
      ⊢ ∀A m.
          A ∈ measurable_sets lebesgue ∧ 0 ≤ m ⇒
          (measure lebesgue A = Normal m ⇔
           ((λn. integral (line n) (indicator A)) --> m) sequentially)
   
   [lebesgue_of_negligible]  Theorem
      
      ⊢ ∀s. negligible s ⇒ measure lebesgue s = 0
   
   [lebesgue_open_interval]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ measure lebesgue (interval (a,b)) = Normal (b − a)
   
   [lebesgue_sing]  Theorem
      
      ⊢ ∀c. measure lebesgue {c} = 0
   
   [liminf_limsup]  Theorem
      
      ⊢ ∀E. COMPL (liminf E) = limsup (COMPL ∘ E)
   
   [liminf_limsup_sp]  Theorem
      
      ⊢ ∀sp E. (∀n. E n ⊆ sp) ⇒ sp DIFF liminf E = limsup (λn. sp DIFF E n)
   
   [limseq_indicator_BIGUNION]  Theorem
      
      ⊢ ∀A x.
          ((λk. indicator (BIGUNION {A i | i < k}) x) -->
           indicator (BIGUNION {A i | i ∈ 𝕌(:num)}) x) sequentially
   
   [limsup_suminf_indicator]  Theorem
      
      ⊢ ∀A. limsup A = {x | suminf (λn. 𝟙 (A n) x) = +∞}
   
   [limsup_suminf_indicator_space]  Theorem
      
      ⊢ ∀a A.
          sigma_algebra a ∧ (∀n. A n ∈ subsets a) ⇒
          limsup A = {x | x ∈ space a ∧ suminf (λn. 𝟙 (A n) x) = +∞}
   
   [m_space_lborel]  Theorem
      
      ⊢ m_space lborel = space borel
   
   [measure_lebesgue]  Theorem
      
      ⊢ measure lebesgue =
        (λA. sup {Normal (integral (line n) (indicator A)) | n ∈ 𝕌(:num)})
   
   [measure_liminf]  Theorem
      
      ⊢ ∀p A.
          measure_space p ∧ (∀n. A n ∈ measurable_sets p) ⇒
          measure p (liminf A) =
          sup (IMAGE (λm. measure p (BIGINTER {A n | m ≤ n})) 𝕌(:num))
   
   [measure_limsup]  Theorem
      
      ⊢ ∀p A.
          measure_space p ∧ measure p (BIGUNION (IMAGE A 𝕌(:num))) < +∞ ∧
          (∀n. A n ∈ measurable_sets p) ⇒
          measure p (limsup A) =
          inf (IMAGE (λm. measure p (BIGUNION {A n | m ≤ n})) 𝕌(:num))
   
   [measure_limsup_finite]  Theorem
      
      ⊢ ∀p A.
          measure_space p ∧ measure p (m_space p) < +∞ ∧
          (∀n. A n ∈ measurable_sets p) ⇒
          measure p (limsup A) =
          inf (IMAGE (λm. measure p (BIGUNION {A n | m ≤ n})) 𝕌(:num))
   
   [measure_space_lborel]  Theorem
      
      ⊢ measure_space lborel
   
   [measure_space_lebesgue]  Theorem
      
      ⊢ measure_space lebesgue
   
   [negligible_in_lebesgue]  Theorem
      
      ⊢ ∀s. negligible s ⇒ s ∈ measurable_sets lebesgue
   
   [nonneg_abs]  Theorem
      
      ⊢ ∀f. nonneg (abs ∘ f)
   
   [nonneg_fn_abs]  Theorem
      
      ⊢ ∀f. nonneg f ⇒ abs ∘ f = f
   
   [nonneg_fn_minus]  Theorem
      
      ⊢ ∀f. nonneg f ⇒ f⁻ = (λx. 0)
   
   [nonneg_fn_plus]  Theorem
      
      ⊢ ∀f. nonneg f ⇒ f⁺ = f
   
   [positive_lebesgue]  Theorem
      
      ⊢ positive lebesgue
   
   [seq_le_imp_lim_le]  Theorem
      
      ⊢ ∀x y f. (∀n. f n ≤ x) ∧ (f --> y) sequentially ⇒ y ≤ x
   
   [seq_mono_le]  Theorem
      
      ⊢ ∀f x n. (∀n. f n ≤ f (n + 1)) ∧ (f --> x) sequentially ⇒ f n ≤ x
   
   [set_limsup_alt]  Theorem
      
      ⊢ ∀E. limsup E =
            BIGINTER (IMAGE (λn. BIGUNION (IMAGE E (from n))) 𝕌(:num))
   
   [sets_lborel]  Theorem
      
      ⊢ measurable_sets lborel = subsets borel
   
   [sets_lebesgue]  Theorem
      
      ⊢ measurable_sets lebesgue =
        {A | ∀n. indicator A integrable_on line n}
   
   [sigma_algebra_lebesgue]  Theorem
      
      ⊢ sigma_algebra (𝕌(:real),{A | ∀n. indicator A integrable_on line n})
   
   [sigma_finite_lborel]  Theorem
      
      ⊢ sigma_finite lborel
   
   [space_lborel]  Theorem
      
      ⊢ m_space lborel = 𝕌(:real)
   
   [space_lebesgue]  Theorem
      
      ⊢ m_space lebesgue = 𝕌(:real)
   
   [sup_sequence]  Theorem
      
      ⊢ ∀f l.
          mono_increasing f ⇒
          ((f --> l) sequentially ⇔
           sup (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l)
   
   
*)
end

HOL 4, Kananaskis-14