Structure sigma_algebraTheory
signature sigma_algebraTheory =
sig
type thm = Thm.thm
(* Definitions *)
val algebra_def : thm
val dynkin_def : thm
val dynkin_system_def : thm
val measurable_def : thm
val prod_sigma_def : thm
val ring_def : thm
val semiring_def : thm
val sigma_algebra_def : thm
val sigma_def : thm
val sigma_function_def : thm
val sigma_functions_def : thm
val smallest_ring_def : thm
val space_def : thm
val subset_class_def : thm
val subsets_def : thm
(* Theorems *)
val ALGEBRA_ALT_INTER : thm
val ALGEBRA_COMPL : thm
val ALGEBRA_COMPL_SETS : thm
val ALGEBRA_DIFF : thm
val ALGEBRA_EMPTY : thm
val ALGEBRA_FINITE_INTER : thm
val ALGEBRA_FINITE_INTER' : thm
val ALGEBRA_FINITE_UNION : thm
val ALGEBRA_IMP_RING : thm
val ALGEBRA_IMP_SEMIRING : thm
val ALGEBRA_INTER : thm
val ALGEBRA_INTER_SPACE : thm
val ALGEBRA_RESTRICT : thm
val ALGEBRA_RESTRICT' : thm
val ALGEBRA_SETS_COLLECT_CONST : thm
val ALGEBRA_SETS_COLLECT_IMP : thm
val ALGEBRA_SETS_COLLECT_NEG : thm
val ALGEBRA_SINGLE_SET : thm
val ALGEBRA_SPACE : thm
val ALGEBRA_UNION : thm
val DYNKIN : thm
val DYNKIN_LEMMA : thm
val DYNKIN_MONOTONE : thm
val DYNKIN_SMALLEST : thm
val DYNKIN_STABLE : thm
val DYNKIN_STABLE_LEMMA : thm
val DYNKIN_SUBSET : thm
val DYNKIN_SUBSET_SIGMA : thm
val DYNKIN_SUBSET_SUBSETS : thm
val DYNKIN_SYSTEM_ALT : thm
val DYNKIN_SYSTEM_ALT_MONO : thm
val DYNKIN_SYSTEM_COMPL : thm
val DYNKIN_SYSTEM_COUNTABLY_DUNION : thm
val DYNKIN_SYSTEM_DUNION : thm
val DYNKIN_SYSTEM_EMPTY : thm
val DYNKIN_SYSTEM_INCREASING : thm
val DYNKIN_SYSTEM_SPACE : thm
val DYNKIN_THM : thm
val INTER_SPACE_EQ1 : thm
val INTER_SPACE_REDUCE : thm
val IN_DYNKIN : thm
val IN_MEASURABLE : thm
val IN_MEASURABLE_COMP : thm
val IN_MEASURABLE_CONG : thm
val IN_MEASURABLE_EQ : thm
val IN_MEASURABLE_PROD_SIGMA : thm
val IN_SIGMA : thm
val IN_SPACE_PROD_SIGMA : thm
val MEASUBABLE_BIGUNION_LEMMA : thm
val MEASURABLE_BIGUNION_PROPERTY : thm
val MEASURABLE_COMP : thm
val MEASURABLE_COMP_STRONG : thm
val MEASURABLE_COMP_STRONGER : thm
val MEASURABLE_DIFF_PROPERTY : thm
val MEASURABLE_FST : thm
val MEASURABLE_I : thm
val MEASURABLE_LEMMA : thm
val MEASURABLE_LIFT : thm
val MEASURABLE_PROD_SIGMA : thm
val MEASURABLE_PROD_SIGMA' : thm
val MEASURABLE_SIGMA : thm
val MEASURABLE_SIGMA_PREIMAGES : thm
val MEASURABLE_SND : thm
val MEASURABLE_SUBSET : thm
val MEASURABLE_UP_LIFT : thm
val MEASURABLE_UP_SIGMA : thm
val MEASURABLE_UP_SUBSET : thm
val POW_ALGEBRA : thm
val POW_SIGMA_ALGEBRA : thm
val PREIMAGE_SIGMA : thm
val PREIMAGE_SIGMA_ALGEBRA : thm
val RING_BIGUNION : thm
val RING_DIFF : thm
val RING_DIFF_ALT : thm
val RING_EMPTY : thm
val RING_FINITE_BIGUNION1 : thm
val RING_FINITE_BIGUNION2 : thm
val RING_FINITE_INTER : thm
val RING_FINITE_INTER' : thm
val RING_FINITE_UNION : thm
val RING_FINITE_UNION_ALT : thm
val RING_IMP_SEMIRING : thm
val RING_INSERT : thm
val RING_INTER : thm
val RING_SETS_COLLECT_FINITE : thm
val RING_SPACE_IMP_ALGEBRA : thm
val RING_UNION : thm
val SEMIRING_DIFF : thm
val SEMIRING_DIFF_ALT : thm
val SEMIRING_EMPTY : thm
val SEMIRING_FINITE_INTER : thm
val SEMIRING_FINITE_INTER' : thm
val SEMIRING_INTER : thm
val SEMIRING_PROD_SETS : thm
val SEMIRING_PROD_SETS' : thm
val SEMIRING_SETS_COLLECT : thm
val SIGMA_ALGEBRA : thm
val SIGMA_ALGEBRA_ALGEBRA : thm
val SIGMA_ALGEBRA_ALT : thm
val SIGMA_ALGEBRA_ALT_DISJOINT : thm
val SIGMA_ALGEBRA_ALT_MONO : thm
val SIGMA_ALGEBRA_ALT_SPACE : thm
val SIGMA_ALGEBRA_COMPL : thm
val SIGMA_ALGEBRA_COUNTABLE_INT : thm
val SIGMA_ALGEBRA_COUNTABLE_INT' : thm
val SIGMA_ALGEBRA_COUNTABLE_UN : thm
val SIGMA_ALGEBRA_COUNTABLE_UN' : thm
val SIGMA_ALGEBRA_COUNTABLE_UNION : thm
val SIGMA_ALGEBRA_DIFF : thm
val SIGMA_ALGEBRA_EMPTY : thm
val SIGMA_ALGEBRA_ENUM : thm
val SIGMA_ALGEBRA_FINITE_INTER : thm
val SIGMA_ALGEBRA_FINITE_INTER' : thm
val SIGMA_ALGEBRA_FINITE_UNION : thm
val SIGMA_ALGEBRA_FN : thm
val SIGMA_ALGEBRA_FN_BIGINTER : thm
val SIGMA_ALGEBRA_FN_DISJOINT : thm
val SIGMA_ALGEBRA_IMP_DYNKIN_SYSTEM : thm
val SIGMA_ALGEBRA_INTER : thm
val SIGMA_ALGEBRA_PROD_SIGMA : thm
val SIGMA_ALGEBRA_PROD_SIGMA' : thm
val SIGMA_ALGEBRA_PROD_SIGMA_WEAK : thm
val SIGMA_ALGEBRA_RESTRICT : thm
val SIGMA_ALGEBRA_RESTRICT' : thm
val SIGMA_ALGEBRA_RESTRICT_SUBSET : thm
val SIGMA_ALGEBRA_SIGMA : thm
val SIGMA_ALGEBRA_SPACE : thm
val SIGMA_ALGEBRA_SUBSET_SPACE : thm
val SIGMA_ALGEBRA_UNION : thm
val SIGMA_CONG : thm
val SIGMA_MEASURABLE : thm
val SIGMA_MONOTONE : thm
val SIGMA_POW : thm
val SIGMA_PROPERTY : thm
val SIGMA_PROPERTY_ALT : thm
val SIGMA_PROPERTY_DISJOINT : thm
val SIGMA_PROPERTY_DISJOINT_LEMMA : thm
val SIGMA_PROPERTY_DISJOINT_LEMMA1 : thm
val SIGMA_PROPERTY_DISJOINT_LEMMA2 : thm
val SIGMA_PROPERTY_DISJOINT_WEAK : thm
val SIGMA_PROPERTY_DISJOINT_WEAK_ALT : thm
val SIGMA_REDUCE : thm
val SIGMA_RESTRICT : thm
val SIGMA_SIMULTANEOUSLY_MEASURABLE : thm
val SIGMA_SMALLEST : thm
val SIGMA_STABLE : thm
val SIGMA_STABLE_LEMMA : thm
val SIGMA_SUBSET : thm
val SIGMA_SUBSET_SUBSETS : thm
val SMALLEST_RING : thm
val SMALLEST_RING_OF_SEMIRING : thm
val SMALLEST_RING_SUBSET_SUBSETS : thm
val SPACE : thm
val SPACE_DYNKIN : thm
val SPACE_PROD_SIGMA : thm
val SPACE_SIGMA : thm
val SPACE_SMALLEST_RING : thm
val TRACE_SIGMA_ALGEBRA : thm
val UNIV_SIGMA_ALGEBRA : thm
val algebra_alt : thm
val algebra_alt_inter : thm
val algebra_alt_union : thm
val algebra_finite_space_imp_sigma_algebra : thm
val algebra_finite_subsets_imp_sigma_algebra : thm
val prod_sigma_alt_sigma_functions : thm
val prod_sigma_alt_sigma_functions' : thm
val ring_alt : thm
val ring_alt_pow : thm
val ring_alt_pow_imp : thm
val ring_and_semiring : thm
val ring_disjointed_sets : thm
val semiring_alt : thm
val sigma_algebra_alt : thm
val sigma_algebra_alt_pow : thm
val sigma_algebra_sigma_function : thm
val sigma_algebra_sigma_functions : thm
val sigma_algebra_sigma_sets : thm
val sigma_function_alt_sigma_functions : thm
val sigma_function_subset : thm
val sigma_functions_1 : thm
val sigma_functions_subset : thm
val sigma_sets_BIGINTER : thm
val sigma_sets_BIGINTER2 : thm
val sigma_sets_BIGUNION : thm
val sigma_sets_basic : thm
val sigma_sets_cases : thm
val sigma_sets_compl : thm
val sigma_sets_empty : thm
val sigma_sets_fixpoint : thm
val sigma_sets_ind : thm
val sigma_sets_into_sp : thm
val sigma_sets_least_sigma_algebra : thm
val sigma_sets_rules : thm
val sigma_sets_strongind : thm
val sigma_sets_subset : thm
val sigma_sets_superset_generator : thm
val sigma_sets_top : thm
val sigma_sets_union : thm
val space_sigma_function : thm
val space_sigma_functions : thm
val subset_class_POW : thm
val sigma_algebra_grammars : type_grammar.grammar * term_grammar.grammar
(*
[seq] Parent theory of "sigma_algebra"
[util_prob] Parent theory of "sigma_algebra"
[algebra_def] Definition
⊢ ∀a. algebra a ⇔
subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
(∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a
[dynkin_def] Definition
⊢ ∀sp sts.
dynkin sp sts =
(sp,BIGINTER {d | sts ⊆ d ∧ dynkin_system (sp,d)})
[dynkin_system_def] Definition
⊢ ∀d. dynkin_system d ⇔
subset_class (space d) (subsets d) ∧ space d ∈ subsets d ∧
(∀s. s ∈ subsets d ⇒ space d DIFF s ∈ subsets d) ∧
∀f. f ∈ (𝕌(:num) → subsets d) ∧
(∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d
[measurable_def] Definition
⊢ ∀a b.
measurable a b =
{f |
f ∈ (space a → space b) ∧
∀s. s ∈ subsets b ⇒ PREIMAGE f s ∩ space a ∈ subsets a}
[prod_sigma_def] Definition
⊢ ∀a b.
a × b =
sigma (space a × space b) (prod_sets (subsets a) (subsets b))
[ring_def] Definition
⊢ ∀r. ring r ⇔
subset_class (space r) (subsets r) ∧ ∅ ∈ subsets r ∧
(∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∪ t ∈ subsets r) ∧
∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s DIFF t ∈ subsets r
[semiring_def] Definition
⊢ ∀r. semiring r ⇔
subset_class (space r) (subsets r) ∧ ∅ ∈ subsets r ∧
(∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∩ t ∈ subsets r) ∧
∀s t.
s ∈ subsets r ∧ t ∈ subsets r ⇒
∃c. c ⊆ subsets r ∧ FINITE c ∧ disjoint c ∧
s DIFF t = BIGUNION c
[sigma_algebra_def] Definition
⊢ ∀a. sigma_algebra a ⇔
algebra a ∧
∀c. countable c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a
[sigma_def] Definition
⊢ ∀sp sts.
sigma sp sts = (sp,BIGINTER {s | sts ⊆ s ∧ sigma_algebra (sp,s)})
[sigma_function_def] Definition
⊢ ∀sp A f.
sigma sp A f = (sp,IMAGE (λs. PREIMAGE f s ∩ sp) (subsets A))
[sigma_functions_def] Definition
⊢ ∀sp A f J.
sigma sp A f J =
sigma sp
(BIGUNION
(IMAGE
(λi. IMAGE (λs. PREIMAGE (f i) s ∩ sp) (subsets (A i))) J))
[smallest_ring_def] Definition
⊢ ∀sp sts.
smallest_ring sp sts = (sp,BIGINTER {s | sts ⊆ s ∧ ring (sp,s)})
[space_def] Definition
⊢ ∀x y. space (x,y) = x
[subset_class_def] Definition
⊢ ∀sp sts. subset_class sp sts ⇔ ∀x. x ∈ sts ⇒ x ⊆ sp
[subsets_def] Definition
⊢ ∀x y. subsets (x,y) = y
[ALGEBRA_ALT_INTER] Theorem
⊢ ∀a. algebra a ⇔
subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
(∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∩ t ∈ subsets a
[ALGEBRA_COMPL] Theorem
⊢ ∀a s. algebra a ∧ s ∈ subsets a ⇒ space a DIFF s ∈ subsets a
[ALGEBRA_COMPL_SETS] Theorem
⊢ ∀sp sts a. algebra (sp,sts) ∧ a ∈ sts ⇒ sp DIFF a ∈ sts
[ALGEBRA_DIFF] Theorem
⊢ ∀a s t.
algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s DIFF t ∈ subsets a
[ALGEBRA_EMPTY] Theorem
⊢ ∀a. algebra a ⇒ ∅ ∈ subsets a
[ALGEBRA_FINITE_INTER] Theorem
⊢ ∀a f n.
algebra a ∧ 0 < n ∧ (∀i. i < n ⇒ f i ∈ subsets a) ⇒
BIGINTER (IMAGE f (count n)) ∈ subsets a
[ALGEBRA_FINITE_INTER'] Theorem
⊢ ∀a c.
algebra a ∧ FINITE c ∧ c ⊆ subsets a ∧ c ≠ ∅ ⇒
BIGINTER c ∈ subsets a
[ALGEBRA_FINITE_UNION] Theorem
⊢ ∀a c. algebra a ∧ FINITE c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a
[ALGEBRA_IMP_RING] Theorem
⊢ ∀a. algebra a ⇒ ring a
[ALGEBRA_IMP_SEMIRING] Theorem
⊢ ∀a. algebra a ⇒ semiring a
[ALGEBRA_INTER] Theorem
⊢ ∀a s t.
algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∩ t ∈ subsets a
[ALGEBRA_INTER_SPACE] Theorem
⊢ ∀a s. algebra a ∧ s ∈ subsets a ⇒ space a ∩ s = s ∧ s ∩ space a = s
[ALGEBRA_RESTRICT] Theorem
⊢ ∀sp sts a.
algebra (sp,sts) ∧ a ∈ sts ⇒ algebra (a,IMAGE (λs. s ∩ a) sts)
[ALGEBRA_RESTRICT'] Theorem
⊢ ∀sp sts a.
algebra (sp,sts) ∧ a ⊆ sp ⇒ algebra (a,IMAGE (λs. s ∩ a) sts)
[ALGEBRA_SETS_COLLECT_CONST] Theorem
⊢ ∀sp sts P. algebra (sp,sts) ⇒ {x | x ∈ sp ∧ P} ∈ sts
[ALGEBRA_SETS_COLLECT_IMP] Theorem
⊢ ∀sp sts P Q.
algebra (sp,sts) ∧ {x | x ∈ sp ∧ P x} ∈ sts ⇒
{x | x ∈ sp ∧ Q x} ∈ sts ⇒
{x | x ∈ sp ∧ (Q x ⇒ P x)} ∈ sts
[ALGEBRA_SETS_COLLECT_NEG] Theorem
⊢ ∀sp sts P.
algebra (sp,sts) ∧ {x | x ∈ sp ∧ P x} ∈ sts ⇒
{x | x ∈ sp ∧ ¬P x} ∈ sts
[ALGEBRA_SINGLE_SET] Theorem
⊢ ∀X S. X ⊆ S ⇒ algebra (S,{∅; X; S DIFF X; S})
[ALGEBRA_SPACE] Theorem
⊢ ∀a. algebra a ⇒ space a ∈ subsets a
[ALGEBRA_UNION] Theorem
⊢ ∀a s t.
algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a
[DYNKIN] Theorem
⊢ ∀sp sts.
subset_class sp sts ⇒
sts ⊆ subsets (dynkin sp sts) ∧ dynkin_system (dynkin sp sts) ∧
subset_class sp (subsets (dynkin sp sts))
[DYNKIN_LEMMA] Theorem
⊢ ∀d. dynkin_system d ∧
(∀s t. s ∈ subsets d ∧ t ∈ subsets d ⇒ s ∩ t ∈ subsets d) ⇔
sigma_algebra d
[DYNKIN_MONOTONE] Theorem
⊢ ∀sp a b. a ⊆ b ⇒ subsets (dynkin sp a) ⊆ subsets (dynkin sp b)
[DYNKIN_SMALLEST] Theorem
⊢ ∀sp sts D.
sts ⊆ D ∧ D ⊆ subsets (dynkin sp sts) ∧ dynkin_system (sp,D) ⇒
D = subsets (dynkin sp sts)
[DYNKIN_STABLE] Theorem
⊢ ∀d. dynkin_system d ⇒ dynkin (space d) (subsets d) = d
[DYNKIN_STABLE_LEMMA] Theorem
⊢ ∀sp sts. dynkin_system (sp,sts) ⇒ dynkin sp sts = (sp,sts)
[DYNKIN_SUBSET] Theorem
⊢ ∀a b.
dynkin_system b ∧ a ⊆ subsets b ⇒
subsets (dynkin (space b) a) ⊆ subsets b
[DYNKIN_SUBSET_SIGMA] Theorem
⊢ ∀sp sts.
subset_class sp sts ⇒
subsets (dynkin sp sts) ⊆ subsets (sigma sp sts)
[DYNKIN_SUBSET_SUBSETS] Theorem
⊢ ∀sp a. a ⊆ subsets (dynkin sp a)
[DYNKIN_SYSTEM_ALT] Theorem
⊢ ∀d. dynkin_system d ⇔
subset_class (space d) (subsets d) ∧ space d ∈ subsets d ∧
(∀s. s ∈ subsets d ⇒ space d DIFF s ∈ subsets d) ∧
(∀f. f ∈ (𝕌(:num) → subsets d) ∧ f 0 = ∅ ∧
(∀n. f n ⊆ f (SUC n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d) ∧
∀f. f ∈ (𝕌(:num) → subsets d) ∧
(∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d
[DYNKIN_SYSTEM_ALT_MONO] Theorem
⊢ ∀d. dynkin_system d ⇔
subset_class (space d) (subsets d) ∧ space d ∈ subsets d ∧
(∀s t.
s ∈ subsets d ∧ t ∈ subsets d ∧ s ⊆ t ⇒ t DIFF s ∈ subsets d) ∧
∀f. f ∈ (𝕌(:num) → subsets d) ∧ f 0 = ∅ ∧ (∀n. f n ⊆ f (SUC n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d
[DYNKIN_SYSTEM_COMPL] Theorem
⊢ ∀d s. dynkin_system d ∧ s ∈ subsets d ⇒ space d DIFF s ∈ subsets d
[DYNKIN_SYSTEM_COUNTABLY_DUNION] Theorem
⊢ ∀d f.
dynkin_system d ∧ f ∈ (𝕌(:num) → subsets d) ∧
(∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d
[DYNKIN_SYSTEM_DUNION] Theorem
⊢ ∀d s t.
dynkin_system d ∧ s ∈ subsets d ∧ t ∈ subsets d ∧ DISJOINT s t ⇒
s ∪ t ∈ subsets d
[DYNKIN_SYSTEM_EMPTY] Theorem
⊢ ∀d. dynkin_system d ⇒ ∅ ∈ subsets d
[DYNKIN_SYSTEM_INCREASING] Theorem
⊢ ∀p f.
dynkin_system p ∧ f ∈ (𝕌(:num) → subsets p) ∧ f 0 = ∅ ∧
(∀n. f n ⊆ f (SUC n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets p
[DYNKIN_SYSTEM_SPACE] Theorem
⊢ ∀d. dynkin_system d ⇒ space d ∈ subsets d
[DYNKIN_THM] Theorem
⊢ ∀sp sts.
subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ⇒
dynkin sp sts = sigma sp sts
[INTER_SPACE_EQ1] Theorem
⊢ ∀sp sts. subset_class sp sts ⇒ ∀x. x ∈ sts ⇒ sp ∩ x = x
[INTER_SPACE_REDUCE] Theorem
⊢ ∀sp sts. subset_class sp sts ⇒ ∀x. x ∈ sts ⇒ x ∩ sp = x
[IN_DYNKIN] Theorem
⊢ ∀sp a x. x ∈ a ⇒ x ∈ subsets (dynkin sp a)
[IN_MEASURABLE] Theorem
⊢ ∀a b f.
f ∈ measurable a b ⇔
f ∈ (space a → space b) ∧
∀s. s ∈ subsets b ⇒ PREIMAGE f s ∩ space a ∈ subsets a
[IN_MEASURABLE_COMP] Theorem
⊢ ∀f g h a b c.
f ∈ measurable a b ∧ g ∈ measurable b c ∧
(∀x. x ∈ space a ⇒ h x = g (f x)) ⇒
h ∈ measurable a c
[IN_MEASURABLE_CONG] Theorem
⊢ ∀a b c d f g.
a = c ∧ b = d ∧ (∀x. x ∈ space c ⇒ f x = g x) ⇒
(f ∈ measurable a b ⇔ g ∈ measurable c d)
[IN_MEASURABLE_EQ] Theorem
⊢ ∀a b f g.
f ∈ measurable a b ∧ (∀x. x ∈ space a ⇒ g x = f x) ⇒
g ∈ measurable a b
[IN_MEASURABLE_PROD_SIGMA] Theorem
⊢ ∀a bx by fx fy f.
sigma_algebra a ∧ subset_class (space bx) (subsets bx) ∧
subset_class (space by) (subsets by) ∧ fx ∈ measurable a bx ∧
fy ∈ measurable a by ∧ (∀z. z ∈ space a ⇒ f z = (fx z,fy z)) ⇒
f ∈ measurable a (bx × by)
[IN_SIGMA] Theorem
⊢ ∀sp a x. x ∈ a ⇒ x ∈ subsets (sigma sp a)
[IN_SPACE_PROD_SIGMA] Theorem
⊢ ∀a b z. z ∈ space (a × b) ⇔ FST z ∈ space a ∧ SND z ∈ space b
[MEASUBABLE_BIGUNION_LEMMA] Theorem
⊢ ∀a b f.
sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a → space b) ∧
(∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
∀c. countable c ∧ c ⊆ IMAGE (PREIMAGE f) (subsets b) ⇒
BIGUNION c ∈ IMAGE (PREIMAGE f) (subsets b)
[MEASURABLE_BIGUNION_PROPERTY] Theorem
⊢ ∀a b f.
sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a → space b) ∧
(∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
∀c. c ⊆ subsets b ⇒
PREIMAGE f (BIGUNION c) = BIGUNION (IMAGE (PREIMAGE f) c)
[MEASURABLE_COMP] Theorem
⊢ ∀f g a b c.
f ∈ measurable a b ∧ g ∈ measurable b c ⇒ g ∘ f ∈ measurable a c
[MEASURABLE_COMP_STRONG] Theorem
⊢ ∀f g a b c.
f ∈ measurable a b ∧ sigma_algebra c ∧ g ∈ (space b → space c) ∧
(∀x. x ∈ subsets c ⇒ PREIMAGE g x ∩ IMAGE f (space a) ∈ subsets b) ⇒
g ∘ f ∈ measurable a c
[MEASURABLE_COMP_STRONGER] Theorem
⊢ ∀f g a b c t.
f ∈ measurable a b ∧ sigma_algebra c ∧ g ∈ (space b → space c) ∧
IMAGE f (space a) ⊆ t ∧
(∀s. s ∈ subsets c ⇒ PREIMAGE g s ∩ t ∈ subsets b) ⇒
g ∘ f ∈ measurable a c
[MEASURABLE_DIFF_PROPERTY] Theorem
⊢ ∀a b f.
sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a → space b) ∧
(∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
∀s. s ∈ subsets b ⇒
PREIMAGE f (space b DIFF s) = space a DIFF PREIMAGE f s
[MEASURABLE_FST] Theorem
⊢ ∀a b.
sigma_algebra a ∧ sigma_algebra b ⇒ FST ∈ measurable (a × b) a
[MEASURABLE_I] Theorem
⊢ ∀a. sigma_algebra a ⇒ I ∈ measurable a a
[MEASURABLE_LEMMA] Theorem
⊢ ∀f a b sp sts.
sigma_algebra a ∧ subset_class sp sts ∧ f ∈ (space a → sp) ∧
b = sigma sp sts ⇒
((∀s. s ∈ subsets b ⇒ PREIMAGE f s ∩ space a ∈ subsets a) ⇔
∀s. s ∈ sts ⇒ PREIMAGE f s ∩ space a ∈ subsets a)
[MEASURABLE_LIFT] Theorem
⊢ ∀f a b.
sigma_algebra a ∧ subset_class (space b) (subsets b) ∧
f ∈ measurable a b ⇒
f ∈ measurable a (sigma (space b) (subsets b))
[MEASURABLE_PROD_SIGMA] Theorem
⊢ ∀a a1 a2 f.
sigma_algebra a ∧ subset_class (space a1) (subsets a1) ∧
subset_class (space a2) (subsets a2) ∧
FST ∘ f ∈ measurable a a1 ∧ SND ∘ f ∈ measurable a a2 ⇒
f ∈
measurable a
(sigma (space a1 × space a2)
(prod_sets (subsets a1) (subsets a2)))
[MEASURABLE_PROD_SIGMA'] Theorem
⊢ ∀a a1 a2 f.
sigma_algebra a ∧ subset_class (space a1) (subsets a1) ∧
subset_class (space a2) (subsets a2) ∧
FST ∘ f ∈ measurable a a1 ∧ SND ∘ f ∈ measurable a a2 ⇒
f ∈ measurable a (a1 × a2)
[MEASURABLE_SIGMA] Theorem
⊢ ∀f a b sp.
sigma_algebra a ∧ subset_class sp b ∧ f ∈ (space a → sp) ∧
(∀s. s ∈ b ⇒ PREIMAGE f s ∩ space a ∈ subsets a) ⇒
f ∈ measurable a (sigma sp b)
[MEASURABLE_SIGMA_PREIMAGES] Theorem
⊢ ∀a b f.
sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a → space b) ∧
(∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
sigma_algebra (space a,IMAGE (PREIMAGE f) (subsets b))
[MEASURABLE_SND] Theorem
⊢ ∀a b.
sigma_algebra a ∧ sigma_algebra b ⇒ SND ∈ measurable (a × b) b
[MEASURABLE_SUBSET] Theorem
⊢ ∀a b.
sigma_algebra a ∧ subset_class (space b) (subsets b) ⇒
measurable a b ⊆ measurable a (sigma (space b) (subsets b))
[MEASURABLE_UP_LIFT] Theorem
⊢ ∀sp a b c f.
f ∈ measurable (sp,a) c ∧ sigma_algebra (sp,b) ∧ a ⊆ b ⇒
f ∈ measurable (sp,b) c
[MEASURABLE_UP_SIGMA] Theorem
⊢ ∀a b.
subset_class (space a) (subsets a) ∧ sigma_algebra b ⇒
measurable a b ⊆ measurable (sigma (space a) (subsets a)) b
[MEASURABLE_UP_SUBSET] Theorem
⊢ ∀sp a b c.
a ⊆ b ∧ sigma_algebra (sp,b) ⇒
measurable (sp,a) c ⊆ measurable (sp,b) c
[POW_ALGEBRA] Theorem
⊢ ∀sp. algebra (sp,POW sp)
[POW_SIGMA_ALGEBRA] Theorem
⊢ ∀sp. sigma_algebra (sp,POW sp)
[PREIMAGE_SIGMA] Theorem
⊢ ∀Z sp sts f.
subset_class sp sts ∧ f ∈ (Z → sp) ⇒
IMAGE (λs. PREIMAGE f s ∩ Z) (subsets (sigma sp sts)) =
subsets (sigma Z (IMAGE (λs. PREIMAGE f s ∩ Z) sts))
[PREIMAGE_SIGMA_ALGEBRA] Theorem
⊢ ∀sp A f.
sigma_algebra A ∧ f ∈ (sp → space A) ⇒
sigma_algebra (sp,IMAGE (λs. PREIMAGE f s ∩ sp) (subsets A))
[RING_BIGUNION] Theorem
⊢ ∀sp sts A n.
ring (sp,sts) ∧ IMAGE A 𝕌(:num) ⊆ sts ⇒
BIGUNION {A i | i < n} ∈ sts
[RING_DIFF] Theorem
⊢ ∀r s t.
ring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s DIFF t ∈ subsets r
[RING_DIFF_ALT] Theorem
⊢ ∀a b sp sts. ring (sp,sts) ∧ a ∈ sts ∧ b ∈ sts ⇒ a DIFF b ∈ sts
[RING_EMPTY] Theorem
⊢ ∀r. ring r ⇒ ∅ ∈ subsets r
[RING_FINITE_BIGUNION1] Theorem
⊢ ∀X sp sts. ring (sp,sts) ∧ FINITE X ⇒ X ⊆ sts ⇒ BIGUNION X ∈ sts
[RING_FINITE_BIGUNION2] Theorem
⊢ ∀A N sp sts.
ring (sp,sts) ∧ FINITE N ∧ (∀i. i ∈ N ⇒ A i ∈ sts) ⇒
BIGUNION {A i | i ∈ N} ∈ sts
[RING_FINITE_INTER] Theorem
⊢ ∀r f n.
ring r ∧ 0 < n ∧ (∀i. i < n ⇒ f i ∈ subsets r) ⇒
BIGINTER (IMAGE f (count n)) ∈ subsets r
[RING_FINITE_INTER'] Theorem
⊢ ∀r c.
ring r ∧ FINITE c ∧ c ⊆ subsets r ∧ c ≠ ∅ ⇒
BIGINTER c ∈ subsets r
[RING_FINITE_UNION] Theorem
⊢ ∀r c. ring r ∧ c ⊆ subsets r ∧ FINITE c ⇒ BIGUNION c ∈ subsets r
[RING_FINITE_UNION_ALT] Theorem
⊢ ∀r f n.
ring r ∧ (∀i. i < n ⇒ f i ∈ subsets r) ⇒
BIGUNION (IMAGE f (count n)) ∈ subsets r
[RING_IMP_SEMIRING] Theorem
⊢ ∀r. ring r ⇒ semiring r
[RING_INSERT] Theorem
⊢ ∀x A sp sts. ring (sp,sts) ∧ {x} ∈ sts ∧ A ∈ sts ⇒ x INSERT A ∈ sts
[RING_INTER] Theorem
⊢ ∀r s t. ring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∩ t ∈ subsets r
[RING_SETS_COLLECT_FINITE] Theorem
⊢ ∀sp sts s P.
ring (sp,sts) ∧ (∀i. i ∈ s ⇒ equiv_class P sp i ∈ sts) ∧ FINITE s ⇒
{x | x ∈ sp ∧ ∃i. i ∈ s ∧ P i x} ∈ sts
[RING_SPACE_IMP_ALGEBRA] Theorem
⊢ ∀r. ring r ∧ space r ∈ subsets r ⇒ algebra r
[RING_UNION] Theorem
⊢ ∀r s t. ring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∪ t ∈ subsets r
[SEMIRING_DIFF] Theorem
⊢ ∀r s t.
semiring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒
∃c. c ⊆ subsets r ∧ FINITE c ∧ disjoint c ∧ s DIFF t = BIGUNION c
[SEMIRING_DIFF_ALT] Theorem
⊢ ∀r s t.
semiring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒
∃f n.
(∀i. i < n ⇒ f i ∈ subsets r) ∧
(∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
s DIFF t = BIGUNION (IMAGE f (count n))
[SEMIRING_EMPTY] Theorem
⊢ ∀r. semiring r ⇒ ∅ ∈ subsets r
[SEMIRING_FINITE_INTER] Theorem
⊢ ∀r f n.
semiring r ∧ 0 < n ∧ (∀i. i < n ⇒ f i ∈ subsets r) ⇒
BIGINTER (IMAGE f (count n)) ∈ subsets r
[SEMIRING_FINITE_INTER'] Theorem
⊢ ∀r c.
semiring r ∧ FINITE c ∧ c ⊆ subsets r ∧ c ≠ ∅ ⇒
BIGINTER c ∈ subsets r
[SEMIRING_INTER] Theorem
⊢ ∀r s t.
semiring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∩ t ∈ subsets r
[SEMIRING_PROD_SETS] Theorem
⊢ ∀a b.
semiring a ∧ semiring b ⇒
semiring (space a × space b,prod_sets (subsets a) (subsets b))
[SEMIRING_PROD_SETS'] Theorem
⊢ ∀a b.
sigma_algebra a ∧ sigma_algebra b ⇒
semiring (space a × space b,prod_sets (subsets a) (subsets b))
[SEMIRING_SETS_COLLECT] Theorem
⊢ ∀sp sts P Q.
semiring (sp,sts) ∧ {x | x ∈ sp ∧ P x} ∈ sts ∧
{x | x ∈ sp ∧ Q x} ∈ sts ⇒
{x | x ∈ sp ∧ P x ∧ Q x} ∈ sts
[SIGMA_ALGEBRA] Theorem
⊢ ∀p. sigma_algebra p ⇔
subset_class (space p) (subsets p) ∧ ∅ ∈ subsets p ∧
(∀s. s ∈ subsets p ⇒ space p DIFF s ∈ subsets p) ∧
∀c. countable c ∧ c ⊆ subsets p ⇒ BIGUNION c ∈ subsets p
[SIGMA_ALGEBRA_ALGEBRA] Theorem
⊢ ∀a. sigma_algebra a ⇒ algebra a
[SIGMA_ALGEBRA_ALT] Theorem
⊢ ∀a. sigma_algebra a ⇔
algebra a ∧
∀f. f ∈ (𝕌(:num) → subsets a) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
[SIGMA_ALGEBRA_ALT_DISJOINT] Theorem
⊢ ∀a. sigma_algebra a ⇔
algebra a ∧
∀f. f ∈ (𝕌(:num) → subsets a) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
[SIGMA_ALGEBRA_ALT_MONO] Theorem
⊢ ∀a. sigma_algebra a ⇔
algebra a ∧
∀f. f ∈ (𝕌(:num) → subsets a) ∧ f 0 = ∅ ∧ (∀n. f n ⊆ f (SUC n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
[SIGMA_ALGEBRA_ALT_SPACE] Theorem
⊢ ∀a. sigma_algebra a ⇔
subset_class (space a) (subsets a) ∧ space a ∈ subsets a ∧
(∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
∀f. f ∈ (𝕌(:num) → subsets a) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
[SIGMA_ALGEBRA_COMPL] Theorem
⊢ ∀a s. sigma_algebra a ∧ s ∈ subsets a ⇒ space a DIFF s ∈ subsets a
[SIGMA_ALGEBRA_COUNTABLE_INT] Theorem
⊢ ∀sp sts A X.
sigma_algebra (sp,sts) ∧ IMAGE A X ⊆ sts ∧ X ≠ ∅ ⇒
BIGINTER {A x | x ∈ X} ∈ sts
[SIGMA_ALGEBRA_COUNTABLE_INT'] Theorem
⊢ ∀sp sts A X.
sigma_algebra (sp,sts) ∧ countable X ∧ X ≠ ∅ ∧ IMAGE A X ⊆ sts ⇒
BIGINTER {A x | x ∈ X} ∈ sts
[SIGMA_ALGEBRA_COUNTABLE_UN] Theorem
⊢ ∀sp sts A X.
sigma_algebra (sp,sts) ∧ IMAGE A X ⊆ sts ⇒
BIGUNION {A x | x ∈ X} ∈ sts
[SIGMA_ALGEBRA_COUNTABLE_UN'] Theorem
⊢ ∀sp sts A X.
sigma_algebra (sp,sts) ∧ IMAGE A X ⊆ sts ∧ countable X ⇒
BIGUNION {A x | x ∈ X} ∈ sts
[SIGMA_ALGEBRA_COUNTABLE_UNION] Theorem
⊢ ∀a c.
sigma_algebra a ∧ countable c ∧ c ⊆ subsets a ⇒
BIGUNION c ∈ subsets a
[SIGMA_ALGEBRA_DIFF] Theorem
⊢ ∀a s t.
sigma_algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒
s DIFF t ∈ subsets a
[SIGMA_ALGEBRA_EMPTY] Theorem
⊢ ∀a. sigma_algebra a ⇒ ∅ ∈ subsets a
[SIGMA_ALGEBRA_ENUM] Theorem
⊢ ∀a f.
sigma_algebra a ∧ f ∈ (𝕌(:num) → subsets a) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
[SIGMA_ALGEBRA_FINITE_INTER] Theorem
⊢ ∀a f n.
sigma_algebra a ∧ 0 < n ∧ (∀i. i < n ⇒ f i ∈ subsets a) ⇒
BIGINTER (IMAGE f (count n)) ∈ subsets a
[SIGMA_ALGEBRA_FINITE_INTER'] Theorem
⊢ ∀a c.
sigma_algebra a ∧ FINITE c ∧ c ⊆ subsets a ∧ c ≠ ∅ ⇒
BIGINTER c ∈ subsets a
[SIGMA_ALGEBRA_FINITE_UNION] Theorem
⊢ ∀a c.
sigma_algebra a ∧ FINITE c ∧ c ⊆ subsets a ⇒
BIGUNION c ∈ subsets a
[SIGMA_ALGEBRA_FN] Theorem
⊢ ∀a. sigma_algebra a ⇔
subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
(∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
∀f. f ∈ (𝕌(:num) → subsets a) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
[SIGMA_ALGEBRA_FN_BIGINTER] Theorem
⊢ ∀a. sigma_algebra a ⇒
subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
(∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
∀f. f ∈ (𝕌(:num) → subsets a) ⇒
BIGINTER (IMAGE f 𝕌(:num)) ∈ subsets a
[SIGMA_ALGEBRA_FN_DISJOINT] Theorem
⊢ ∀a. sigma_algebra a ⇔
subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
(∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
(∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a) ∧
∀f. f ∈ (𝕌(:num) → subsets a) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a
[SIGMA_ALGEBRA_IMP_DYNKIN_SYSTEM] Theorem
⊢ ∀a. sigma_algebra a ⇒ dynkin_system a
[SIGMA_ALGEBRA_INTER] Theorem
⊢ ∀a s t.
sigma_algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒
s ∩ t ∈ subsets a
[SIGMA_ALGEBRA_PROD_SIGMA] Theorem
⊢ ∀a b.
subset_class (space a) (subsets a) ∧
subset_class (space b) (subsets b) ⇒
sigma_algebra (a × b)
[SIGMA_ALGEBRA_PROD_SIGMA'] Theorem
⊢ ∀X Y A B.
subset_class X A ∧ subset_class Y B ⇒
sigma_algebra ((X,A) × (Y,B))
[SIGMA_ALGEBRA_PROD_SIGMA_WEAK] Theorem
⊢ ∀a b. sigma_algebra a ∧ sigma_algebra b ⇒ sigma_algebra (a × b)
[SIGMA_ALGEBRA_RESTRICT] Theorem
⊢ ∀sp sts a.
sigma_algebra (sp,sts) ∧ a ∈ sts ⇒
sigma_algebra (a,IMAGE (λs. s ∩ a) sts)
[SIGMA_ALGEBRA_RESTRICT'] Theorem
⊢ ∀sp sts a.
sigma_algebra (sp,sts) ∧ a ⊆ sp ⇒
sigma_algebra (a,IMAGE (λs. s ∩ a) sts)
[SIGMA_ALGEBRA_RESTRICT_SUBSET] Theorem
⊢ ∀sp sts a.
sigma_algebra (sp,sts) ∧ a ∈ sts ⇒ IMAGE (λs. s ∩ a) sts ⊆ sts
[SIGMA_ALGEBRA_SIGMA] Theorem
⊢ ∀sp sts. subset_class sp sts ⇒ sigma_algebra (sigma sp sts)
[SIGMA_ALGEBRA_SPACE] Theorem
⊢ ∀a. sigma_algebra a ⇒ space a ∈ subsets a
[SIGMA_ALGEBRA_SUBSET_SPACE] Theorem
⊢ ∀a s. sigma_algebra a ∧ s ∈ subsets a ⇒ s ⊆ space a
[SIGMA_ALGEBRA_UNION] Theorem
⊢ ∀a s t.
sigma_algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒
s ∪ t ∈ subsets a
[SIGMA_CONG] Theorem
⊢ ∀sp a b.
subsets (sigma sp a) = subsets (sigma sp b) ⇒
sigma sp a = sigma sp b
[SIGMA_MEASURABLE] Theorem
⊢ ∀sp A f.
sigma_algebra A ∧ f ∈ (sp → space A) ⇒
f ∈ measurable (sigma sp A f) A
[SIGMA_MONOTONE] Theorem
⊢ ∀sp a b. a ⊆ b ⇒ subsets (sigma sp a) ⊆ subsets (sigma sp b)
[SIGMA_POW] Theorem
⊢ ∀s. sigma s (POW s) = (s,POW s)
[SIGMA_PROPERTY] Theorem
⊢ ∀sp p a.
subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
(∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
(∀c. countable c ∧ c ⊆ p ∩ subsets (sigma sp a) ⇒ BIGUNION c ∈ p) ⇒
subsets (sigma sp a) ⊆ p
[SIGMA_PROPERTY_ALT] Theorem
⊢ ∀sp p a.
subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
(∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
(∀f. f ∈ (𝕌(:num) → p ∩ subsets (sigma sp a)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
subsets (sigma sp a) ⊆ p
[SIGMA_PROPERTY_DISJOINT] Theorem
⊢ ∀sp p a.
algebra (sp,a) ∧ a ⊆ p ∧
(∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
(∀f. f ∈ (𝕌(:num) → p ∩ subsets (sigma sp a)) ∧ f 0 = ∅ ∧
(∀n. f n ⊆ f (SUC n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ∧
(∀f. f ∈ (𝕌(:num) → p ∩ subsets (sigma sp a)) ∧
(∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
subsets (sigma sp a) ⊆ p
[SIGMA_PROPERTY_DISJOINT_LEMMA] Theorem
⊢ ∀sp a d.
algebra (sp,a) ∧ a ⊆ d ∧ dynkin_system (sp,d) ⇒
subsets (sigma sp a) ⊆ d
[SIGMA_PROPERTY_DISJOINT_LEMMA1] Theorem
⊢ ∀sp sts.
algebra (sp,sts) ⇒
∀s t.
s ∈ sts ∧ t ∈ subsets (dynkin sp sts) ⇒
s ∩ t ∈ subsets (dynkin sp sts)
[SIGMA_PROPERTY_DISJOINT_LEMMA2] Theorem
⊢ ∀sp sts.
algebra (sp,sts) ⇒
∀s t.
s ∈ subsets (dynkin sp sts) ∧ t ∈ subsets (dynkin sp sts) ⇒
s ∩ t ∈ subsets (dynkin sp sts)
[SIGMA_PROPERTY_DISJOINT_WEAK] Theorem
⊢ ∀sp p a.
subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
(∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
(∀s t. s ∈ p ∧ t ∈ p ⇒ s ∪ t ∈ p) ∧
(∀f. f ∈ (𝕌(:num) → p ∩ subsets (sigma sp a)) ∧
(∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
subsets (sigma sp a) ⊆ p
[SIGMA_PROPERTY_DISJOINT_WEAK_ALT] Theorem
⊢ ∀sp p a.
algebra (sp,a) ∧ a ⊆ p ∧ subset_class sp p ∧
(∀s. s ∈ p ⇒ sp DIFF s ∈ p) ∧
(∀f. f ∈ (𝕌(:num) → p) ∧ f 0 = ∅ ∧ (∀n. f n ⊆ f (SUC n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ∧
(∀f. f ∈ (𝕌(:num) → p) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
subsets (sigma sp a) ⊆ p
[SIGMA_REDUCE] Theorem
⊢ ∀sp a. (sp,subsets (sigma sp a)) = sigma sp a
[SIGMA_RESTRICT] Theorem
⊢ ∀sp sts B.
subset_class sp sts ∧ B ⊆ sp ⇒
sigma_algebra (B,IMAGE (λs. s ∩ B) (subsets (sigma sp sts))) ∧
subsets (sigma B (IMAGE (λs. s ∩ B) sts)) =
IMAGE (λs. s ∩ B) (subsets (sigma sp sts))
[SIGMA_SIMULTANEOUSLY_MEASURABLE] Theorem
⊢ ∀sp A f J.
(∀i. i ∈ J ⇒ sigma_algebra (A i)) ∧
(∀i. f i ∈ (sp → space (A i))) ⇒
∀i. i ∈ J ⇒ f i ∈ measurable (sigma sp A f J) (A i)
[SIGMA_SMALLEST] Theorem
⊢ ∀sp sts A.
sts ⊆ A ∧ A ⊆ subsets (sigma sp sts) ∧ sigma_algebra (sp,A) ⇒
A = subsets (sigma sp sts)
[SIGMA_STABLE] Theorem
⊢ ∀a. sigma_algebra a ⇒ sigma (space a) (subsets a) = a
[SIGMA_STABLE_LEMMA] Theorem
⊢ ∀sp sts. sigma_algebra (sp,sts) ⇒ sigma sp sts = (sp,sts)
[SIGMA_SUBSET] Theorem
⊢ ∀a b.
sigma_algebra b ∧ a ⊆ subsets b ⇒
subsets (sigma (space b) a) ⊆ subsets b
[SIGMA_SUBSET_SUBSETS] Theorem
⊢ ∀sp a. a ⊆ subsets (sigma sp a)
[SMALLEST_RING] Theorem
⊢ ∀sp sts. subset_class sp sts ⇒ ring (smallest_ring sp sts)
[SMALLEST_RING_OF_SEMIRING] Theorem
⊢ ∀sp sts.
semiring (sp,sts) ⇒
subsets (smallest_ring sp sts) =
{BIGUNION c | c ⊆ sts ∧ FINITE c ∧ disjoint c}
[SMALLEST_RING_SUBSET_SUBSETS] Theorem
⊢ ∀sp a. a ⊆ subsets (smallest_ring sp a)
[SPACE] Theorem
⊢ ∀a. (space a,subsets a) = a
[SPACE_DYNKIN] Theorem
⊢ ∀sp sts. space (dynkin sp sts) = sp
[SPACE_PROD_SIGMA] Theorem
⊢ ∀a b. space (a × b) = space a × space b
[SPACE_SIGMA] Theorem
⊢ ∀sp a. space (sigma sp a) = sp
[SPACE_SMALLEST_RING] Theorem
⊢ ∀sp sts. space (smallest_ring sp sts) = sp
[TRACE_SIGMA_ALGEBRA] Theorem
⊢ ∀a E.
sigma_algebra a ∧ E ⊆ space a ⇒
sigma_algebra (E,{A ∩ E | A ∈ subsets a})
[UNIV_SIGMA_ALGEBRA] Theorem
⊢ sigma_algebra (𝕌(:α),𝕌(:α -> bool))
[algebra_alt] Theorem
⊢ ∀sp sts. algebra (sp,sts) ⇔ ring (sp,sts) ∧ sp ∈ sts
[algebra_alt_inter] Theorem
⊢ ∀sp sts.
algebra (sp,sts) ⇔
sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀a. a ∈ sts ⇒ sp DIFF a ∈ sts) ∧
∀a b. a ∈ sts ∧ b ∈ sts ⇒ a ∩ b ∈ sts
[algebra_alt_union] Theorem
⊢ ∀sp sts.
algebra (sp,sts) ⇔
sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀a. a ∈ sts ⇒ sp DIFF a ∈ sts) ∧
∀a b. a ∈ sts ∧ b ∈ sts ⇒ a ∪ b ∈ sts
[algebra_finite_space_imp_sigma_algebra] Theorem
⊢ ∀a. algebra a ∧ FINITE (space a) ⇒ sigma_algebra a
[algebra_finite_subsets_imp_sigma_algebra] Theorem
⊢ ∀a. algebra a ∧ FINITE (subsets a) ⇒ sigma_algebra a
[prod_sigma_alt_sigma_functions] Theorem
⊢ ∀A B.
sigma_algebra A ∧ sigma_algebra B ⇒
A × B =
sigma (space A × space B) (binary A B) (binary FST SND) {0; 1}
[prod_sigma_alt_sigma_functions'] Theorem
⊢ ∀A B.
algebra A ∧ algebra B ⇒
A × B =
sigma (space A × space B) (binary A B) (binary FST SND) {0; 1}
[ring_alt] Theorem
⊢ ∀sp sts.
ring (sp,sts) ⇔
subset_class sp sts ∧ ∅ ∈ sts ∧
(∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∪ t ∈ sts) ∧
∀s t. s ∈ sts ∧ t ∈ sts ⇒ s DIFF t ∈ sts
[ring_alt_pow] Theorem
⊢ ∀sp sts.
ring (sp,sts) ⇔
sts ⊆ POW sp ∧ ∅ ∈ sts ∧
(∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∪ t ∈ sts) ∧
∀s t. s ∈ sts ∧ t ∈ sts ⇒ s DIFF t ∈ sts
[ring_alt_pow_imp] Theorem
⊢ ∀sp sts.
sts ⊆ POW sp ∧ ∅ ∈ sts ∧
(∀a b. a ∈ sts ∧ b ∈ sts ⇒ a ∪ b ∈ sts) ∧
(∀a b. a ∈ sts ∧ b ∈ sts ⇒ a DIFF b ∈ sts) ⇒
ring (sp,sts)
[ring_and_semiring] Theorem
⊢ ∀r. ring r ⇔
semiring r ∧
∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∪ t ∈ subsets r
[ring_disjointed_sets] Theorem
⊢ ∀sp sts A.
ring (sp,sts) ∧ IMAGE A 𝕌(:num) ⊆ sts ⇒
IMAGE (λn. disjointed A n) 𝕌(:num) ⊆ sts
[semiring_alt] Theorem
⊢ ∀sp sts.
semiring (sp,sts) ⇔
subset_class sp sts ∧ ∅ ∈ sts ∧
(∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
∀s t.
s ∈ sts ∧ t ∈ sts ⇒
∃c. c ⊆ sts ∧ FINITE c ∧ disjoint c ∧ s DIFF t = BIGUNION c
[sigma_algebra_alt] Theorem
⊢ ∀sp sts.
sigma_algebra (sp,sts) ⇔
algebra (sp,sts) ∧
∀A. IMAGE A 𝕌(:num) ⊆ sts ⇒ BIGUNION {A i | i ∈ 𝕌(:num)} ∈ sts
[sigma_algebra_alt_pow] Theorem
⊢ ∀sp sts.
sigma_algebra (sp,sts) ⇔
sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀s. s ∈ sts ⇒ sp DIFF s ∈ sts) ∧
∀A. IMAGE A 𝕌(:num) ⊆ sts ⇒ BIGUNION {A i | i ∈ 𝕌(:num)} ∈ sts
[sigma_algebra_sigma_function] Theorem
⊢ ∀sp A f.
sigma_algebra A ∧ f ∈ (sp → space A) ⇒
sigma_algebra (sigma sp A f)
[sigma_algebra_sigma_functions] Theorem
⊢ ∀sp A f J.
(∀i. f i ∈ (sp → space (A i))) ⇒ sigma_algebra (sigma sp A f J)
[sigma_algebra_sigma_sets] Theorem
⊢ ∀sp st. st ⊆ POW sp ⇒ sigma_algebra (sp,sigma_sets sp st)
[sigma_function_alt_sigma_functions] Theorem
⊢ ∀sp A X.
sigma_algebra A ∧ X ∈ (sp → space A) ⇒
sigma sp A X = sigma sp (λn. A) (λn x. X x) (count 1)
[sigma_function_subset] Theorem
⊢ ∀A B f.
sigma_algebra A ∧ f ∈ measurable A B ⇒
subsets (sigma (space A) B f) ⊆ subsets A
[sigma_functions_1] Theorem
⊢ ∀sp A f.
sigma_algebra A ∧ f 0 ∈ (sp → space A) ⇒
sigma sp (λn. A) f (count 1) = sigma sp A (f 0)
[sigma_functions_subset] Theorem
⊢ ∀A B f J.
sigma_algebra A ∧ (∀i. i ∈ J ⇒ sigma_algebra (B i)) ∧
(∀i. i ∈ J ⇒ f i ∈ measurable A (B i)) ⇒
subsets (sigma (space A) B f J) ⊆ subsets A
[sigma_sets_BIGINTER] Theorem
⊢ ∀sp st A.
st ⊆ POW sp ⇒
(∀i. A i ∈ sigma_sets sp st) ⇒
BIGINTER {A i | i ∈ 𝕌(:num)} ∈ sigma_sets sp st
[sigma_sets_BIGINTER2] Theorem
⊢ ∀sp st A N.
st ⊆ POW sp ∧ (∀i. i ∈ N ⇒ A i ∈ sigma_sets sp st) ∧ N ≠ ∅ ⇒
BIGINTER {A i | i ∈ N} ∈ sigma_sets sp st
[sigma_sets_BIGUNION] Theorem
⊢ ∀sp st A.
(∀i. A i ∈ sigma_sets sp st) ⇒
BIGUNION {A i | i ∈ 𝕌(:num)} ∈ sigma_sets sp st
[sigma_sets_basic] Theorem
⊢ ∀sp st a. a ∈ st ⇒ a ∈ sigma_sets sp st
[sigma_sets_cases] Theorem
⊢ ∀sp st a0.
sigma_sets sp st a0 ⇔
a0 = ∅ ∨ st a0 ∨ (∃a. a0 = sp DIFF a ∧ sigma_sets sp st a) ∨
∃A. a0 = BIGUNION {A i | i ∈ 𝕌(:num)} ∧
∀i. sigma_sets sp st (A i)
[sigma_sets_compl] Theorem
⊢ ∀sp st a. a ∈ sigma_sets sp st ⇒ sp DIFF a ∈ sigma_sets sp st
[sigma_sets_empty] Theorem
⊢ ∀sp st. ∅ ∈ sigma_sets sp st
[sigma_sets_fixpoint] Theorem
⊢ ∀sp sts. sigma_algebra (sp,sts) ⇒ sigma_sets sp sts = sts
[sigma_sets_ind] Theorem
⊢ ∀sp st sigma_sets'.
sigma_sets' ∅ ∧ (∀a. st a ⇒ sigma_sets' a) ∧
(∀a. sigma_sets' a ⇒ sigma_sets' (sp DIFF a)) ∧
(∀A. (∀i. sigma_sets' (A i)) ⇒
sigma_sets' (BIGUNION {A i | i ∈ 𝕌(:num)})) ⇒
∀a0. sigma_sets sp st a0 ⇒ sigma_sets' a0
[sigma_sets_into_sp] Theorem
⊢ ∀sp st. st ⊆ POW sp ⇒ ∀x. x ∈ sigma_sets sp st ⇒ x ⊆ sp
[sigma_sets_least_sigma_algebra] Theorem
⊢ ∀sp A.
A ⊆ POW sp ⇒
sigma_sets sp A = BIGINTER {B | A ⊆ B ∧ sigma_algebra (sp,B)}
[sigma_sets_rules] Theorem
⊢ ∀sp st.
sigma_sets sp st ∅ ∧ (∀a. st a ⇒ sigma_sets sp st a) ∧
(∀a. sigma_sets sp st a ⇒ sigma_sets sp st (sp DIFF a)) ∧
∀A. (∀i. sigma_sets sp st (A i)) ⇒
sigma_sets sp st (BIGUNION {A i | i ∈ 𝕌(:num)})
[sigma_sets_strongind] Theorem
⊢ ∀sp st sigma_sets'.
sigma_sets' ∅ ∧ (∀a. st a ⇒ sigma_sets' a) ∧
(∀a. sigma_sets sp st a ∧ sigma_sets' a ⇒ sigma_sets' (sp DIFF a)) ∧
(∀A. (∀i. sigma_sets sp st (A i) ∧ sigma_sets' (A i)) ⇒
sigma_sets' (BIGUNION {A i | i ∈ 𝕌(:num)})) ⇒
∀a0. sigma_sets sp st a0 ⇒ sigma_sets' a0
[sigma_sets_subset] Theorem
⊢ ∀sp sts st.
sigma_algebra (sp,sts) ∧ st ⊆ sts ⇒ sigma_sets sp st ⊆ sts
[sigma_sets_superset_generator] Theorem
⊢ ∀X A. A ⊆ sigma_sets X A
[sigma_sets_top] Theorem
⊢ ∀sp A. sp ∈ sigma_sets sp A
[sigma_sets_union] Theorem
⊢ ∀sp st a b.
a ∈ sigma_sets sp st ∧ b ∈ sigma_sets sp st ⇒
a ∪ b ∈ sigma_sets sp st
[space_sigma_function] Theorem
⊢ ∀sp A f. space (sigma sp A f) = sp
[space_sigma_functions] Theorem
⊢ ∀sp A f J. space (sigma sp A f J) = sp
[subset_class_POW] Theorem
⊢ ∀sp. subset_class sp (POW sp)
*)
end
HOL 4, Trindemossen-1