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 lambda0_def : thm
val lborel_def : thm
(* Theorems *)
val AE_ALT : thm
val AE_BIGINTER : thm
val AE_BIGUNION : thm
val AE_DEF : thm
val AE_FORALL_SWAP_THM : thm
val AE_I : thm
val AE_IMP_MEASURABLE_SETS : thm
val AE_INTER : thm
val AE_NOT_IN : thm
val AE_T : thm
val AE_THM : thm
val AE_UNION : thm
val AE_cong : thm
val AE_eq_add : thm
val AE_eq_sum : thm
val AE_filter : thm
val AE_iff_measurable : thm
val AE_iff_null : thm
val AE_iff_null_sets : thm
val AE_not_in : thm
val AE_subset : thm
val BOREL_2D : 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_EMPTY : thm
val BOREL_MEASURABLE_SETS_FINITE : thm
val BOREL_MEASURABLE_SETS_NORMAL : 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 FORALL_IMP_AE : thm
val IN_MEASURABLE_BOREL : thm
val IN_MEASURABLE_BOREL_2D_FUNCTION : thm
val IN_MEASURABLE_BOREL_2D_MUL : thm
val IN_MEASURABLE_BOREL_2D_VECTOR : thm
val IN_MEASURABLE_BOREL_ABS : thm
val IN_MEASURABLE_BOREL_ABS' : thm
val IN_MEASURABLE_BOREL_ABS_POWR : thm
val IN_MEASURABLE_BOREL_ADD : thm
val IN_MEASURABLE_BOREL_ADD' : thm
val IN_MEASURABLE_BOREL_AE_EQ : thm
val IN_MEASURABLE_BOREL_AINV : thm
val IN_MEASURABLE_BOREL_ALL : thm
val IN_MEASURABLE_BOREL_ALL_ABS : thm
val IN_MEASURABLE_BOREL_ALL_MEASURE : thm
val IN_MEASURABLE_BOREL_ALL_MEASURE_ABS : thm
val IN_MEASURABLE_BOREL_ALL_MEASURE_ABS' : 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_ABS_POWR : thm
val IN_MEASURABLE_BOREL_BOREL_AINV : thm
val IN_MEASURABLE_BOREL_BOREL_CONST : thm
val IN_MEASURABLE_BOREL_BOREL_I : thm
val IN_MEASURABLE_BOREL_BOREL_MAX : thm
val IN_MEASURABLE_BOREL_BOREL_MIN : thm
val IN_MEASURABLE_BOREL_BOREL_MONO_DECREASING : thm
val IN_MEASURABLE_BOREL_BOREL_MONO_INCREASING : thm
val IN_MEASURABLE_BOREL_BOREL_POW : 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_COMP : thm
val IN_MEASURABLE_BOREL_COMP_BOREL : thm
val IN_MEASURABLE_BOREL_CONG : thm
val IN_MEASURABLE_BOREL_CONG' : 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_EXP : 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_INF : thm
val IN_MEASURABLE_BOREL_INV : 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_MAX_FN_SEQ : thm
val IN_MEASURABLE_BOREL_MIN : thm
val IN_MEASURABLE_BOREL_MINIMAL : thm
val IN_MEASURABLE_BOREL_MINUS : thm
val IN_MEASURABLE_BOREL_MONO_INF : thm
val IN_MEASURABLE_BOREL_MONO_SUP : thm
val IN_MEASURABLE_BOREL_MUL : 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_MUL_INV : thm
val IN_MEASURABLE_BOREL_NEGINF : thm
val IN_MEASURABLE_BOREL_NORMAL_REAL : 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_POW' : thm
val IN_MEASURABLE_BOREL_POW_EXP : thm
val IN_MEASURABLE_BOREL_PROD : thm
val IN_MEASURABLE_BOREL_PROD' : 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_SUM' : thm
val IN_MEASURABLE_BOREL_SUMINF : thm
val IN_MEASURABLE_BOREL_SUP : thm
val IN_MEASURABLE_BOREL_TIMES : thm
val IN_MEASURABLE_BOREL_TIMES' : thm
val MEASURABLE_BOREL : thm
val MEASURE_SPACE_LBOREL : thm
val RIGHT_IMP_AE_THM : thm
val RIGHT_IMP_AE_THM' : 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 borel_eq_real_set : thm
val in_borel_measurable_from_Borel : thm
val in_borel_measurable_imp : thm
val in_measurable_sigma_pow : 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_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 m_space_lborel : thm
val measure_space_lborel : thm
val seq_le_imp_lim_le : thm
val seq_mono_le : thm
val sets_lborel : thm
val sigma_finite_lborel : thm
val space_lborel : thm
val sup_seq' : 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 lborel 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)
[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) ∧
measurable_space lborel = borel ∧ measure_space lborel
[AE_ALT] Theorem
⊢ ∀m P.
(AE x::m. P x) ⇔
∃N. null_set m N ∧ {x | x ∈ m_space m ∧ ¬P x} ⊆ N
[AE_BIGINTER] Theorem
⊢ ∀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
[AE_BIGUNION] Theorem
⊢ ∀m P s.
measure_space m ∧ (∃n. n ∈ s ∧ AE x::m. P n x) ⇒
AE x::m. ∃n. n ∈ s ∧ P n x
[AE_DEF] Theorem
⊢ ∀m P.
(AE x::m. P x) ⇔
∃N. null_set m N ∧ ∀x. x ∈ m_space m DIFF N ⇒ P x
[AE_FORALL_SWAP_THM] Theorem
⊢ ∀m P.
measure_space m ∧ countable 𝕌(:'index) ⇒
((AE x::m. ∀i. P i x) ⇔ ∀i. AE x::m. P i x)
[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_INTER] Theorem
⊢ ∀m P Q.
measure_space m ∧ (AE x::m. P x) ∧ (AE x::m. Q x) ⇒
AE x::m. P x ∧ Q x
[AE_NOT_IN] Theorem
⊢ ∀N M. null_set M N ⇒ AE x::M. x ∉ N
[AE_T] Theorem
⊢ ∀m. measure_space m ⇒ AE x::m. T
[AE_THM] Theorem
⊢ ∀m P. (AE x::m. P x) ⇔ almost_everywhere m P
[AE_UNION] Theorem
⊢ ∀m P Q.
measure_space m ∧ ((AE x::m. P x) ∨ AE x::m. Q x) ⇒
AE x::m. P x ∨ Q x
[AE_cong] Theorem
⊢ ∀m P Q.
(∀x. x ∈ m_space m ⇒ (P x ⇔ Q x)) ⇒
((AE x::m. P x) ⇔ AE x::m. Q x)
[AE_eq_add] Theorem
⊢ ∀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
[AE_eq_sum] Theorem
⊢ ∀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
[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. ¬N x)
[AE_not_in] Theorem
⊢ ∀N M. null_set M N ⇒ AE x::M. ¬N x
[AE_subset] Theorem
⊢ ∀m P Q.
(AE x::m. P x) ∧ (∀x. x ∈ m_space m ∧ P x ⇒ Q x) ⇒ AE x::m. Q x
[BOREL_2D] Theorem
⊢ 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})
[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_EMPTY] Theorem
⊢ ∅ ∈ subsets Borel
[BOREL_MEASURABLE_SETS_FINITE] Theorem
⊢ ∀s. FINITE s ⇒ s ∈ subsets Borel
[BOREL_MEASURABLE_SETS_NORMAL] Theorem
⊢ ∀b. b ∈ subsets borel ⇒ IMAGE Normal b ∈ 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))
[FORALL_IMP_AE] Theorem
⊢ ∀m P. measure_space m ∧ (∀x. x ∈ m_space m ⇒ P x) ⇒ AE x::m. P x
[IN_MEASURABLE_BOREL] Theorem
⊢ ∀f a.
sigma_algebra a ⇒
(f ∈ Borel_measurable 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_MUL] Theorem
⊢ (λ(x,y). x * y) ∈ Borel_measurable (Borel × Borel)
[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_ABS_POWR] Theorem
⊢ ∀a p f.
f ∈ Borel_measurable a ∧ 0 ≤ p ∧ p ≠ +∞ ⇒
(λx. abs (f x) powr p) ∈ 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 (measurable_space m) ⇒
g ∈ Borel_measurable (measurable_space m)
[IN_MEASURABLE_BOREL_AINV] Theorem
⊢ ∀a f.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
(λx. -f x) ∈ Borel_measurable a
[IN_MEASURABLE_BOREL_ALL] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_ALL_ABS] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_ALL_MEASURE] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_ALL_MEASURE_ABS] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_ALL_MEASURE_ABS'] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_ALT1] Theorem
⊢ ∀f a.
sigma_algebra a ⇒
(f ∈ Borel_measurable a ⇔
f ∈ (space a → 𝕌(:extreal)) ∧
∀c. {x | Normal c ≤ f x} ∩ space a ∈ subsets a)
[IN_MEASURABLE_BOREL_ALT1_IMP] Theorem
⊢ ∀f a.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
∀c. {x | c ≤ f x} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_ALT2] Theorem
⊢ ∀f a.
sigma_algebra a ⇒
(f ∈ Borel_measurable a ⇔
f ∈ (space a → 𝕌(:extreal)) ∧
∀c. {x | f x ≤ Normal c} ∩ space a ∈ subsets a)
[IN_MEASURABLE_BOREL_ALT2_IMP] Theorem
⊢ ∀f a.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
∀c. {x | f x ≤ c} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_ALT3] Theorem
⊢ ∀f a.
sigma_algebra a ⇒
(f ∈ Borel_measurable a ⇔
f ∈ (space a → 𝕌(:extreal)) ∧
∀c. {x | Normal c < f x} ∩ space a ∈ subsets a)
[IN_MEASURABLE_BOREL_ALT3_IMP] Theorem
⊢ ∀f a.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
∀c. {x | c < f x} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_ALT4] Theorem
⊢ ∀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)
[IN_MEASURABLE_BOREL_ALT4_IMP] Theorem
⊢ ∀f a.
sigma_algebra 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.
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)
[IN_MEASURABLE_BOREL_ALT5_IMP] Theorem
⊢ ∀f a.
sigma_algebra 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.
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)
[IN_MEASURABLE_BOREL_ALT6_IMP] Theorem
⊢ ∀f a.
sigma_algebra 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.
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)
[IN_MEASURABLE_BOREL_ALT7_IMP] Theorem
⊢ ∀f a.
sigma_algebra 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.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
∀c. {x | f x = c} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_ALT9] Theorem
⊢ ∀f a.
sigma_algebra 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_ABS_POWR] Theorem
⊢ ∀p. 0 ≤ p ∧ p ≠ +∞ ⇒ (λx. abs x powr p) ∈ Borel_measurable Borel
[IN_MEASURABLE_BOREL_BOREL_AINV] Theorem
⊢ numeric_negate ∈ Borel_measurable Borel
[IN_MEASURABLE_BOREL_BOREL_CONST] Theorem
⊢ ∀c. (λx. c) ∈ Borel_measurable Borel
[IN_MEASURABLE_BOREL_BOREL_I] Theorem
⊢ (λx. x) ∈ Borel_measurable Borel
[IN_MEASURABLE_BOREL_BOREL_MAX] Theorem
⊢ ∀c. (λx. max x c) ∈ Borel_measurable Borel
[IN_MEASURABLE_BOREL_BOREL_MIN] Theorem
⊢ ∀c. (λx. min x c) ∈ Borel_measurable Borel
[IN_MEASURABLE_BOREL_BOREL_MONO_DECREASING] Theorem
⊢ ∀f. (∀x y. x ≤ y ⇒ f y ≤ f x) ⇒ f ∈ Borel_measurable Borel
[IN_MEASURABLE_BOREL_BOREL_MONO_INCREASING] Theorem
⊢ ∀f. (∀x y. x ≤ y ⇒ f x ≤ f y) ⇒ f ∈ Borel_measurable Borel
[IN_MEASURABLE_BOREL_BOREL_POW] Theorem
⊢ ∀n. (λx. x pow n) ∈ Borel_measurable Borel
[IN_MEASURABLE_BOREL_CC] Theorem
⊢ ∀f a.
sigma_algebra 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.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
∀c d. {x | c ≤ f x ∧ f x < d} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_COMP] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_COMP_BOREL] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_CONG] Theorem
⊢ ∀m f g.
(∀x. x ∈ m_space m ⇒ f x = g x) ⇒
(f ∈ Borel_measurable (measurable_space m) ⇔
g ∈ Borel_measurable (measurable_space m))
[IN_MEASURABLE_BOREL_CONG'] Theorem
⊢ ∀a f g.
(∀x. x ∈ space a ⇒ f x = g x) ⇒
(f ∈ Borel_measurable a ⇔ g ∈ Borel_measurable 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.
sigma_algebra 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 (measurable_space m) ⇒
f ∈ Borel_measurable (measurable_space 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_EXP] Theorem
⊢ ∀a f g.
sigma_algebra a ∧ f ∈ Borel_measurable a ∧
(∀x. x ∈ space a ⇒ g x = exp (f x)) ⇒
g ∈ Borel_measurable a
[IN_MEASURABLE_BOREL_FN_MINUS] Theorem
⊢ ∀a f.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
f⁻ ∈ Borel_measurable a
[IN_MEASURABLE_BOREL_FN_PLUS] Theorem
⊢ ∀a f.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
f⁺ ∈ Borel_measurable a
[IN_MEASURABLE_BOREL_IMP] Theorem
⊢ ∀f a.
sigma_algebra 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 (measurable_space m) ⇒
Normal ∘ f ∈ Borel_measurable (measurable_space 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_INF] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_INV] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_LE] Theorem
⊢ ∀a f g.
sigma_algebra a ∧ 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.
sigma_algebra 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_MAX_FN_SEQ] Theorem
⊢ ∀a f.
sigma_algebra a ∧ (∀i. f i ∈ Borel_measurable a) ⇒
∀n. max_fn_seq f n ∈ 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_INF] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_MONO_SUP] Theorem
⊢ ∀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
[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'] 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_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_MUL_INV] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_NEGINF] Theorem
⊢ ∀f a.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
{x | f x = −∞} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_NORMAL_REAL] Theorem
⊢ ∀a f.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
Normal ∘ real ∘ f ∈ Borel_measurable a
[IN_MEASURABLE_BOREL_NOT_NEGINF] Theorem
⊢ ∀f a.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
{x | f x ≠ −∞} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_NOT_POSINF] Theorem
⊢ ∀f a.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
{x | f x ≠ +∞} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_NOT_SING] Theorem
⊢ ∀f a.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
∀c. {x | f x ≠ c} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_OC] Theorem
⊢ ∀f a.
sigma_algebra 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.
sigma_algebra 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.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
∀c. {x | c < f x} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_PLUS_MINUS] Theorem
⊢ ∀a f.
sigma_algebra a ⇒
(f ∈ Borel_measurable a ⇔
f⁺ ∈ Borel_measurable a ∧ f⁻ ∈ Borel_measurable a)
[IN_MEASURABLE_BOREL_POSINF] Theorem
⊢ ∀f a.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
{x | f x = +∞} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_POW] Theorem
⊢ ∀n a f.
f ∈ Borel_measurable a ⇒ (λx. f x pow n) ∈ Borel_measurable a
[IN_MEASURABLE_BOREL_POW'] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_POW_EXP] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_PROD] 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 ≠ −∞ ∧ f i x ≠ +∞) ∧
(∀x. x ∈ space a ⇒ g x = ∏ (λi. f i x) s) ⇒
g ∈ Borel_measurable a
[IN_MEASURABLE_BOREL_PROD'] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_RC] Theorem
⊢ ∀f a.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
∀c. {x | f x ≤ c} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_RO] Theorem
⊢ ∀f a.
sigma_algebra a ∧ f ∈ Borel_measurable a ⇒
∀c. {x | f x < c} ∩ space a ∈ subsets a
[IN_MEASURABLE_BOREL_SING] Theorem
⊢ ∀f a.
sigma_algebra 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_SUM'] Theorem
⊢ ∀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
[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_SUP] Theorem
⊢ ∀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
[IN_MEASURABLE_BOREL_TIMES] Theorem
⊢ ∀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)
[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.
sigma_algebra a ⇒
(f ∈ Borel_measurable a ⇔
f ∈ (space a → 𝕌(:extreal)) ∧
∀c. PREIMAGE f {x | x < Normal c} ∩ space a ∈ subsets a)
[MEASURE_SPACE_LBOREL] Theorem
⊢ measure_space ext_lborel
[RIGHT_IMP_AE_THM] Theorem
⊢ ∀m P Q. measure_space m ⇒ (P ⇒ (AE x::m. Q x) ⇔ AE x::m. P ⇒ Q x)
[RIGHT_IMP_AE_THM'] Theorem
⊢ ∀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] 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)
[borel_eq_real_set] Theorem
⊢ borel = (𝕌(:real),IMAGE real_set (subsets Borel))
[in_borel_measurable_from_Borel] Theorem
⊢ ∀a f.
sigma_algebra a ∧ 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 (measurable_space 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 (measurable_space m) (sigma sp N)
[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_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
[m_space_lborel] Theorem
⊢ m_space lborel = space borel
[measure_space_lborel] Theorem
⊢ measure_space lborel
[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
[sets_lborel] Theorem
⊢ measurable_sets lborel = subsets borel
[sigma_finite_lborel] Theorem
⊢ sigma_finite lborel
[space_lborel] Theorem
⊢ m_space lborel = 𝕌(:real)
[sup_seq'] Theorem
⊢ ∀f l.
mono_increasing f ⇒
((f --> l) sequentially ⇔
sup (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l)
*)
end
HOL 4, Trindemossen-1