Structure real_borelTheory

signature real_borelTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val borel : thm
    val box : thm
    val indicator_fn_def : thm
    val line : thm
    val mr2 : thm
    val real_rat_set_def : thm
    val right_open_interval : thm
    val right_open_intervals : thm
  
  (*  Theorems  *)
    val ADD_IN_QSET : thm
    val BALL_IN_LINE : thm
    val BIGUNION_IMAGE_QSET : thm
    val CLG_UBOUND : thm
    val DIV_IN_QSET : thm
    val IMAGE_FST_CROSS_INTERVAL : thm
    val IMAGE_SND_CROSS_INTERVAL : thm
    val INV_IN_QSET : thm
    val ISMET_R2 : thm
    val LINE_MONO : thm
    val LINE_MONO_EQ : thm
    val LINE_MONO_SUC : thm
    val MR2_DEF : thm
    val MUL_IN_QSET : thm
    val NON_NEG_REAL_RAT_DENSE : thm
    val NUM_IN_QSET : thm
    val OPP_IN_QSET : thm
    val QSET_COUNTABLE : thm
    val Q_DENSE_IN_REAL : thm
    val Q_DENSE_IN_REAL_LEMMA : thm
    val REAL_IN_LINE : thm
    val REAL_RAT_DENSE : thm
    val REAL_SING_BIGINTER : thm
    val SUB_IN_QSET : thm
    val borel_2d : thm
    val borel_2d_alt_box : thm
    val borel_closed : thm
    val borel_comp : thm
    val borel_def : thm
    val borel_eq_box : thm
    val borel_eq_ge_le : thm
    val borel_eq_ge_less : thm
    val borel_eq_gr : thm
    val borel_eq_gr_le : thm
    val borel_eq_gr_less : thm
    val borel_eq_le : thm
    val borel_eq_less : thm
    val borel_eq_sigmaI1 : thm
    val borel_eq_sigmaI2 : thm
    val borel_eq_sigmaI3 : thm
    val borel_eq_sigmaI4 : thm
    val borel_eq_sigmaI5 : thm
    val borel_line : thm
    val borel_measurable_const : thm
    val borel_measurable_image : thm
    val borel_measurable_indicator : thm
    val borel_measurable_sets : thm
    val borel_measurable_sets_ge : thm
    val borel_measurable_sets_ge_le : thm
    val borel_measurable_sets_ge_less : thm
    val borel_measurable_sets_gr : thm
    val borel_measurable_sets_gr_le : thm
    val borel_measurable_sets_gr_less : thm
    val borel_measurable_sets_le : thm
    val borel_measurable_sets_less : thm
    val borel_measurable_sets_not_sing : thm
    val borel_measurable_sets_sing : thm
    val borel_open : thm
    val borel_sigma_sets_subset : thm
    val borel_singleton : thm
    val box_alt : thm
    val box_open_in_mr2 : thm
    val countable_real_rat_set : thm
    val in_borel_measurable : thm
    val in_borel_measurable_add : thm
    val in_borel_measurable_borel : thm
    val in_borel_measurable_cmul : thm
    val in_borel_measurable_const : thm
    val in_borel_measurable_ge : thm
    val in_borel_measurable_gr : thm
    val in_borel_measurable_le : thm
    val in_borel_measurable_less : thm
    val in_borel_measurable_mul : thm
    val in_borel_measurable_open : thm
    val in_borel_measurable_sqr : thm
    val in_borel_measurable_sub : thm
    val in_right_open_interval : thm
    val in_right_open_intervals : thm
    val in_right_open_intervals_nonempty : thm
    val line_closed : thm
    val open_UNION_box : thm
    val open_UNION_rational_box : thm
    val q_set_def : thm
    val rational_boxes : thm
    val right_open_interval_11 : thm
    val right_open_interval_DISJOINT : thm
    val right_open_interval_DISJOINT_imp : thm
    val right_open_interval_between_bounds : thm
    val right_open_interval_disjoint : thm
    val right_open_interval_empty : thm
    val right_open_interval_empty_eq : thm
    val right_open_interval_in_intervals : thm
    val right_open_interval_inter : thm
    val right_open_interval_interior : thm
    val right_open_interval_lowerbound : thm
    val right_open_interval_two_bounds : thm
    val right_open_interval_union : thm
    val right_open_interval_union_imp : thm
    val right_open_interval_upperbound : thm
    val right_open_intervals_semiring : thm
    val right_open_intervals_sigma_borel : thm
    val right_open_intervals_subset_borel : thm
    val sigma_algebra_borel : thm
    val sigma_algebra_borel_2d : thm
    val sigma_ge_gr : thm
    val sigma_gr_le : thm
    val sigma_le_less : thm
    val sigma_less_ge : thm
    val space_borel : thm
    val space_in_borel : thm
  
  val real_borel_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [integration] Parent theory of "real_borel"
   
   [sigma_algebra] Parent theory of "real_borel"
   
   [borel]  Definition
      
      ⊢ borel = sigma 𝕌(:real) {s | open s}
   
   [box]  Definition
      
      ⊢ ∀a b. box a b = {x | a < x ∧ x < b}
   
   [indicator_fn_def]  Definition
      
      ⊢ ∀s. 𝟙 s = (λx. if x ∈ s then 1 else 0)
   
   [line]  Definition
      
      ⊢ ∀n. line n = {x | -&n ≤ x ∧ x ≤ &n}
   
   [mr2]  Definition
      
      ⊢ mr2 = metric (λ((x1,x2),y1,y2). sqrt ((x1 − y1)² + (x2 − y2)²))
   
   [real_rat_set_def]  Definition
      
      ⊢ q_set =
        {x | ∃a b. x = &a / &b ∧ 0 < &b} ∪
        {x | ∃a b. x = -(&a / &b) ∧ 0 < &b}
   
   [right_open_interval]  Definition
      
      ⊢ ∀a b. right_open_interval a b = {x | a ≤ x ∧ x < b}
   
   [right_open_intervals]  Definition
      
      ⊢ right_open_intervals = (𝕌(:real),{right_open_interval a b | T})
   
   [ADD_IN_QSET]  Theorem
      
      ⊢ ∀x y. x ∈ q_set ∧ y ∈ q_set ⇒ x + y ∈ q_set
   
   [BALL_IN_LINE]  Theorem
      
      ⊢ ∀n. ball (0,&n) ⊆ line n
   
   [BIGUNION_IMAGE_QSET]  Theorem
      
      ⊢ ∀a f.
          sigma_algebra a ∧ f ∈ (q_set → subsets a) ⇒
          BIGUNION (IMAGE f q_set) ∈ subsets a
   
   [CLG_UBOUND]  Theorem
      
      ⊢ ∀x. 0 ≤ x ⇒ &clg x < x + 1
   
   [DIV_IN_QSET]  Theorem
      
      ⊢ ∀x y. x ∈ q_set ∧ y ∈ q_set ∧ y ≠ 0 ⇒ x / y ∈ q_set
   
   [IMAGE_FST_CROSS_INTERVAL]  Theorem
      
      ⊢ ∀a b c d.
          c < d ⇒
          IMAGE FST (interval (a,b) × interval (c,d)) = interval (a,b)
   
   [IMAGE_SND_CROSS_INTERVAL]  Theorem
      
      ⊢ ∀a b c d.
          a < b ⇒
          IMAGE SND (interval (a,b) × interval (c,d)) = interval (c,d)
   
   [INV_IN_QSET]  Theorem
      
      ⊢ ∀x. x ∈ q_set ∧ x ≠ 0 ⇒ 1 / x ∈ q_set
   
   [ISMET_R2]  Theorem
      
      ⊢ ismet (λ((x1,x2),y1,y2). sqrt ((x1 − y1)² + (x2 − y2)²))
   
   [LINE_MONO]  Theorem
      
      ⊢ ∀n N. n ≤ N ⇒ line n ⊆ line N
   
   [LINE_MONO_EQ]  Theorem
      
      ⊢ ∀n N. line n ⊆ line N ⇔ n ≤ N
   
   [LINE_MONO_SUC]  Theorem
      
      ⊢ ∀n. line n ⊆ line (SUC n)
   
   [MR2_DEF]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          dist mr2 ((x1,x2),y1,y2) = sqrt ((x1 − y1)² + (x2 − y2)²)
   
   [MUL_IN_QSET]  Theorem
      
      ⊢ ∀x y. x ∈ q_set ∧ y ∈ q_set ⇒ x * y ∈ q_set
   
   [NON_NEG_REAL_RAT_DENSE]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ x < y ⇒ ∃m n. x < &m / &n ∧ &m / &n < y
   
   [NUM_IN_QSET]  Theorem
      
      ⊢ ∀n. &n ∈ q_set ∧ -&n ∈ q_set
   
   [OPP_IN_QSET]  Theorem
      
      ⊢ ∀x. x ∈ q_set ⇒ -x ∈ q_set
   
   [QSET_COUNTABLE]  Theorem
      
      ⊢ COUNTABLE q_set
   
   [Q_DENSE_IN_REAL]  Theorem
      
      ⊢ ∀x y. x < y ⇒ ∃r. r ∈ q_set ∧ x < r ∧ r < y
   
   [Q_DENSE_IN_REAL_LEMMA]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ x < y ⇒ ∃r. r ∈ q_set ∧ x < r ∧ r < y
   
   [REAL_IN_LINE]  Theorem
      
      ⊢ ∀x. ∃n. x ∈ line n
   
   [REAL_RAT_DENSE]  Theorem
      
      ⊢ ∀x y. x < y ⇒ ∃r. r ∈ q_set ∧ x < r ∧ r < y
   
   [REAL_SING_BIGINTER]  Theorem
      
      ⊢ ∀c. {c} =
            BIGINTER
              (IMAGE
                 (λn. {x | c − (1 / 2) pow n ≤ x ∧ x < c + (1 / 2) pow n})
                 𝕌(:num))
   
   [SUB_IN_QSET]  Theorem
      
      ⊢ ∀x y. x ∈ q_set ∧ y ∈ q_set ⇒ x − y ∈ q_set
   
   [borel_2d]  Theorem
      
      ⊢ borel × borel = sigma 𝕌(:real # real) {s | open_in (mtop mr2) s}
   
   [borel_2d_alt_box]  Theorem
      
      ⊢ borel × borel = sigma 𝕌(:real # real) {box a b × box c d | T}
   
   [borel_closed]  Theorem
      
      ⊢ ∀A. closed A ⇒ A ∈ subsets borel
   
   [borel_comp]  Theorem
      
      ⊢ ∀A. A ∈ subsets borel ⇒ 𝕌(:real) DIFF A ∈ subsets borel
   
   [borel_def]  Theorem
      
      ⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | x ≤ a}) 𝕌(:real))
   
   [borel_eq_box]  Theorem
      
      ⊢ borel = sigma 𝕌(:real) (IMAGE (λ(a,b). box a b) 𝕌(:real # real))
   
   [borel_eq_ge_le]  Theorem
      
      ⊢ borel =
        sigma 𝕌(:real)
          (IMAGE (λ(a,b). {x | a ≤ x ∧ x ≤ b}) 𝕌(:real # real))
   
   [borel_eq_ge_less]  Theorem
      
      ⊢ borel =
        sigma 𝕌(:real)
          (IMAGE (λ(a,b). {x | a ≤ x ∧ x < b}) 𝕌(:real # real))
   
   [borel_eq_gr]  Theorem
      
      ⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | a < x}) 𝕌(:real))
   
   [borel_eq_gr_le]  Theorem
      
      ⊢ borel =
        sigma 𝕌(:real)
          (IMAGE (λ(a,b). {x | a < x ∧ x ≤ b}) 𝕌(:real # real))
   
   [borel_eq_gr_less]  Theorem
      
      ⊢ borel =
        sigma 𝕌(:real)
          (IMAGE (λ(a,b). {x | a < x ∧ x < b}) 𝕌(:real # real))
   
   [borel_eq_le]  Theorem
      
      ⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | x ≤ a}) 𝕌(:real))
   
   [borel_eq_less]  Theorem
      
      ⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | x < a}) 𝕌(:real))
   
   [borel_eq_sigmaI1]  Theorem
      
      ⊢ ∀X A f.
          borel = sigma 𝕌(:real) X ∧
          (∀x. x ∈ X ⇒ x ∈ subsets (sigma 𝕌(:real) (IMAGE f A))) ∧
          (∀i. i ∈ A ⇒ f i ∈ subsets borel) ⇒
          borel = sigma 𝕌(:real) (IMAGE f A)
   
   [borel_eq_sigmaI2]  Theorem
      
      ⊢ ∀G f A B.
          borel = sigma 𝕌(:real) (IMAGE (λ(i,j). G i j) B) ∧
          (∀i j.
             (i,j) ∈ B ⇒
             G i j ∈ subsets (sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) A))) ∧
          (∀i j. (i,j) ∈ A ⇒ f i j ∈ subsets borel) ⇒
          borel = sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) A)
   
   [borel_eq_sigmaI3]  Theorem
      
      ⊢ ∀f A X.
          borel = sigma 𝕌(:real) X ∧
          (∀x. x ∈ X ⇒
               x ∈ subsets (sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) A))) ∧
          (∀i j. (i,j) ∈ A ⇒ f i j ∈ subsets borel) ⇒
          borel = sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) A)
   
   [borel_eq_sigmaI4]  Theorem
      
      ⊢ ∀G f A.
          borel = sigma 𝕌(:real) (IMAGE (λ(i,j). G i j) A) ∧
          (∀i j.
             (i,j) ∈ A ⇒ G i j ∈ subsets (sigma 𝕌(:real) (IMAGE f 𝕌(:γ)))) ∧
          (∀i. f i ∈ subsets borel) ⇒
          borel = sigma 𝕌(:real) (IMAGE f 𝕌(:γ))
   
   [borel_eq_sigmaI5]  Theorem
      
      ⊢ ∀G f.
          borel = sigma 𝕌(:real) (IMAGE G 𝕌(:α)) ∧
          (∀i. G i ∈
               subsets (sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) 𝕌(:β # γ)))) ∧
          (∀i j. f i j ∈ subsets borel) ⇒
          borel = sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) 𝕌(:β # γ))
   
   [borel_line]  Theorem
      
      ⊢ ∀n. line n ∈ subsets borel
   
   [borel_measurable_const]  Theorem
      
      ⊢ ∀M c. sigma_algebra M ⇒ (λx. c) ∈ borel_measurable M
   
   [borel_measurable_image]  Theorem
      
      ⊢ ∀f M x.
          f ∈ borel_measurable M ⇒ PREIMAGE f {x} ∩ space M ∈ subsets M
   
   [borel_measurable_indicator]  Theorem
      
      ⊢ ∀s a. sigma_algebra s ∧ a ∈ subsets s ⇒ 𝟙 a ∈ borel_measurable s
   
   [borel_measurable_sets]  Theorem
      
      ⊢ (∀a. {x | x < a} ∈ subsets borel) ∧
        (∀a. {x | x ≤ a} ∈ subsets borel) ∧
        (∀a. {x | a < x} ∈ subsets borel) ∧
        (∀a. {x | a ≤ x} ∈ subsets borel) ∧
        (∀a b. {x | a < x ∧ x < b} ∈ subsets borel) ∧
        (∀a b. {x | a < x ∧ x ≤ b} ∈ subsets borel) ∧
        (∀a b. {x | a ≤ x ∧ x < b} ∈ subsets borel) ∧
        (∀a b. {x | a ≤ x ∧ x ≤ b} ∈ subsets borel) ∧
        (∀c. {c} ∈ subsets borel) ∧ ∀c. {x | x ≠ c} ∈ subsets borel
   
   [borel_measurable_sets_ge]  Theorem
      
      ⊢ ∀a. {x | a ≤ x} ∈ subsets borel
   
   [borel_measurable_sets_ge_le]  Theorem
      
      ⊢ ∀a b. {x | a ≤ x ∧ x ≤ b} ∈ subsets borel
   
   [borel_measurable_sets_ge_less]  Theorem
      
      ⊢ ∀a b. {x | a ≤ x ∧ x < b} ∈ subsets borel
   
   [borel_measurable_sets_gr]  Theorem
      
      ⊢ ∀a. {x | a < x} ∈ subsets borel
   
   [borel_measurable_sets_gr_le]  Theorem
      
      ⊢ ∀a b. {x | a < x ∧ x ≤ b} ∈ subsets borel
   
   [borel_measurable_sets_gr_less]  Theorem
      
      ⊢ ∀a b. {x | a < x ∧ x < b} ∈ subsets borel
   
   [borel_measurable_sets_le]  Theorem
      
      ⊢ ∀a. {x | x ≤ a} ∈ subsets borel
   
   [borel_measurable_sets_less]  Theorem
      
      ⊢ ∀a. {x | x < a} ∈ subsets borel
   
   [borel_measurable_sets_not_sing]  Theorem
      
      ⊢ ∀c. {x | x ≠ c} ∈ subsets borel
   
   [borel_measurable_sets_sing]  Theorem
      
      ⊢ ∀c. {c} ∈ subsets borel
   
   [borel_open]  Theorem
      
      ⊢ ∀A. open A ⇒ A ∈ subsets borel
   
   [borel_sigma_sets_subset]  Theorem
      
      ⊢ ∀A. A ⊆ subsets borel ⇒ sigma_sets 𝕌(:real) A ⊆ subsets borel
   
   [borel_singleton]  Theorem
      
      ⊢ ∀A x. A ∈ subsets borel ⇒ x INSERT A ∈ subsets borel
   
   [box_alt]  Theorem
      
      ⊢ ∀a b. box a b = interval (a,b)
   
   [box_open_in_mr2]  Theorem
      
      ⊢ ∀a b c d. open_in (mtop mr2) (interval (a,b) × interval (c,d))
   
   [countable_real_rat_set]  Theorem
      
      ⊢ COUNTABLE q_set
   
   [in_borel_measurable]  Theorem
      
      ⊢ ∀f s.
          f ∈ borel_measurable s ⇔
          sigma_algebra s ∧
          ∀s'.
            s' ∈
            subsets (sigma 𝕌(:real) (IMAGE (λa. {x | x ≤ a}) 𝕌(:real))) ⇒
            PREIMAGE f s' ∩ space s ∈ subsets s
   
   [in_borel_measurable_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_borel_measurable_borel]  Theorem
      
      ⊢ ∀f M.
          f ∈ borel_measurable M ⇔
          sigma_algebra M ∧
          ∀s. s ∈ subsets borel ⇒ PREIMAGE f s ∩ space M ∈ subsets M
   
   [in_borel_measurable_cmul]  Theorem
      
      ⊢ ∀a f g z.
          sigma_algebra a ∧ f ∈ borel_measurable a ∧
          (∀x. x ∈ space a ⇒ g x = z * f x) ⇒
          g ∈ borel_measurable a
   
   [in_borel_measurable_const]  Theorem
      
      ⊢ ∀a k f.
          sigma_algebra a ∧ (∀x. x ∈ space a ⇒ f x = k) ⇒
          f ∈ borel_measurable a
   
   [in_borel_measurable_ge]  Theorem
      
      ⊢ ∀f m.
          f ∈ borel_measurable m ⇔
          sigma_algebra m ∧ f ∈ (space m → 𝕌(:real)) ∧
          ∀a. {w | w ∈ space m ∧ a ≤ f w} ∈ subsets m
   
   [in_borel_measurable_gr]  Theorem
      
      ⊢ ∀f m.
          f ∈ borel_measurable m ⇔
          sigma_algebra m ∧ f ∈ (space m → 𝕌(:real)) ∧
          ∀a. {w | w ∈ space m ∧ a < f w} ∈ subsets m
   
   [in_borel_measurable_le]  Theorem
      
      ⊢ ∀f m.
          f ∈ borel_measurable m ⇔
          sigma_algebra m ∧ f ∈ (space m → 𝕌(:real)) ∧
          ∀a. {w | w ∈ space m ∧ f w ≤ a} ∈ subsets m
   
   [in_borel_measurable_less]  Theorem
      
      ⊢ ∀f m.
          f ∈ borel_measurable m ⇔
          sigma_algebra m ∧ f ∈ (space m → 𝕌(:real)) ∧
          ∀a. {w | w ∈ space m ∧ f w < a} ∈ subsets m
   
   [in_borel_measurable_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) ⇒
          h ∈ borel_measurable a
   
   [in_borel_measurable_open]  Theorem
      
      ⊢ ∀f M.
          f ∈ borel_measurable M ⇔
          sigma_algebra M ∧
          ∀s. s ∈ subsets (sigma 𝕌(:real) {s | open s}) ⇒
              PREIMAGE f s ∩ space M ∈ subsets M
   
   [in_borel_measurable_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_borel_measurable_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_right_open_interval]  Theorem
      
      ⊢ ∀a b x. x ∈ right_open_interval a b ⇔ a ≤ x ∧ x < b
   
   [in_right_open_intervals]  Theorem
      
      ⊢ ∀s. s ∈ subsets right_open_intervals ⇔
            ∃a b. s = right_open_interval a b
   
   [in_right_open_intervals_nonempty]  Theorem
      
      ⊢ ∀s. s ≠ ∅ ∧ s ∈ subsets right_open_intervals ⇔
            ∃a b. a < b ∧ s = right_open_interval a b
   
   [line_closed]  Theorem
      
      ⊢ ∀n. closed (line n)
   
   [open_UNION_box]  Theorem
      
      ⊢ ∀M. open M ⇒ M = BIGUNION {box a b | box a b ⊆ M}
   
   [open_UNION_rational_box]  Theorem
      
      ⊢ ∀M. open M ⇒
            M = BIGUNION {box a b | a ∈ q_set ∧ b ∈ q_set ∧ box a b ⊆ M}
   
   [q_set_def]  Theorem
      
      ⊢ q_set =
        {x | ∃a b. x = &a / &b ∧ 0 < &b} ∪
        {x | ∃a b. x = -(&a / &b) ∧ 0 < &b}
   
   [rational_boxes]  Theorem
      
      ⊢ ∀x e.
          0 < e ⇒
          ∃a b. a ∈ q_set ∧ b ∈ q_set ∧ x ∈ box a b ∧ box a b ⊆ ball (x,e)
   
   [right_open_interval_11]  Theorem
      
      ⊢ ∀a b c d.
          a < b ∧ c < d ⇒
          (right_open_interval a b = right_open_interval c d ⇔
           a = c ∧ b = d)
   
   [right_open_interval_DISJOINT]  Theorem
      
      ⊢ ∀a b c d.
          a ≤ b ∧ b ≤ c ∧ c ≤ d ⇒
          DISJOINT (right_open_interval a b) (right_open_interval c d)
   
   [right_open_interval_DISJOINT_imp]  Theorem
      
      ⊢ ∀a b c d.
          a < b ∧ c < d ∧
          DISJOINT (right_open_interval a b) (right_open_interval c d) ⇒
          b ≤ c ∨ d ≤ a
   
   [right_open_interval_between_bounds]  Theorem
      
      ⊢ ∀x a b.
          x ∈ right_open_interval a b ⇔
          interval_lowerbound (right_open_interval a b) ≤ x ∧
          x < interval_upperbound (right_open_interval a b)
   
   [right_open_interval_disjoint]  Theorem
      
      ⊢ ∀a b c d.
          a ≤ b ∧ b ≤ c ∧ c ≤ d ⇒
          disjoint {right_open_interval a b; right_open_interval c d}
   
   [right_open_interval_empty]  Theorem
      
      ⊢ ∀a b. right_open_interval a b = ∅ ⇔ ¬(a < b)
   
   [right_open_interval_empty_eq]  Theorem
      
      ⊢ ∀a b. a = b ⇒ right_open_interval a b = ∅
   
   [right_open_interval_in_intervals]  Theorem
      
      ⊢ ∀a b. right_open_interval a b ∈ subsets right_open_intervals
   
   [right_open_interval_inter]  Theorem
      
      ⊢ ∀a b c d.
          right_open_interval a b ∩ right_open_interval c d =
          right_open_interval (max a c) (min b d)
   
   [right_open_interval_interior]  Theorem
      
      ⊢ ∀a b. a < b ⇒ a ∈ right_open_interval a b
   
   [right_open_interval_lowerbound]  Theorem
      
      ⊢ ∀a b. a < b ⇒ interval_lowerbound (right_open_interval a b) = a
   
   [right_open_interval_two_bounds]  Theorem
      
      ⊢ ∀a b.
          interval_lowerbound (right_open_interval a b) ≤
          interval_upperbound (right_open_interval a b)
   
   [right_open_interval_union]  Theorem
      
      ⊢ ∀a b c d.
          a < b ∧ c < d ∧ a ≤ d ∧ c ≤ b ⇒
          right_open_interval a b ∪ right_open_interval c d =
          right_open_interval (min a c) (max b d)
   
   [right_open_interval_union_imp]  Theorem
      
      ⊢ ∀a b c d.
          a < b ∧ c < d ∧
          right_open_interval a b ∪ right_open_interval c d ∈
          subsets right_open_intervals ⇒
          a ≤ d ∧ c ≤ b
   
   [right_open_interval_upperbound]  Theorem
      
      ⊢ ∀a b. a < b ⇒ interval_upperbound (right_open_interval a b) = b
   
   [right_open_intervals_semiring]  Theorem
      
      ⊢ semiring right_open_intervals
   
   [right_open_intervals_sigma_borel]  Theorem
      
      ⊢ sigma (space right_open_intervals) (subsets right_open_intervals) =
        borel
   
   [right_open_intervals_subset_borel]  Theorem
      
      ⊢ subsets right_open_intervals ⊆ subsets borel
   
   [sigma_algebra_borel]  Theorem
      
      ⊢ sigma_algebra borel
   
   [sigma_algebra_borel_2d]  Theorem
      
      ⊢ sigma_algebra (borel × borel)
   
   [sigma_ge_gr]  Theorem
      
      ⊢ ∀f A.
          sigma_algebra A ∧ (∀a. {w | w ∈ space A ∧ a ≤ f w} ∈ subsets A) ⇒
          ∀a. {w | w ∈ space A ∧ a < f w} ∈ subsets A
   
   [sigma_gr_le]  Theorem
      
      ⊢ ∀f A.
          sigma_algebra A ∧ (∀a. {w | w ∈ space A ∧ a < f w} ∈ subsets A) ⇒
          ∀a. {w | w ∈ space A ∧ f w ≤ a} ∈ subsets A
   
   [sigma_le_less]  Theorem
      
      ⊢ ∀f A.
          sigma_algebra A ∧ (∀a. {w | w ∈ space A ∧ f w ≤ a} ∈ subsets A) ⇒
          ∀a. {w | w ∈ space A ∧ f w < a} ∈ subsets A
   
   [sigma_less_ge]  Theorem
      
      ⊢ ∀f A.
          sigma_algebra A ∧ (∀a. {w | w ∈ space A ∧ f w < a} ∈ subsets A) ⇒
          ∀a. {w | w ∈ space A ∧ a ≤ f w} ∈ subsets A
   
   [space_borel]  Theorem
      
      ⊢ space borel = 𝕌(:real)
   
   [space_in_borel]  Theorem
      
      ⊢ 𝕌(:real) ∈ subsets borel
   
   
*)
end

HOL 4, Kananaskis-14