Theory "borel"

Signature

Definitions

AE_def

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

Borel

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

almost_everywhere_def

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

ext_lborel_def

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

fn_minus_def

⊢ ∀f. f⁻ = (λx. if f x < 0 then -f x else 0)

fn_plus_def

⊢ ∀f. f⁺ = (λx. if 0 < f x then f x else 0)

indicator_fn_def

⊢ ∀s. 𝟙 s = (λx. if x ∈ s then 1 else 0)

lambda0_def

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

lborel_def

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

lebesgue_def

⊢ lebesgue =
  (𝕌(:real),{A | ∀n. indicator A integrable_on line n},
   (λA. sup {Normal (∫ (line n) (indicator A)) | n ∈ 𝕌(:num)}))

nonneg_def

⊢ ∀f. nonneg f ⇔ ∀x. 0 ≤ f x

set_liminf_def

⊢ ∀E. liminf E = BIGUNION (IMAGE (λm. BIGINTER {E n | m ≤ n}) 𝕌(:num))

set_limsup_def

⊢ ∀E. limsup E = BIGINTER (IMAGE (λm. BIGUNION {E n | m ≤ n}) 𝕌(:num))

Theorems

AE_ALT

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

AE_I

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

AE_IMP_MEASURABLE_SETS

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

AE_NOT_IN

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

AE_THM

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

AE_all_S

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

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

⊢ ∀P. (AE x. P x) ⇔ AE x::lebesgue. P x

AE_filter

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

AE_iff_measurable

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

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

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

AE_impl

⊢ ∀P M Q. measure_space M ⇒ (P ⇒ AE x::M. Q x) ⇒ AE x::M. (λx. P ⇒ Q x) x

AE_not_in

⊢ ∀N M. null_set M N ⇒ AE x::M. {x | ¬N x} x

BOREL_MEASURABLE_INFINITY

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

BOREL_MEASURABLE_SETS

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

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

BOREL_MEASURABLE_SETS10

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

BOREL_MEASURABLE_SETS2

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

BOREL_MEASURABLE_SETS3

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

BOREL_MEASURABLE_SETS4

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

BOREL_MEASURABLE_SETS5

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

BOREL_MEASURABLE_SETS6

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

BOREL_MEASURABLE_SETS7

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

BOREL_MEASURABLE_SETS8

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

BOREL_MEASURABLE_SETS9

⊢ ∀c. {c} ∈ subsets Borel

BOREL_MEASURABLE_SETS_CC

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

BOREL_MEASURABLE_SETS_CO

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

BOREL_MEASURABLE_SETS_CR

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

BOREL_MEASURABLE_SETS_FINITE

⊢ ∀s. FINITE s ⇒ s ∈ subsets Borel

BOREL_MEASURABLE_SETS_NOT_SING

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

BOREL_MEASURABLE_SETS_OC

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

BOREL_MEASURABLE_SETS_OO

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

BOREL_MEASURABLE_SETS_OR

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

BOREL_MEASURABLE_SETS_RC

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

BOREL_MEASURABLE_SETS_RO

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

BOREL_MEASURABLE_SETS_SING

⊢ ∀c. {c} ∈ subsets Borel

BOREL_MEASURABLE_SETS_SING'

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

Borel_def

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

Borel_eq_ge

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

Borel_eq_gr

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

Borel_eq_le

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

FN_ABS

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

FN_ABS'

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

FN_DECOMP

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

FN_DECOMP'

⊢ ∀f. f = (λx. f⁺ x − f⁻ x)

FN_MINUS_ABS_ZERO

⊢ ∀f. (abs ∘ f)⁻ = (λx. 0)

FN_MINUS_ADD_LE

⊢ ∀f g x.
    f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞ ⇒
    (λx. f x + g x)⁻ x ≤ f⁻ x + g⁻ x

FN_MINUS_ALT

⊢ ∀f. f⁻ = (λx. -min (f x) 0)

FN_MINUS_ALT'

⊢ ∀f. f⁻ = (λx. -min 0 (f x))

FN_MINUS_CMUL

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

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

⊢ ∀f c. (∀x. 0 ≤ c x) ⇒ ((λx. c x * f x)⁻ = (λx. c x * f⁻ x))

FN_MINUS_INFTY_IMP

⊢ ∀f x. (f⁻ x = +∞) ⇒ (f⁺ x = 0)

FN_MINUS_LE_ABS

⊢ ∀f x. f⁻ x ≤ abs (f x)

FN_MINUS_NOT_INFTY

⊢ ∀f. (∀x. f x ≠ −∞) ⇒ ∀x. f⁻ x ≠ +∞

FN_MINUS_NOT_INFTY'

⊢ ∀f x. f x ≠ −∞ ⇒ f⁻ x ≠ +∞

FN_MINUS_POS

⊢ ∀g x. 0 ≤ g⁻ x

FN_MINUS_POS_ZERO

⊢ ∀g. (∀x. 0 ≤ g x) ⇒ (g⁻ = (λx. 0))

FN_MINUS_REDUCE

⊢ ∀f x. 0 ≤ f x ⇒ (f⁻ x = 0)

FN_MINUS_TO_PLUS

⊢ ∀f. (λx. -f x)⁻ = f⁺

FN_MINUS_ZERO

⊢ (λx. 0)⁻ = (λx. 0)

FN_PLUS_ABS_SELF

⊢ ∀f. (abs ∘ f)⁺ = abs ∘ f

FN_PLUS_ADD_LE

⊢ ∀f g x. (λx. f x + g x)⁺ x ≤ f⁺ x + g⁺ x

FN_PLUS_ALT

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

FN_PLUS_ALT'

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

FN_PLUS_CMUL

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

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

⊢ ∀f c. (∀x. 0 ≤ c x) ⇒ ((λx. c x * f x)⁺ = (λx. c x * f⁺ x))

FN_PLUS_INFTY_IMP

⊢ ∀f x. (f⁺ x = +∞) ⇒ (f⁻ x = 0)

FN_PLUS_LE_ABS

⊢ ∀f x. f⁺ x ≤ abs (f x)

FN_PLUS_NEG_ZERO

⊢ ∀g. (∀x. g x ≤ 0) ⇒ (g⁺ = (λx. 0))

FN_PLUS_NOT_INFTY

⊢ ∀f. (∀x. f x ≠ +∞) ⇒ ∀x. f⁺ x ≠ +∞

FN_PLUS_NOT_INFTY'

⊢ ∀f x. f x ≠ +∞ ⇒ f⁺ x ≠ +∞

FN_PLUS_POS

⊢ ∀g x. 0 ≤ g⁺ x

FN_PLUS_POS_ID

⊢ ∀g. (∀x. 0 ≤ g x) ⇒ (g⁺ = g)

FN_PLUS_REDUCE

⊢ ∀f x. 0 ≤ f x ⇒ (f⁺ x = f x)

FN_PLUS_TO_MINUS

⊢ ∀f. (λx. -f x)⁺ = f⁻

FN_PLUS_ZERO

⊢ (λx. 0)⁺ = (λx. 0)

FORALL_IMP_AE

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

INDICATOR_FN_ABS

⊢ ∀s. abs ∘ 𝟙 s = 𝟙 s

INDICATOR_FN_ABS_MUL

⊢ ∀f s. abs ∘ (λx. f x * 𝟙 s x) = (λx. (abs ∘ f) x * 𝟙 s x)

INDICATOR_FN_CROSS

⊢ ∀s t x y. 𝟙 (s × t) (x,y) = 𝟙 s x * 𝟙 t y

INDICATOR_FN_DIFF

⊢ ∀A B. 𝟙 (A DIFF B) = (λt. 𝟙 A t − 𝟙 (A ∩ B) t)

INDICATOR_FN_DIFF_SPACE

⊢ ∀A B sp. A ⊆ sp ∧ B ⊆ sp ⇒ (𝟙 (A ∩ (sp DIFF B)) = (λt. 𝟙 A t − 𝟙 (A ∩ B) t))

INDICATOR_FN_EMPTY

⊢ ∀x. 𝟙 ∅ x = 0

INDICATOR_FN_FCP_CROSS

⊢ ∀s t x y.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
    (𝟙 (fcp_cross s t) (FCP_CONCAT x y) = 𝟙 s x * 𝟙 t y)

INDICATOR_FN_INTER

⊢ ∀A B. 𝟙 (A ∩ B) = (λt. 𝟙 A t * 𝟙 B t)

INDICATOR_FN_INTER_MIN

⊢ ∀A B. 𝟙 (A ∩ B) = (λt. min (𝟙 A t) (𝟙 B t))

INDICATOR_FN_LE_1

⊢ ∀s x. 𝟙 s x ≤ 1

INDICATOR_FN_MONO

⊢ ∀s t x. s ⊆ t ⇒ 𝟙 s x ≤ 𝟙 t x

INDICATOR_FN_MUL_INTER

⊢ ∀A B. (λt. 𝟙 A t * 𝟙 B t) = (λt. 𝟙 (A ∩ B) t)

INDICATOR_FN_NOT_INFTY

⊢ ∀s x. 𝟙 s x ≠ −∞ ∧ 𝟙 s x ≠ +∞

INDICATOR_FN_POS

⊢ ∀s x. 0 ≤ 𝟙 s x

INDICATOR_FN_SING_0

⊢ ∀x y. x ≠ y ⇒ (𝟙 {x} y = 0)

INDICATOR_FN_SING_1

⊢ ∀x y. (x = y) ⇒ (𝟙 {x} y = 1)

INDICATOR_FN_UNION

⊢ ∀A B. 𝟙 (A ∪ B) = (λt. 𝟙 A t + 𝟙 B t − 𝟙 (A ∩ B) t)

INDICATOR_FN_UNION_MAX

⊢ ∀A B. 𝟙 (A ∪ B) = (λt. max (𝟙 A t) (𝟙 B t))

INDICATOR_FN_UNION_MIN

⊢ ∀A B. 𝟙 (A ∪ B) = (λt. min (𝟙 A t + 𝟙 B t) 1)

IN_LIMINF

⊢ ∀A x. x ∈ liminf A ⇔ ∃m. ∀n. m ≤ n ⇒ x ∈ A n

IN_LIMSUP

⊢ ∀A x. x ∈ limsup A ⇔ ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ x ∈ A n

IN_MEASURABLE_BOREL

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

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

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

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

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

IN_MEASURABLE_BOREL_ADD

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

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

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

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

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

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

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

IN_MEASURABLE_BOREL_ALT2

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

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

IN_MEASURABLE_BOREL_ALT3

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

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

IN_MEASURABLE_BOREL_ALT4

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

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

IN_MEASURABLE_BOREL_ALT5

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

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

IN_MEASURABLE_BOREL_ALT6

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

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

IN_MEASURABLE_BOREL_ALT7

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

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

IN_MEASURABLE_BOREL_ALT8

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

IN_MEASURABLE_BOREL_ALT9

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

IN_MEASURABLE_BOREL_BOREL_ABS

⊢ abs ∈ Borel_measurable Borel

IN_MEASURABLE_BOREL_BOREL_I

⊢ (λx. x) ∈ Borel_measurable Borel

IN_MEASURABLE_BOREL_CC

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

IN_MEASURABLE_BOREL_CMUL

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

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

IN_MEASURABLE_BOREL_CMUL_INDICATOR'

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

IN_MEASURABLE_BOREL_CO

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

IN_MEASURABLE_BOREL_CONST

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

IN_MEASURABLE_BOREL_CONST'

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

IN_MEASURABLE_BOREL_CR

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

IN_MEASURABLE_BOREL_EQ

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

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

IN_MEASURABLE_BOREL_FN_MINUS

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

IN_MEASURABLE_BOREL_FN_PLUS

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

IN_MEASURABLE_BOREL_IMP

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

IN_MEASURABLE_BOREL_IMP_BOREL

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

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

IN_MEASURABLE_BOREL_INDICATOR

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

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

IN_MEASURABLE_BOREL_LT

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

IN_MEASURABLE_BOREL_MAX

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

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

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

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

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

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

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

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

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

IN_MEASURABLE_BOREL_NEGINF

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

IN_MEASURABLE_BOREL_NOT_NEGINF

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

IN_MEASURABLE_BOREL_NOT_POSINF

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

IN_MEASURABLE_BOREL_NOT_SING

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

IN_MEASURABLE_BOREL_OC

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

IN_MEASURABLE_BOREL_OO

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

IN_MEASURABLE_BOREL_OR

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

IN_MEASURABLE_BOREL_PLUS_MINUS

⊢ ∀a f.
    f ∈ Borel_measurable a ⇔ f⁺ ∈ Borel_measurable a ∧ f⁻ ∈ Borel_measurable a

IN_MEASURABLE_BOREL_POSINF

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

IN_MEASURABLE_BOREL_POW

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

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

IN_MEASURABLE_BOREL_RO

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

IN_MEASURABLE_BOREL_SING

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

IN_MEASURABLE_BOREL_SQR

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

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

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

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

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

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

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

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

⊢ measure_space ext_lborel

SIGMA_ALGEBRA_BOREL

⊢ sigma_algebra Borel

SIGMA_ALGEBRA_BOREL_2D

⊢ sigma_algebra (Borel × Borel)

SIGMA_FINITE_LBOREL

⊢ sigma_finite ext_lborel

SPACE_BOREL

⊢ space Borel = 𝕌(:extreal)

SPACE_BOREL_2D

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

absolutely_integrable_on_indicator

⊢ ∀A X. indicator A absolutely_integrable_on X ⇔ indicator A integrable_on X

borel_eq_real_set

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

borel_imp_lebesgue_measurable

⊢ ∀f. f ∈ borel_measurable (space borel,subsets borel) ⇒
      f ∈ borel_measurable (m_space lebesgue,measurable_sets lebesgue)

borel_imp_lebesgue_sets

⊢ ∀s. s ∈ subsets borel ⇒ s ∈ measurable_sets lebesgue

countably_additive_lebesgue

⊢ countably_additive lebesgue

fn_minus

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

fn_minus_mul_indicator

⊢ ∀f s. (λx. f x * 𝟙 s x)⁻ = (λx. f⁻ x * 𝟙 s x)

fn_plus

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

fn_plus_mul_indicator

⊢ ∀f s. (λx. f x * 𝟙 s x)⁺ = (λx. f⁺ x * 𝟙 s x)

has_integral_indicator_UNIV

⊢ ∀s A x.
    (indicator (s ∩ A) has_integral x) 𝕌(:real) ⇔
    (indicator s has_integral x) A

has_integral_interval_cube

⊢ ∀a b n.
    (indicator (interval [(a,b)]) has_integral
     content (interval [(a,b)] ∩ line n)) (line n)

in_borel_measurable_continuous_on

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

in_borel_measurable_from_Borel

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

in_borel_measurable_imp

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

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

⊢ ∀A. (∀n. indicator A integrable_on line n) ⇒ A ∈ measurable_sets lebesgue

in_sets_lebesgue_imp

⊢ ∀A n. A ∈ measurable_sets lebesgue ⇒ indicator A integrable_on line n

indicator_fn_general_cross

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

⊢ ∀s x. ∃r. (𝟙 s x = Normal r) ∧ 0 ≤ r ∧ r ≤ 1

indicator_fn_split

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

⊢ ∀a x.
    (∀m n. m ≠ n ⇒ DISJOINT (a m) (a n)) ⇒
    (suminf (λi. 𝟙 (a i) x) = 𝟙 (BIGUNION (IMAGE a 𝕌(:num))) x)

integrable_indicator_UNIV

⊢ ∀s A. indicator (s ∩ A) integrable_on 𝕌(:real) ⇔ indicator s integrable_on A

integral_indicator_UNIV

⊢ ∀s A. ∫ 𝕌(:real) (indicator (s ∩ A)) = ∫ A (indicator s)

integral_one

⊢ ∀A. ∫ A (λx. 1) = ∫ 𝕌(:real) (indicator A)

lambda0_empty

⊢ lambda0 ∅ = 0

lambda0_not_infty

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

lambda_closed_interval

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

lambda_closed_interval_content

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

lambda_empty

⊢ lambda ∅ = 0

lambda_eq

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

⊢ ∀s. s ∈ subsets borel ⇒ (lambda s = measure lebesgue s)

lambda_not_infty

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

lambda_open_interval

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

lambda_prop

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

lambda_sing

⊢ ∀c. lambda {c} = 0

lborel0_additive

⊢ additive lborel0

lborel0_finite_additive

⊢ finite_additive lborel0

lborel0_positive

⊢ positive lborel0

lborel0_premeasure

⊢ premeasure lborel0

lborel0_subadditive

⊢ subadditive lborel0

lborel_subset_lebesgue

⊢ measurable_sets lborel ⊆ measurable_sets lebesgue

lebesgue_closed_interval

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

lebesgue_closed_interval_content

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

lebesgue_empty

⊢ measure lebesgue ∅ = 0

lebesgue_eq_lambda

⊢ ∀s. s ∈ subsets borel ⇒ (measure lebesgue s = lambda s)

lebesgue_measure_iff_LIMSEQ

⊢ ∀A m.
    A ∈ measurable_sets lebesgue ∧ 0 ≤ m ⇒
    ((measure lebesgue A = Normal m) ⇔
     ((λn. ∫ (line n) (indicator A)) ⟶ m) sequentially)

lebesgue_of_negligible

⊢ ∀s. negligible s ⇒ (measure lebesgue s = 0)

lebesgue_open_interval

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

lebesgue_sing

⊢ ∀c. measure lebesgue {c} = 0

liminf_limsup

⊢ ∀E. COMPL (liminf E) = limsup (COMPL ∘ E)

liminf_limsup_sp

⊢ ∀sp E. (∀n. E n ⊆ sp) ⇒ (sp DIFF liminf E = limsup (λn. sp DIFF E n))

limseq_indicator_BIGUNION

⊢ ∀A x.
    ((λk. indicator (BIGUNION {A i | i < k}) x) ⟶
     indicator (BIGUNION {A i | i ∈ 𝕌(:num)}) x) sequentially

limsup_suminf_indicator

⊢ ∀A. limsup A = {x | suminf (λn. 𝟙 (A n) x) = +∞}

limsup_suminf_indicator_space

⊢ ∀a A.
    sigma_algebra a ∧ (∀n. A n ∈ subsets a) ⇒
    (limsup A = {x | x ∈ space a ∧ (suminf (λn. 𝟙 (A n) x) = +∞)})

m_space_lborel

⊢ m_space lborel = space borel

measure_lebesgue

⊢ measure lebesgue =
  (λA. sup {Normal (∫ (line n) (indicator A)) | n ∈ 𝕌(:num)})

measure_liminf

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

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

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

⊢ measure_space lborel

measure_space_lebesgue

⊢ measure_space lebesgue

negligible_in_lebesgue

⊢ ∀s. negligible s ⇒ s ∈ measurable_sets lebesgue

nonneg_abs

⊢ ∀f. nonneg (abs ∘ f)

nonneg_fn_abs

⊢ ∀f. nonneg f ⇒ (abs ∘ f = f)

nonneg_fn_minus

⊢ ∀f. nonneg f ⇒ (f⁻ = (λx. 0))

nonneg_fn_plus

⊢ ∀f. nonneg f ⇒ (f⁺ = f)

positive_lebesgue

⊢ positive lebesgue

seq_le_imp_lim_le

⊢ ∀x y f. (∀n. f n ≤ x) ∧ (f ⟶ y) sequentially ⇒ y ≤ x

seq_mono_le

⊢ ∀f x n. (∀n. f n ≤ f (n + 1)) ∧ (f ⟶ x) sequentially ⇒ f n ≤ x

set_limsup_alt

⊢ ∀E. limsup E = BIGINTER (IMAGE (λn. BIGUNION (IMAGE E (from n))) 𝕌(:num))

sets_lborel

⊢ measurable_sets lborel = subsets borel

sets_lebesgue

⊢ measurable_sets lebesgue = {A | ∀n. indicator A integrable_on line n}

sigma_algebra_lebesgue

⊢ sigma_algebra (𝕌(:real),{A | ∀n. indicator A integrable_on line n})

sigma_finite_lborel

⊢ sigma_finite lborel

space_lborel

⊢ m_space lborel = 𝕌(:real)

space_lebesgue

⊢ m_space lebesgue = 𝕌(:real)

sup_sequence

⊢ ∀f l.
    mono_increasing f ⇒
    ((f ⟶ l) sequentially ⇔
     (sup (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l))