Theory borel

⊢ $AE = (λP. almost_everywhere lborel P)

⊢ Borel =
  (𝕌(:extreal),
   {B' |
    ∃B S.
      B' = IMAGE Normal B ∪ S ∧ B ∈ subsets borel ∧
      S ∈ {∅; {−∞}; {+∞}; {−∞; +∞}}})

⊢ ∀m P.
    almost_everywhere m P ⇔
    ∃N. null_set m N ∧ ∀x. x ∈ m_space m DIFF N ⇒ P x

⊢ ext_lborel = (space Borel,subsets Borel,lambda ∘ real_set)

⊢ ∀a b. a ≤ b ⇒ lambda0 (right_open_interval a b) = Normal (b − a)

⊢ (∀s. s ∈ subsets right_open_intervals ⇒ lambda s = lambda0 s) ∧
  measurable_space lborel = borel ∧ measure_space lborel

⊢ ∀m P. (AE x::m. P x) ⇔ ∃N. null_set m N ∧ {x | x ∈ m_space m ∧ ¬P x} ⊆ N

⊢ ∀m P s.
    measure_space m ∧ countable s ∧ (∀n. n ∈ s ⇒ AE x::m. P n x) ⇒
    AE x::m. ∀n. n ∈ s ⇒ P n x

⊢ ∀m P s.
    measure_space m ∧ (∃n. n ∈ s ∧ AE x::m. P n x) ⇒
    AE x::m. ∃n. n ∈ s ∧ P n x

⊢ ∀m P. (AE x::m. P x) ⇔ ∃N. null_set m N ∧ ∀x. x ∈ m_space m DIFF N ⇒ P x

⊢ ∀m P.
    measure_space m ∧ countable 𝕌(:'index) ⇒
    ((AE x::m. ∀i. P i x) ⇔ ∀i. AE x::m. P i x)

⊢ ∀N M P. null_set M N ⇒ {x | x ∈ m_space M ∧ ¬P x} ⊆ N ⇒ AE x::M. P x

⊢ ∀m P.
    complete_measure_space m ∧ (AE x::m. P x) ⇒
    {x | x ∈ m_space m ∧ P x} ∈ measurable_sets m

⊢ ∀m P Q.
    measure_space m ∧ (AE x::m. P x) ∧ (AE x::m. Q x) ⇒ AE x::m. P x ∧ Q x

⊢ ∀N M. null_set M N ⇒ AE x::M. x ∉ N

⊢ ∀m. measure_space m ⇒ AE x::m. T

⊢ ∀m P. (AE x::m. P x) ⇔ almost_everywhere m P

⊢ ∀m P Q.
    measure_space m ∧ ((AE x::m. P x) ∨ AE x::m. Q x) ⇒ AE x::m. P x ∨ Q x

⊢ ∀m P Q.
    (∀x. x ∈ m_space m ⇒ (P x ⇔ Q x)) ⇒ ((AE x::m. P x) ⇔ AE x::m. Q x)

⊢ ∀m f fae g gae.
    measure_space m ∧ (AE x::m. f x = fae x) ∧ (AE x::m. g x = gae x) ⇒
    AE x::m. f x + g x = fae x + gae x

⊢ ∀m f fae s.
    FINITE s ∧ measure_space m ∧ (∀n. n ∈ s ⇒ AE x::m. f n x = fae n x) ⇒
    AE x::m. ∑ (C f x) s = ∑ (C fae x) s

⊢ ∀m P.
    (AE x::m. P x) ⇔ ∃N. N ∈ null_set m ∧ {x | x ∈ m_space m ∧ x ∉ P} ⊆ N

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

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

⊢ ∀N M.
    measure_space M ∧ N ∈ measurable_sets M ⇒
    (null_set M N ⇔ AE x::M. ¬N x)

⊢ ∀N M. null_set M N ⇒ AE x::M. ¬N x

⊢ ∀m P Q. (AE x::m. P x) ∧ (∀x. x ∈ m_space m ∧ P x ⇒ Q x) ⇒ AE x::m. Q x

⊢ Borel × Borel =
  (𝕌(:extreal # extreal),
   {B' |
    ∃B S B1 B2 B3 B4.
      B' = IMAGE (λ(x,y). (Normal x,Normal y)) B ∪ S ∧
      B ∈ subsets (borel × borel) ∧
      S = {+∞} × B1 ∪ {−∞} × B2 ∪ B3 × {+∞} ∪ B4 × {−∞} ∧
      B1 ∈ subsets Borel ∧ B2 ∈ subsets Borel ∧ B3 ∈ subsets Borel ∧
      B4 ∈ subsets Borel})

⊢ {+∞} ∈ subsets Borel ∧ {−∞} ∈ subsets Borel

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

⊢ ∀c. {x | x < c} ∈ subsets Borel

⊢ ∀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 d. {x | c ≤ x ∧ x ≤ d} ∈ subsets Borel

⊢ ∀c d. {x | c ≤ x ∧ x < d} ∈ subsets Borel

⊢ ∀c. {x | c ≤ x} ∈ subsets Borel

⊢ ∅ ∈ subsets Borel

⊢ ∀s. FINITE s ⇒ s ∈ subsets Borel

⊢ ∀b. b ∈ subsets borel ⇒ IMAGE Normal b ∈ subsets Borel

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

⊢ ∀c d. {x | c < x ∧ x ≤ d} ∈ subsets Borel

⊢ ∀c d. {x | c < x ∧ x < d} ∈ subsets Borel

⊢ ∀c. {x | c < x} ∈ subsets Borel

⊢ ∀c. {x | x ≤ c} ∈ subsets Borel

⊢ ∀c. {x | x < c} ∈ subsets Borel

⊢ ∀c. {c} ∈ subsets Borel

⊢ ∀c. {x | x = c} ∈ subsets Borel

⊢ Borel = general_borel ext_euclidean

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

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

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

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

⊢ Borel = sigma 𝕌(:extreal) (IMAGE (λc. {x | x ≤ c}) 𝕌(:extreal))

⊢ ∀m P. measure_space m ∧ (∀x. x ∈ m_space m ⇒ P x) ⇒ AE x::m. P x

⊢ ∀f a.
    sigma_algebra a ⇒
    (f ∈ Borel_measurable a ⇔
     f ∈ (space a → 𝕌(:extreal)) ∧
     ∀c. {x | f x < Normal c} ∩ space a ∈ subsets a)

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

⊢ (λ(x,y). x * y) ∈ Borel_measurable (Borel × Borel)

⊢ ∀a X Y.
    sigma_algebra a ∧ X ∈ Borel_measurable a ∧ Y ∈ Borel_measurable a ⇒
    (λx. (X x,Y x)) ∈ measurable a (Borel × 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 p f.
    f ∈ Borel_measurable a ∧ 0 ≤ p ∧ p ≠ +∞ ⇒
    (λx. abs (f x) powr p) ∈ Borel_measurable a

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

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

⊢ ∀m f g.
    complete_measure_space m ∧ (AE x::m. f x = g x) ∧
    f ∈ Borel_measurable (measurable_space m) ⇒
    g ∈ Borel_measurable (measurable_space m)

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

⊢ ∀f a.
    sigma_algebra 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

⊢ ∀f a.
    sigma_algebra 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. {x | abs (f x) < c} ∩ space a ∈ subsets a) ∧
    (∀c. {x | c ≤ abs (f x)} ∩ space a ∈ subsets a) ∧
    (∀c. {x | abs (f x) ≤ c} ∩ space a ∈ subsets a) ∧
    (∀c. {x | c < abs (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) ∧
    (∀c. {x | abs (f x) = c} ∩ space a ∈ subsets a) ∧
    ∀c. {x | abs (f x) ≠ c} ∩ space a ∈ subsets a

⊢ ∀f m.
    sigma_algebra (measurable_space m) ∧
    f ∈ Borel_measurable (measurable_space 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

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space 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. {x | abs (f x) < c} ∩ m_space m ∈ measurable_sets m) ∧
    (∀c. {x | c ≤ abs (f x)} ∩ m_space m ∈ measurable_sets m) ∧
    (∀c. {x | abs (f x) ≤ c} ∩ m_space m ∈ measurable_sets m) ∧
    (∀c. {x | c < abs (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) ∧
    (∀c. {x | abs (f x) = c} ∩ m_space m ∈ measurable_sets m) ∧
    ∀c. {x | abs (f x) ≠ c} ∩ m_space m ∈ measurable_sets m

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    (∀c. {x | x ∈ m_space m ∧ f x < c} ∈ measurable_sets m) ∧
    (∀c. {x | x ∈ m_space m ∧ c ≤ f x} ∈ measurable_sets m) ∧
    (∀c. {x | x ∈ m_space m ∧ f x ≤ c} ∈ measurable_sets m) ∧
    (∀c. {x | x ∈ m_space m ∧ c < f x} ∈ measurable_sets m) ∧
    (∀c. {x | x ∈ m_space m ∧ abs (f x) < c} ∈ measurable_sets m) ∧
    (∀c. {x | x ∈ m_space m ∧ c ≤ abs (f x)} ∈ measurable_sets m) ∧
    (∀c. {x | x ∈ m_space m ∧ abs (f x) ≤ c} ∈ measurable_sets m) ∧
    (∀c. {x | x ∈ m_space m ∧ c < abs (f x)} ∈ measurable_sets m) ∧
    (∀c d. {x | x ∈ m_space m ∧ c ≤ f x ∧ f x < d} ∈ measurable_sets m) ∧
    (∀c d. {x | x ∈ m_space m ∧ c < f x ∧ f x ≤ d} ∈ measurable_sets m) ∧
    (∀c d. {x | x ∈ m_space m ∧ c ≤ f x ∧ f x ≤ d} ∈ measurable_sets m) ∧
    (∀c d. {x | x ∈ m_space m ∧ c < f x ∧ f x < d} ∈ measurable_sets m) ∧
    (∀c. {x | x ∈ m_space m ∧ f x = c} ∈ measurable_sets m) ∧
    (∀c. {x | x ∈ m_space m ∧ f x ≠ c} ∈ measurable_sets m) ∧
    (∀c. {x | x ∈ m_space m ∧ abs (f x) = c} ∈ measurable_sets m) ∧
    ∀c. {x | x ∈ m_space m ∧ abs (f x) ≠ c} ∈ measurable_sets m

⊢ ∀f a.
    sigma_algebra a ⇒
    (f ∈ Borel_measurable a ⇔
     f ∈ (space a → 𝕌(:extreal)) ∧
     ∀c. {x | Normal c ≤ f x} ∩ space a ∈ subsets a)

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

⊢ ∀f a.
    sigma_algebra a ⇒
    (f ∈ Borel_measurable a ⇔
     f ∈ (space a → 𝕌(:extreal)) ∧
     ∀c. {x | f x ≤ Normal c} ∩ space a ∈ subsets a)

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

⊢ ∀f a.
    sigma_algebra a ⇒
    (f ∈ Borel_measurable a ⇔
     f ∈ (space a → 𝕌(:extreal)) ∧
     ∀c. {x | Normal c < f x} ∩ space a ∈ subsets a)

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

⊢ ∀f a.
    sigma_algebra a ∧ (∀x. x ∈ space a ⇒ f x ≠ −∞) ⇒
    (f ∈ Borel_measurable a ⇔
     f ∈ (space a → 𝕌(:extreal)) ∧
     ∀c d. {x | Normal c ≤ f x ∧ f x < Normal d} ∩ space a ∈ subsets a)

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

⊢ ∀f a.
    sigma_algebra a ∧ (∀x. x ∈ space a ⇒ f x ≠ −∞) ⇒
    (f ∈ Borel_measurable a ⇔
     f ∈ (space a → 𝕌(:extreal)) ∧
     ∀c d. {x | Normal c < f x ∧ f x ≤ Normal d} ∩ space a ∈ subsets a)

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

⊢ ∀f a.
    sigma_algebra a ∧ (∀x. x ∈ space a ⇒ f x ≠ −∞) ⇒
    (f ∈ Borel_measurable a ⇔
     f ∈ (space a → 𝕌(:extreal)) ∧
     ∀c d. {x | Normal c ≤ f x ∧ f x ≤ Normal d} ∩ space a ∈ subsets a)

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

⊢ ∀f a.
    sigma_algebra a ∧ (∀x. x ∈ space a ⇒ f x ≠ −∞) ⇒
    (f ∈ Borel_measurable a ⇔
     f ∈ (space a → 𝕌(:extreal)) ∧
     ∀c d. {x | Normal c < f x ∧ f x < Normal d} ∩ space a ∈ subsets a)

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

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

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

⊢ abs ∈ Borel_measurable Borel

⊢ ∀p. 0 ≤ p ∧ p ≠ +∞ ⇒ (λx. abs x powr p) ∈ Borel_measurable Borel

⊢ numeric_negate ∈ Borel_measurable Borel

⊢ ∀c. (λx. c) ∈ Borel_measurable Borel

⊢ (λx. x) ∈ Borel_measurable Borel

⊢ ∀c. (λx. max x c) ∈ Borel_measurable Borel

⊢ ∀c. (λx. min x c) ∈ Borel_measurable Borel

⊢ ∀f. (∀x y. x ≤ y ⇒ f y ≤ f x) ⇒ f ∈ Borel_measurable Borel

⊢ ∀f. (∀x y. x ≤ y ⇒ f x ≤ f y) ⇒ f ∈ Borel_measurable Borel

⊢ ∀f. f ∈ borel_measurable borel ⇒
      (λx. Normal (f x)) ∈ Borel_measurable borel

⊢ ∀n. (λx. x pow n) ∈ Borel_measurable Borel

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

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

⊢ ∀a z s.
    sigma_algebra a ∧ s ∈ subsets a ⇒
    (λx. Normal z * 𝟙 s x) ∈ Borel_measurable a

⊢ ∀a c s.
    sigma_algebra a ∧ s ∈ subsets a ⇒ (λx. c * 𝟙 s x) ∈ Borel_measurable a

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

⊢ ∀a b f g h.
    f ∈ Borel_measurable b ∧ g ∈ measurable a b ∧
    (∀x. x ∈ space a ⇒ h x = f (g x)) ⇒
    h ∈ Borel_measurable a

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

⊢ ∀m f g.
    (∀x. x ∈ m_space m ⇒ f x = g x) ⇒
    (f ∈ Borel_measurable (measurable_space m) ⇔
     g ∈ Borel_measurable (measurable_space m))

⊢ ∀a f g.
    (∀x. x ∈ space a ⇒ f x = g x) ⇒
    (f ∈ Borel_measurable a ⇔ g ∈ Borel_measurable a)

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

⊢ ∀a k. sigma_algebra a ⇒ (λx. k) ∈ Borel_measurable a

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

⊢ ∀m f g.
    (∀x. x ∈ m_space m ⇒ f x = g x) ∧
    g ∈ Borel_measurable (measurable_space m) ⇒
    f ∈ Borel_measurable (measurable_space m)

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

⊢ ∀a f g.
    (∀x. x ∈ space a ⇒ f x = g x) ⇒
    (f ∈ Borel_measurable a ⇔ g ∈ Borel_measurable a)

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ Borel_measurable a ∧
    (∀x. x ∈ space a ⇒ g x = exp (f x)) ⇒
    g ∈ Borel_measurable a

⊢ ∀a f. sigma_algebra a ∧ f ∈ Borel_measurable a ⇒ f⁻ ∈ Borel_measurable a

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

⊢ ∀a b f.
    sigma_algebra a ∧ sigma_algebra b ∧ f ∈ Borel_measurable (a × b) ⇒
    (∀y. y ∈ space b ⇒ (λx. f (x,y)) ∈ Borel_measurable a) ∧
    ∀x. x ∈ space a ⇒ (λy. f (x,y)) ∈ Borel_measurable b

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

⊢ ∀f m.
    f ∈ borel_measurable (measurable_space m) ⇒
    Normal ∘ f ∈ Borel_measurable (measurable_space m)

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ borel_measurable a ⇒
    Normal ∘ f ∈ Borel_measurable a

⊢ ∀a A f.
    sigma_algebra a ∧ A ∈ subsets a ∧ (∀x. x ∈ space a ⇒ f x = 𝟙 A x) ⇒
    f ∈ Borel_measurable a

⊢ ∀a fi f X.
    sigma_algebra a ∧ X ≠ ∅ ∧ (∀n. n ∈ X ⇒ fi n ∈ Borel_measurable a) ∧
    (∀x. x ∈ space a ⇒ f x = inf (IMAGE (λn. fi n x) X)) ⇒
    f ∈ Borel_measurable a

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ Borel_measurable a ∧
    (∀x. x ∈ space a ⇒ g x = (f x)⁻¹ * 𝟙 {y | f y ≠ 0} x) ⇒
    g ∈ Borel_measurable 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 fi f.
    sigma_algebra a ∧ (∀n. fi n ∈ Borel_measurable a) ∧
    (∀x. x ∈ space a ⇒ f x = liminf (λi. fi i x)) ⇒
    f ∈ Borel_measurable a

⊢ ∀a fi f.
    sigma_algebra a ∧ (∀n. fi n ∈ Borel_measurable a) ∧
    (∀x. x ∈ space a ⇒ f x = limsup (λi. fi i x)) ⇒
    f ∈ Borel_measurable a

⊢ ∀f g a.
    sigma_algebra a ∧ f ∈ Borel_measurable a ∧ g ∈ Borel_measurable a ⇒
    {x | f x < g x} ∩ 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

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

⊢ ∀a f.
    sigma_algebra a ∧ (∀i. f i ∈ Borel_measurable a) ⇒
    ∀n. max_fn_seq f n ∈ 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

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

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

⊢ ∀f sp.
    (∀x y. x ≤ y ⇒ f y ≤ f x) ∧ sp ∈ subsets Borel ⇒
    f ∈ Borel_measurable (restrict_algebra Borel sp)

⊢ ∀f sp.
    (∀x y. x ≤ y ⇒ f x ≤ f y) ∧ sp ∈ subsets Borel ⇒
    f ∈ Borel_measurable (restrict_algebra Borel sp)

⊢ ∀fi f a.
    sigma_algebra a ∧ (∀n. fi n ∈ Borel_measurable a) ∧
    (∀x. x ∈ space a ⇒ f x = inf (IMAGE (λn. fi n x) 𝕌(:num))) ⇒
    f ∈ Borel_measurable a

⊢ ∀fi f a.
    sigma_algebra a ∧ (∀n. fi n ∈ Borel_measurable a) ∧
    (∀n x. x ∈ space a ⇒ fi n x ≤ fi (SUC n) x) ∧
    (∀x. x ∈ space a ⇒ f x = sup (IMAGE (λn. fi n x) 𝕌(:num))) ⇒
    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) ∧
    (∀x. x ∈ space a ⇒ f x ≠ −∞ ∧ f x ≠ +∞ ∧ g x ≠ −∞ ∧ g x ≠ +∞) ⇒
    h ∈ 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 * 𝟙 s x) ∈ Borel_measurable a

⊢ ∀a f.
    sigma_algebra a ⇒
    (f ∈ Borel_measurable a ⇔
     (λx. f x * 𝟙 (space a) x) ∈ Borel_measurable a)

⊢ ∀a f g h.
    sigma_algebra a ∧ f ∈ Borel_measurable a ∧ g ∈ Borel_measurable a ∧
    (∀x. x ∈ space a ∧ g x = 0 ⇒ f x = 0) ∧
    (∀x. x ∈ space a ⇒ h x = f x * (g x)⁻¹) ⇒
    h ∈ Borel_measurable a

⊢ ∀f a.
    sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
    {x | f x = −∞} ∩ space a ∈ subsets a

⊢ Normal ∈ Borel_measurable borel

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
    Normal ∘ real ∘ f ∈ Borel_measurable a

⊢ ∀f a.
    sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
    {x | f x ≠ −∞} ∩ space a ∈ subsets a

⊢ ∀f a.
    sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
    {x | f x ≠ +∞} ∩ space a ∈ subsets a

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

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

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

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

⊢ ∀a f.
    sigma_algebra a ⇒
    (f ∈ Borel_measurable a ⇔
     f⁺ ∈ Borel_measurable a ∧ f⁻ ∈ Borel_measurable a)

⊢ ∀f a.
    sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
    {x | f x = +∞} ∩ space a ∈ subsets a

⊢ ∀n a f. f ∈ Borel_measurable a ⇒ (λx. f x pow n) ∈ Borel_measurable a

⊢ ∀n a 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 h.
    sigma_algebra a ∧ f ∈ Borel_measurable a ∧
    (∀n. {x | g x = n} ∩ space a ∈ subsets a) ∧
    (∀x. x ∈ space a ⇒ h x = f x pow g x) ⇒
    h ∈ Borel_measurable a

⊢ ∀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 ≠ −∞ ∧ f i x ≠ +∞) ∧
    (∀x. x ∈ space a ⇒ g x = ∏ (λi. f i x) s) ⇒
    g ∈ 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 = ∏ (λi. f i x) s) ⇒
    g ∈ Borel_measurable a

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

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

⊢ ∀f a.
    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 ∧
    (∀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 ⇒ f x ≠ −∞ ∧ g x ≠ +∞ ∨ f x ≠ +∞ ∧ g x ≠ −∞) ∧
    (∀x. x ∈ space a ⇒ h x = f x − g x) ⇒
    h ∈ 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) ∧
    (∀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

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

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

⊢ ∀a fi f X.
    sigma_algebra a ∧ X ≠ ∅ ∧ (∀n. n ∈ X ⇒ fi n ∈ Borel_measurable a) ∧
    (∀x. x ∈ space a ⇒ f x = sup (IMAGE (λn. fi n x) X)) ⇒
    f ∈ Borel_measurable a

⊢ ∀m f g h.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    g ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ h x = f x * g x) ⇒
    h ∈ Borel_measurable (measurable_space m)

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

⊢ ∀top1 top2 f.
    continuous_map (top1,top2) f ⇒
    f ∈ measurable (general_borel top1) (general_borel top2)

⊢ ∀f a.
    sigma_algebra a ⇒
    (f ∈ Borel_measurable a ⇔
     f ∈ (space a → 𝕌(:extreal)) ∧
     ∀c. PREIMAGE f {x | x < Normal c} ∩ space a ∈ subsets a)

⊢ ∀m P Q. measure_space m ⇒ (P ⇒ (AE x::m. Q x) ⇔ AE x::m. P ⇒ Q x)

⊢ ∀m P Q.
    measure_space m ⇒
    ((∀i. P i ⇒ AE x::m. Q i x) ⇔ ∀i. AE x::m. P i ⇒ Q i x)

⊢ sigma_algebra Borel

⊢ sigma_algebra (Borel × Borel)

⊢ space Borel = 𝕌(:extreal)

⊢ space (Borel × Borel) = 𝕌(:extreal # extreal)

⊢ borel = (𝕌(:real),IMAGE real_set (subsets Borel))

⊢ ∀s. s ∈ subsets Borel ⇒ IMAGE real s ∈ subsets borel

⊢ ∀s. s ∈ subsets Borel ⇒ real_set s ∈ subsets borel

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
    real ∘ f ∈ borel_measurable a

⊢ ∀m f.
    measure_space m ∧
    (∀s. open s ⇒ PREIMAGE f s ∩ m_space m ∈ measurable_sets m) ⇒
    f ∈ borel_measurable (measurable_space m)

⊢ ∀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 (measurable_space m) (sigma sp N)

⊢ lambda0 ∅ = 0

⊢ ∀a b.
    lambda0 (right_open_interval a b) ≠ +∞ ∧
    lambda0 (right_open_interval a b) ≠ −∞

⊢ ∀a b. a ≤ b ⇒ lambda (interval [(a,b)]) = Normal (b − a)

⊢ ∀a b. lambda (interval [(a,b)]) = Normal (content (interval [(a,b)]))

⊢ ∀c. countable c ⇒ lambda c = 0

⊢ lambda ∅ = 0

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

⊢ ∀c. FINITE c ⇒ lambda c = 0

⊢ ∀a b.
    lambda (right_open_interval a b) ≠ +∞ ∧
    lambda (right_open_interval a b) ≠ −∞

⊢ ∀a b. a ≤ b ⇒ lambda (interval (a,b)) = Normal (b − a)

⊢ ∀a b. a ≤ b ⇒ lambda (right_open_interval a b) = Normal (b − a)

⊢ ∀c. lambda {c} = 0

⊢ lambda 𝕌(:real) = +∞

⊢ additive lborel0

⊢ finite_additive lborel0

⊢ positive lborel0

⊢ premeasure lborel0

⊢ subadditive lborel0

⊢ ∀M. (∀a b.
         measure M (interval [(a,b)]) = Normal (content (interval [(a,b)]))) ∧
      measure_space M ∧ measurable_sets M = subsets borel ⇒
      measure_of lborel = measure_of M

⊢ m_space lborel = space borel

⊢ measure_space ext_lborel

⊢ measure_space lborel

⊢ open_in ext_euclidean {−∞; +∞}

⊢ open_in ext_euclidean {−∞}

⊢ open_in ext_euclidean {+∞}

⊢ real ∈ borel_measurable Borel

⊢ measurable_sets lborel = subsets borel

⊢ sigma_finite ext_lborel

⊢ sigma_finite lborel

⊢ m_space lborel = 𝕌(:real)