Theory real_borel

⊢ borel = sigma 𝕌(:real) {s | open s}

⊢ ∀a b. box a b = {x | a < x ∧ x < b}

⊢ ∀n. line n = {x | -&n ≤ x ∧ x ≤ &n}

⊢ ∀f x. fn_minus f x = -min 0 (f x)

⊢ ∀f x. f⁺ x = max 0 (f x)

⊢ ∀a b. right_open_interval a b = {x | a ≤ x ∧ x < b}

⊢ right_open_intervals = (𝕌(:real),{right_open_interval a b | T})

⊢ ∀n. ball (0,&n) ⊆ line n

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ (ℚ → subsets a) ⇒
    BIGUNION (IMAGE f ℚ) ∈ subsets a

⊢ ∀s. bounded s ⇒ ∃n. s ⊆ line n

⊢ ∀a b c d.
    c < d ⇒ IMAGE FST (interval (a,b) × interval (c,d)) = interval (a,b)

⊢ ∀a b c d.
    a < b ⇒ IMAGE SND (interval (a,b) × interval (c,d)) = interval (c,d)

⊢ ∀x n. x ∈ line n ⇔ -&n ≤ x ∧ x ≤ &n

⊢ ∀a b. ∃n. interval [(a,b)] ⊆ line n

⊢ ∀n N. n ≤ N ⇒ line n ⊆ line N

⊢ ∀n N. line n ⊆ line N ⇔ n ≤ N

⊢ ∀n. line n ⊆ line (SUC n)

⊢ ∀c. COMPL {x | c < x} = {x | x ≤ c}

⊢ ∀c. COMPL {x | c ≤ x} = {x | x < c}

⊢ ∀c. COMPL {x | x ≤ c} = {x | c < x}

⊢ ∀c. COMPL {x | x < c} = {x | c ≤ x}

⊢ ∀x. ∃n. x ∈ line n

⊢ ∀c. {c} =
      BIGINTER
        (IMAGE (λn. {x | c − (1 / 2) pow n ≤ x ∧ x < c + (1 / 2) pow n})
           𝕌(:num))

⊢ borel × borel = sigma 𝕌(:real # real) {s | open_in (mtop mr2) s}

⊢ borel × borel = sigma 𝕌(:real # real) {box a b × box c d | T}

⊢ (λ(x,y). x + y) ∈ borel_measurable (borel × borel)

⊢ (λ(x,y). x − y) ∈ borel_measurable (borel × borel)

⊢ borel = general_borel euclidean

⊢ ∀A. closed A ⇒ A ∈ subsets borel

⊢ ∀A. A ∈ subsets borel ⇒ 𝕌(:real) DIFF A ∈ subsets borel

⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | x ≤ a}) 𝕌(:real))

⊢ borel = sigma 𝕌(:real) (IMAGE (λ(a,b). box a b) 𝕌(:real # real))

⊢ borel =
  sigma 𝕌(:real) (IMAGE (λ(a,b). {x | a ≤ x ∧ x ≤ b}) 𝕌(:real # real))

⊢ borel =
  sigma 𝕌(:real) (IMAGE (λ(a,b). {x | a ≤ x ∧ x < b}) 𝕌(:real # real))

⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | a < x}) 𝕌(:real))

⊢ borel =
  sigma 𝕌(:real) (IMAGE (λ(a,b). {x | a < x ∧ x ≤ b}) 𝕌(:real # real))

⊢ borel =
  sigma 𝕌(:real) (IMAGE (λ(a,b). {x | a < x ∧ x < b}) 𝕌(:real # real))

⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | x ≤ a}) 𝕌(:real))

⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | x < a}) 𝕌(:real))

⊢ ∀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)

⊢ ∀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)

⊢ ∀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)

⊢ ∀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 𝕌(:γ))

⊢ ∀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) 𝕌(:β # γ))

⊢ ∀s. frontier s ∈ subsets borel

⊢ ∀s. fsigma s ⇒ s ∈ subsets borel

⊢ ∀s. gdelta s ⇒ s ∈ subsets borel

⊢ ∀n. line n ∈ subsets borel

⊢ ∀M c. sigma_algebra M ⇒ (λx. c) ∈ borel_measurable M

⊢ ∀f M x. f ∈ borel_measurable M ⇒ PREIMAGE f {x} ∩ space M ∈ subsets M

⊢ ∀s a.
    sigma_algebra s ∧ a ∈ subsets s ⇒ indicator_fn a ∈ borel_measurable s

⊢ (∀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

⊢ ∀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. {x | a < x} ∈ subsets borel

⊢ ∀a b. {x | a < x ∧ x ≤ b} ∈ subsets borel

⊢ ∀a b. {x | a < x ∧ x < b} ∈ subsets borel

⊢ ∀a. {x | x ≤ a} ∈ subsets borel

⊢ ∀a. {x | x < a} ∈ subsets borel

⊢ ∀c. {x | x ≠ c} ∈ subsets borel

⊢ ∀c. {c} ∈ subsets borel

⊢ ∀A. open A ⇒ A ∈ subsets borel

⊢ ∀A. A ⊆ subsets borel ⇒ sigma_sets 𝕌(:real) A ⊆ subsets borel

⊢ ∀A x. A ∈ subsets borel ⇒ x INSERT A ∈ subsets borel

⊢ ∀a b. box a b = interval (a,b)

⊢ ∀a b c d. open_in (mtop mr2) (interval (a,b) × interval (c,d))

⊢ ∀a b c d.
    a < b ∧ c < d ⇒ (interval [(a,b)] = interval [(c,d)] ⇔ a = c ∧ b = d)

⊢ ∀a b c d.
    a < b ∧ c < d ⇒
    (DISJOINT (interval (a,b)) (interval (c,d)) ⇔ b ≤ c ∨ d ≤ a)

⊢ ∀a b c d.
    a < b ∧ c < d ∧ interval [(a,b)] ⊆ interval [(c,d)] ⇒ b − a ≤ d − c

⊢ ∀a b c d.
    a < b ∧ c < d ⇒ (interval [(a,b)] ⊆ interval [(c,d)] ⇔ c ≤ a ∧ b ≤ d)

⊢ ∀c. countable c ⇒ c ∈ subsets borel

⊢ ∀c. FINITE c ⇒ c ∈ subsets borel

⊢ ∀f. abs ∘ f = (λx. f⁺ x + fn_minus f x)

⊢ ∀f x. abs (f x) = f⁺ x + fn_minus f x

⊢ ∀f x. f x = f⁺ x − fn_minus f x

⊢ ∀a. {(x,y) | a < x * y} ∈ {s | open_in (mtop mr2) s}

⊢ ∀f s.
    f ∈ borel_measurable s ⇔
    ∀s'.
      s' ∈ subsets (sigma 𝕌(:real) (IMAGE (λa. {x | x ≤ a}) 𝕌(:real))) ⇒
      PREIMAGE f s' ∩ space s ∈ subsets s

⊢ (λx. x) ∈ borel_measurable borel

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ g x = abs (f x)) ⇒
    g ∈ borel_measurable a

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ borel_measurable a ⇒ abs ∘ f ∈ borel_measurable a

⊢ ∀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

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ borel_measurable a ⇒
    (λx. -f x) ∈ borel_measurable a

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ g x = -f x) ⇒
    g ∈ borel_measurable a

⊢ ∀f M.
    f ∈ borel_measurable M ⇔
    ∀s. s ∈ subsets borel ⇒ PREIMAGE f s ∩ space M ∈ subsets M

⊢ abs ∈ borel_measurable borel

⊢ ∀a f g z.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ g x = z * f x) ⇒
    g ∈ borel_measurable a

⊢ ∀a k f.
    sigma_algebra a ∧ (∀x. x ∈ space a ⇒ f x = k) ⇒ f ∈ borel_measurable a

⊢ ∀f. f continuous_on 𝕌(:real) ⇒ f ∈ borel_measurable borel

⊢ ∀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

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ borel_measurable a ⇒
    fn_minus f ∈ borel_measurable a

⊢ ∀a f. sigma_algebra a ∧ f ∈ borel_measurable a ⇒ f⁺ ∈ borel_measurable a

⊢ ∀f m.
    sigma_algebra m ⇒
    (f ∈ borel_measurable m ⇔
     f ∈ (space m → 𝕌(:real)) ∧ ∀a. {w | w ∈ space m ∧ a ≤ f w} ∈ subsets m)

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ borel_measurable a ⇒
    ∀c. {x | c ≤ f x} ∩ space a ∈ subsets a

⊢ ∀A f a b.
    sigma_algebra A ∧ f ∈ borel_measurable A ⇒
    {x | x ∈ space A ∧ a ≤ f x ∧ f x < b} ∈ subsets A

⊢ ∀f m.
    sigma_algebra m ⇒
    (f ∈ borel_measurable m ⇔
     f ∈ (space m → 𝕌(:real)) ∧ ∀a. {w | w ∈ space m ∧ a < f w} ∈ subsets m)

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ borel_measurable a ⇒
    ∀c. {x | c < f x} ∩ space a ∈ subsets a

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ g x = (f x)⁻¹) ⇒
    g ∈ borel_measurable a

⊢ ∀f m.
    sigma_algebra m ⇒
    (f ∈ borel_measurable m ⇔
     f ∈ (space m → 𝕌(:real)) ∧ ∀a. {w | w ∈ space m ∧ f w ≤ a} ∈ subsets m)

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ⇒
    {x | x ∈ space a ∧ f x ≤ g x} ∈ subsets a

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ⇒
    {x | f x ≤ g x} ∩ space a ∈ subsets a

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ borel_measurable a ⇒
    ∀c. {x | f x ≤ c} ∩ space a ∈ subsets a

⊢ ∀f m.
    sigma_algebra m ⇒
    (f ∈ borel_measurable m ⇔
     f ∈ (space m → 𝕌(:real)) ∧ ∀a. {w | w ∈ space m ∧ f w < a} ∈ subsets m)

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ⇒
    {x | x ∈ space a ∧ f x < g x} ∈ subsets a

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ⇒
    {x | f x < g x} ∩ space a ∈ subsets a

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ borel_measurable a ⇒
    ∀c. {x | f x < c} ∩ space a ∈ subsets a

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ⇒
    (λx. max (f x) (g x)) ∈ borel_measurable a

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ⇒
    (λx. min (f x) (g x)) ∈ borel_measurable a

⊢ ∀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

⊢ ∀a f s.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧ s ∈ subsets a ⇒
    (λx. f x * indicator_fn s x) ∈ borel_measurable a

⊢ ∀f M.
    f ∈ borel_measurable M ⇔
    ∀s. s ∈ subsets (sigma 𝕌(:real) {s | open s}) ⇒
        PREIMAGE f s ∩ space M ∈ subsets M

⊢ ∀a f.
    sigma_algebra a ∧ (∀s. open s ⇒ PREIMAGE f s ∩ space a ∈ subsets a) ⇒
    f ∈ borel_measurable a

⊢ ∀a n f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ g x = f x pow n) ⇒
    g ∈ borel_measurable a

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ g x = (f x)²) ⇒
    g ∈ borel_measurable a

⊢ ∀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

⊢ ∀a f g s.
    FINITE s ∧ sigma_algebra a ∧ (∀i. i ∈ s ⇒ f i ∈ borel_measurable a) ∧
    (∀x. x ∈ space a ⇒ g x = SIGMA (λi. f i x) s) ⇒
    g ∈ borel_measurable a

⊢ abs ∈ borel_measurable borel

⊢ numeric_negate ∈ borel_measurable borel

⊢ exp ∈ borel_measurable borel

⊢ ∀a f g h.
    f ∈ borel_measurable borel ∧ g ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ h x = f (g x)) ⇒
    h ∈ borel_measurable a

⊢ ∀a f g.
    (∀x. x ∈ space a ⇒ f x = g x) ∧ g ∈ borel_measurable a ⇒
    f ∈ borel_measurable a

⊢ ∀f a.
    sigma_algebra a ∧ f ∈ borel_measurable a ⇒
    ∀c. {x | f x ≠ c} ∩ space a ∈ subsets a

⊢ ∀a sp N f.
    sigma_algebra a ∧ N ⊆ POW sp ∧ f ∈ (space a → sp) ∧
    (∀y. y ∈ N ⇒ PREIMAGE f y ∩ space a ∈ subsets a) ⇒
    f ∈ measurable a (sigma sp N)

⊢ ∀a b x. x ∈ right_open_interval a b ⇔ a ≤ x ∧ x < b

⊢ ∀s. s ∈ subsets right_open_intervals ⇔ ∃a b. s = right_open_interval a b

⊢ ∀s. s ≠ ∅ ∧ s ∈ subsets right_open_intervals ⇔
      ∃a b. a < b ∧ s = right_open_interval a b

⊢ ∀n. closed (line n)

⊢ ∀n. line n = interval [(-&n,&n)]

⊢ ∀M. open M ⇒ M = BIGUNION {box a b | box a b ⊆ M}

⊢ ∀M. open M ⇒ M = BIGUNION {box a b | a ∈ ℚ ∧ b ∈ ℚ ∧ box a b ⊆ M}

⊢ ∀x e. 0 < e ⇒ ∃a b. a ∈ ℚ ∧ b ∈ ℚ ∧ x ∈ box a b ∧ box a b ⊆ ball (x,e)

⊢ fn_minus f = (λx. -min 0 (f x))

⊢ ∀f x. 0 ≤ fn_minus f x

⊢ ∀f. f⁺ = (λx. max 0 (f x))

⊢ ∀f x. 0 ≤ f⁺ x

⊢ ∀a b c d.
    a < b ∧ c < d ⇒
    (right_open_interval a b = right_open_interval c d ⇔ a = c ∧ b = d)

⊢ ∀a b c d.
    a ≤ b ∧ b ≤ c ∧ c ≤ d ⇒
    DISJOINT (right_open_interval a b) (right_open_interval c d)

⊢ ∀a b c d.
    a < b ∧ c < d ⇒
    (DISJOINT (right_open_interval a b) (right_open_interval c d) ⇔
     b ≤ c ∨ d ≤ a)

⊢ ∀a b c d.
    a < b ∧ c < d ∧
    DISJOINT (right_open_interval a b) (right_open_interval c d) ⇒
    b ≤ c ∨ d ≤ a

⊢ ∀a b c d.
    a < b ∧ c < d ∧ right_open_interval a b ⊆ right_open_interval c d ⇒
    b − a ≤ d − c

⊢ ∀a b c d.
    a < b ∧ c < d ⇒
    (right_open_interval a b ⊆ right_open_interval c d ⇔ c ≤ a ∧ b ≤ d)

⊢ ∀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)

⊢ ∀a b c d.
    a ≤ b ∧ b ≤ c ∧ c ≤ d ⇒
    disjoint {right_open_interval a b; right_open_interval c d}

⊢ ∀a b. right_open_interval a b = ∅ ⇔ ¬(a < b)

⊢ ∀a b. a = b ⇒ right_open_interval a b = ∅

⊢ ∀a b. a < b ⇒ frontier (right_open_interval a b) = {a; b}

⊢ ∀a b. right_open_interval a b ∈ subsets right_open_intervals

⊢ ∀a b c d.
    right_open_interval a b ∩ right_open_interval c d =
    right_open_interval (max a c) (min b d)

⊢ ∀a b. a < b ⇒ a ∈ right_open_interval a b

⊢ ∀a b. a < b ⇒ interval_lowerbound (right_open_interval a b) = a

⊢ ∀c. IMAGE (λx. x + c) (right_open_interval a b) =
      right_open_interval (a + c) (b + c)

⊢ ∀s c.
    s ⊆ right_open_interval 0 1 ⇒
    IMAGE (λx. x + c) s ⊆ right_open_interval c (c + 1)

⊢ ∀a b.
    interval_lowerbound (right_open_interval a b) ≤
    interval_upperbound (right_open_interval a b)

⊢ ∀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)

⊢ ∀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

⊢ ∀a b. a < b ⇒ interval_upperbound (right_open_interval a b) = b

⊢ semiring right_open_intervals

⊢ sigma (space right_open_intervals) (subsets right_open_intervals) = borel

⊢ subsets right_open_intervals ⊆ subsets borel

⊢ sigma_algebra borel

⊢ sigma_algebra (borel × borel)

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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 = 𝕌(:real)

⊢ space (borel × borel) = 𝕌(:real # real)

⊢ 𝕌(:real) ∈ subsets borel