Structure sigma_algebraTheory
signature sigma_algebraTheory =
sig
type thm = Thm.thm
(* Definitions *)
val algebra_def : thm
val binary_def : thm
val disjoint_family_on : thm
val disjointed : thm
val dynkin_def : thm
val dynkin_system_def : thm
val measurable_def : thm
val prod_sets_def : thm
val prod_sigma_def : thm
val restrict_algebra_def : thm
val ring_def : thm
val semiring_def : thm
val set_liminf_def : thm
val set_limsup_def : thm
val sigma_algebra_alt : 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 BIGINTER_OVER_INTER_L : thm
val BIGINTER_OVER_INTER_R : thm
val BIGINTER_PAIR : thm
val BIGUNION_IMAGE_BIGUNION_IMAGE_UNIV : thm
val BIGUNION_IMAGE_COUNT_IMP_UNIV : thm
val BIGUNION_IMAGE_UNIV_CROSS_UNIV : thm
val BIGUNION_OVER_DIFF : thm
val BIGUNION_OVER_INTER_L : thm
val BIGUNION_OVER_INTER_R : thm
val BIGUNION_disjointed : thm
val BINARY_RANGE : thm
val COMPL_BIGINTER : thm
val COMPL_BIGINTER_IMAGE : thm
val COMPL_BIGUNION : thm
val COMPL_BIGUNION_IMAGE : thm
val DIFF_INTER_PAIR : thm
val DINTER_IMP_FINITE_INTER : thm
val DISJOINT_CROSS_L : thm
val DISJOINT_CROSS_R : thm
val DISJOINT_RESTRICT_L : thm
val DISJOINT_RESTRICT_R : thm
val DUNION_IMP_FINITE_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 FINITE_TWO : thm
val GBIGUNION_IMAGE : thm
val GEN_COMPL_BIGINTER : thm
val GEN_COMPL_BIGINTER_IMAGE : thm
val GEN_COMPL_BIGUNION : thm
val GEN_COMPL_BIGUNION_IMAGE : thm
val GEN_COMPL_FINITE_INTER : thm
val GEN_COMPL_FINITE_UNION : thm
val GEN_COMPL_INTER : thm
val GEN_COMPL_UNION : thm
val GEN_DIFF_INTER : thm
val IMAGE_SIGMA : thm
val IMAGE_SIGMA_ALGEBRA : thm
val INCREASING_TO_DISJOINT_SETS : thm
val INCREASING_TO_DISJOINT_SETS' : thm
val INTER_BINARY : thm
val INTER_SPACE_EQ1 : thm
val INTER_SPACE_REDUCE : thm
val IN_DYNKIN : thm
val IN_LIMINF : thm
val IN_LIMSUP : 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_PROD_SETS : thm
val IN_SIGMA : thm
val IN_SPACE_PROD_SIGMA : thm
val LIMSUP_COMPL : thm
val LIMSUP_DIFF : thm
val LIMSUP_MONO_STRONG : thm
val LIMSUP_MONO_STRONGER : thm
val LIMSUP_MONO_WEAK : 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_PAIR : 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 SETS_TO_DISJOINT_SETS : thm
val SETS_TO_DISJOINT_SETS' : thm
val SETS_TO_INCREASING_SETS : thm
val SETS_TO_INCREASING_SETS' : 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_SIGMA_UNIV : 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_PROPERTY_DYNKIN : 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 SUBSET_DIFF_DISJOINT : thm
val SUBSET_DIFF_SUBSET : thm
val SUBSET_INTER_SUBSET_L : thm
val SUBSET_INTER_SUBSET_R : thm
val SUBSET_MONO_DIFF : thm
val SUBSET_RESTRICT_DIFF : thm
val SUBSET_RESTRICT_L : thm
val SUBSET_RESTRICT_R : thm
val SUBSET_TWO : thm
val TRACE_SIGMA_ALGEBRA : thm
val UNION_BINARY : thm
val UNION_TO_3_DISJOINT_UNIONS : 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 count1_def : thm
val count1_numseg : thm
val disjoint_family_def : thm
val disjoint_family_disjoint : thm
val disjoint_family_on_def : thm
val disjoint_family_on_iff_disjoint : thm
val disjoint_family_on_imp_disjoint : thm
val disjointed_subset : thm
val finite_decomposition : thm
val finite_decomposition_simple : thm
val finite_disjoint_decomposition : thm
val finite_disjoint_decomposition' : thm
val finite_enumeration_of_sets_has_max_non_empty : thm
val infinitely_often_lemma : thm
val infinity_bound_lemma : thm
val prod_sigma_alt_sigma_functions : thm
val prod_sigma_alt_sigma_functions' : thm
val restrict_algebra_SUBSET : thm
val restrict_algebra_reduce : thm
val restrict_algebra_reduce' : 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 set_limsup_alt : thm
val sigma_algebra_alt_eq : thm
val sigma_algebra_alt_pow : thm
val sigma_algebra_eq_alt : thm
val sigma_algebra_iff2 : thm
val sigma_algebra_restrict_algebra : 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_eq : 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_sigma : 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 tail_countable : thm
val tail_not_empty : thm
val trivial_algebra_of_space : thm
val trivial_algebra_of_two_points : thm
val trivial_algebra_of_two_sets : thm
(*
[nets] 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
[binary_def] Definition
⊢ ∀a b. binary a b = (λx. if x = 0 then a else b)
[disjoint_family_on] Definition
⊢ ∀a s.
disjoint_family_on a s ⇔
∀m n. m ∈ s ∧ n ∈ s ∧ m ≠ n ⇒ a m ∩ a n = ∅
[disjointed] Definition
⊢ ∀A n.
disjointed A n =
A n DIFF BIGUNION {A i | i ∈ {x | 0 ≤ x ∧ x < n}}
[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_sets_def] Definition
⊢ ∀a b. prod_sets a b = {s × t | s ∈ a ∧ t ∈ b}
[prod_sigma_def] Definition
⊢ ∀a b.
a × b =
sigma (space a × space b) (prod_sets (subsets a) (subsets b))
[restrict_algebra_def] Definition
⊢ ∀A sp.
restrict_algebra A sp =
(sp ∩ space A,IMAGE (λa. a ∩ sp) (subsets A))
[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
[set_liminf_def] Definition
⊢ ∀E. liminf E =
BIGUNION (IMAGE (λm. BIGINTER {E n | m ≤ n}) 𝕌(:num))
[set_limsup_def] Definition
⊢ ∀E. limsup E =
BIGINTER (IMAGE (λm. BIGUNION {E n | m ≤ n}) 𝕌(:num))
[sigma_algebra_alt] Definition
⊢ ∀sp sts.
sigma_algebra_alt sp sts ⇔
algebra (sp,sts) ∧
∀A. IMAGE A 𝕌(:num) ⊆ sts ⇒ BIGUNION {A i | i ∈ 𝕌(:num)} ∈ sts
[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
[BIGINTER_OVER_INTER_L] Theorem
⊢ ∀f s d.
s ≠ ∅ ⇒
BIGINTER (IMAGE f s) ∩ d = BIGINTER (IMAGE (λi. f i ∩ d) s)
[BIGINTER_OVER_INTER_R] Theorem
⊢ ∀f s d.
s ≠ ∅ ⇒
d ∩ BIGINTER (IMAGE f s) = BIGINTER (IMAGE (λi. d ∩ f i) s)
[BIGINTER_PAIR] Theorem
⊢ ∀s t. BIGINTER {s; t} = s ∩ t
[BIGUNION_IMAGE_BIGUNION_IMAGE_UNIV] Theorem
⊢ ∀f. BIGUNION (IMAGE (λn. BIGUNION (IMAGE (f n) 𝕌(:num))) 𝕌(:num)) =
BIGUNION (IMAGE (UNCURRY f) 𝕌(:num # num))
[BIGUNION_IMAGE_COUNT_IMP_UNIV] Theorem
⊢ ∀f g.
(∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ⇒
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[BIGUNION_IMAGE_UNIV_CROSS_UNIV] Theorem
⊢ ∀f h.
BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
BIGUNION (IMAGE (UNCURRY f) 𝕌(:num # num)) =
BIGUNION (IMAGE (UNCURRY f ∘ h) 𝕌(:num))
[BIGUNION_OVER_DIFF] Theorem
⊢ ∀f s d.
BIGUNION (IMAGE f s) DIFF d = BIGUNION (IMAGE (λi. f i DIFF d) s)
[BIGUNION_OVER_INTER_L] Theorem
⊢ ∀f s d. BIGUNION (IMAGE f s) ∩ d = BIGUNION (IMAGE (λi. f i ∩ d) s)
[BIGUNION_OVER_INTER_R] Theorem
⊢ ∀f s d. d ∩ BIGUNION (IMAGE f s) = BIGUNION (IMAGE (λi. d ∩ f i) s)
[BIGUNION_disjointed] Theorem
⊢ ∀A. BIGUNION {disjointed A i | i ∈ 𝕌(:num)} =
BIGUNION {A i | i ∈ 𝕌(:num)}
[BINARY_RANGE] Theorem
⊢ ∀a b. IMAGE (binary a b) 𝕌(:num) = {a; b}
[COMPL_BIGINTER] Theorem
⊢ ∀c. COMPL (BIGINTER c) = BIGUNION (IMAGE COMPL c)
[COMPL_BIGINTER_IMAGE] Theorem
⊢ ∀f. COMPL (BIGINTER (IMAGE f 𝕌(:num))) =
BIGUNION (IMAGE (COMPL ∘ f) 𝕌(:num))
[COMPL_BIGUNION] Theorem
⊢ ∀c. c ≠ ∅ ⇒ COMPL (BIGUNION c) = BIGINTER (IMAGE COMPL c)
[COMPL_BIGUNION_IMAGE] Theorem
⊢ ∀f. COMPL (BIGUNION (IMAGE f 𝕌(:num))) =
BIGINTER (IMAGE (COMPL ∘ f) 𝕌(:num))
[DIFF_INTER_PAIR] Theorem
⊢ ∀sp x y. sp DIFF x ∩ y = sp DIFF x ∪ (sp DIFF y)
[DINTER_IMP_FINITE_INTER] Theorem
⊢ ∀sts f.
(∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧ f ∈ (𝕌(:num) → sts) ⇒
∀n. 0 < n ⇒ BIGINTER (IMAGE f (count n)) ∈ sts
[DISJOINT_CROSS_L] Theorem
⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (s × c) (t × c)
[DISJOINT_CROSS_R] Theorem
⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (c × s) (c × t)
[DISJOINT_RESTRICT_L] Theorem
⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (s ∩ c) (t ∩ c)
[DISJOINT_RESTRICT_R] Theorem
⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (c ∩ s) (c ∩ t)
[DUNION_IMP_FINITE_UNION] Theorem
⊢ ∀sts f.
(∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∪ t ∈ sts) ⇒
∀n. 0 < n ∧ (∀i. i < n ⇒ f i ∈ sts) ⇒
BIGUNION (IMAGE f (count n)) ∈ sts
[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
[FINITE_TWO] Theorem
⊢ ∀s t. FINITE {s; t}
[GBIGUNION_IMAGE] Theorem
⊢ ∀s p n. {s | ∃n. p s n} = BIGUNION (IMAGE (λn. {s | p s n}) 𝕌(:γ))
[GEN_COMPL_BIGINTER] Theorem
⊢ ∀sp c.
(∀x. x ∈ c ⇒ x ⊆ sp) ⇒
sp DIFF BIGINTER c = BIGUNION (IMAGE (λx. sp DIFF x) c)
[GEN_COMPL_BIGINTER_IMAGE] Theorem
⊢ ∀sp f.
(∀n. f n ⊆ sp) ⇒
sp DIFF BIGINTER (IMAGE f 𝕌(:num)) =
BIGUNION (IMAGE (λn. sp DIFF f n) 𝕌(:num))
[GEN_COMPL_BIGUNION] Theorem
⊢ ∀sp c.
c ≠ ∅ ∧ (∀x. x ∈ c ⇒ x ⊆ sp) ⇒
sp DIFF BIGUNION c = BIGINTER (IMAGE (λx. sp DIFF x) c)
[GEN_COMPL_BIGUNION_IMAGE] Theorem
⊢ ∀sp f.
(∀n. f n ⊆ sp) ⇒
sp DIFF BIGUNION (IMAGE f 𝕌(:num)) =
BIGINTER (IMAGE (λn. sp DIFF f n) 𝕌(:num))
[GEN_COMPL_FINITE_INTER] Theorem
⊢ ∀sp f n.
0 < n ⇒
sp DIFF BIGINTER (IMAGE f (count n)) =
BIGUNION (IMAGE (λi. sp DIFF f i) (count n))
[GEN_COMPL_FINITE_UNION] Theorem
⊢ ∀sp f n.
0 < n ⇒
sp DIFF BIGUNION (IMAGE f (count n)) =
BIGINTER (IMAGE (λi. sp DIFF f i) (count n))
[GEN_COMPL_INTER] Theorem
⊢ ∀sp s t. s ⊆ sp ∧ t ⊆ sp ⇒ sp DIFF s ∩ t = sp DIFF s ∪ (sp DIFF t)
[GEN_COMPL_UNION] Theorem
⊢ ∀sp s t.
s ⊆ sp ∧ t ⊆ sp ⇒ sp DIFF (s ∪ t) = (sp DIFF s) ∩ (sp DIFF t)
[GEN_DIFF_INTER] Theorem
⊢ ∀sp s t. s ⊆ sp ∧ t ⊆ sp ⇒ s DIFF t = s ∩ (sp DIFF t)
[IMAGE_SIGMA] Theorem
⊢ ∀sp sts f.
subset_class sp sts ∧ BIJ f sp (IMAGE f sp) ⇒
IMAGE (IMAGE f) (subsets (sigma sp sts)) =
subsets (sigma (IMAGE f sp) (IMAGE (IMAGE f) sts))
[IMAGE_SIGMA_ALGEBRA] Theorem
⊢ ∀sp sts f.
sigma_algebra (sp,sts) ∧ BIJ f sp (IMAGE f sp) ⇒
sigma_algebra (IMAGE f sp,IMAGE (IMAGE f) sts)
[INCREASING_TO_DISJOINT_SETS] Theorem
⊢ ∀f. (∀n. f n ⊆ f (SUC n)) ⇒
∃g. g 0 = f 0 ∧ (∀n. 0 < n ⇒ g n = f n DIFF f (PRE n)) ∧
(∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[INCREASING_TO_DISJOINT_SETS'] Theorem
⊢ ∀f. f 0 = ∅ ∧ (∀n. f n ⊆ f (SUC n)) ⇒
∃g. (∀n. g n = f (SUC n) DIFF f n) ∧
(∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[INTER_BINARY] Theorem
⊢ ∀a b. a ∩ b = BIGINTER {binary a b i | i ∈ 𝕌(:num)}
[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_LIMINF] Theorem
⊢ ∀A x. x ∈ liminf A ⇔ ∃m. ∀n. m ≤ n ⇒ x ∈ A n
[IN_LIMSUP] Theorem
⊢ ∀A x. x ∈ limsup A ⇔ ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ x ∈ A n
[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_PROD_SETS] Theorem
⊢ ∀s a b. s ∈ prod_sets a b ⇔ ∃t u. s = t × u ∧ t ∈ a ∧ u ∈ b
[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
[LIMSUP_COMPL] Theorem
⊢ ∀E. COMPL (liminf E) = limsup (COMPL ∘ E)
[LIMSUP_DIFF] Theorem
⊢ ∀sp E. (∀n. E n ⊆ sp) ⇒ sp DIFF liminf E = limsup (λn. sp DIFF E n)
[LIMSUP_MONO_STRONG] Theorem
⊢ ∀A B. (∀y n. y ∈ A n ⇒ ∃m. n ≤ m ∧ y ∈ B m) ⇒ limsup A ⊆ limsup B
[LIMSUP_MONO_STRONGER] Theorem
⊢ ∀A B.
(∃d. ∀y n. y ∈ A n ⇒ ∃m. n − d ≤ m ∧ y ∈ B m) ⇒
limsup A ⊆ limsup B
[LIMSUP_MONO_WEAK] Theorem
⊢ ∀A B. (∀n. A n ⊆ B n) ⇒ limsup A ⊆ limsup 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_PAIR] Theorem
⊢ ∀a b1 b2 X Y.
sigma_algebra a ∧ sigma_algebra b1 ∧ sigma_algebra b2 ∧
X ∈ measurable a b1 ∧ Y ∈ measurable a b2 ⇒
(λx. (X x,Y x)) ∈ measurable a (b1 × b2)
[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
[SETS_TO_DISJOINT_SETS] Theorem
⊢ ∀sp sts f.
(∀s. s ∈ sts ⇒ s ⊆ sp) ∧ (∀n. f n ∈ sts) ⇒
∃g. g 0 = f 0 ∧
(∀n. 0 < n ⇒
g n = f n ∩ BIGINTER (IMAGE (λi. sp DIFF f i) (count n))) ∧
(∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[SETS_TO_DISJOINT_SETS'] Theorem
⊢ ∀f. ∃g.
g 0 = f 0 ∧
(∀n. 0 < n ⇒ g n = f n ∩ BIGINTER (IMAGE (COMPL ∘ f) (count n))) ∧
(∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[SETS_TO_INCREASING_SETS] Theorem
⊢ ∀f. ∃g.
g 0 = f 0 ∧ (∀n. g n = BIGUNION (IMAGE f (count1 n))) ∧
(∀n. g n ⊆ g (SUC n)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[SETS_TO_INCREASING_SETS'] Theorem
⊢ ∀f. ∃g.
g 0 = ∅ ∧ (∀n. g n = BIGUNION (IMAGE f (count n))) ∧
(∀n. g n ⊆ g (SUC n)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[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_SIGMA_UNIV] Theorem
⊢ ∀sts. sigma_algebra (sigma 𝕌(:α) 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_PROPERTY_DYNKIN] Theorem
⊢ ∀sp sts d.
subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
sts ⊆ d ∧ dynkin_system (sp,d) ⇒
subsets (sigma sp sts) ⊆ d
[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. i ∈ J ⇒ 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
[SUBSET_DIFF_DISJOINT] Theorem
⊢ ∀s1 s2 s3. s1 ⊆ s2 DIFF s3 ⇒ DISJOINT s1 s3
[SUBSET_DIFF_SUBSET] Theorem
⊢ ∀r s t. s ⊆ t ⇒ s DIFF r ⊆ t
[SUBSET_INTER_SUBSET_L] Theorem
⊢ ∀r s t. s ⊆ t ⇒ s ∩ r ⊆ t
[SUBSET_INTER_SUBSET_R] Theorem
⊢ ∀r s t. s ⊆ t ⇒ r ∩ s ⊆ t
[SUBSET_MONO_DIFF] Theorem
⊢ ∀r s t. s ⊆ t ⇒ s DIFF r ⊆ t DIFF r
[SUBSET_RESTRICT_DIFF] Theorem
⊢ ∀r s t. s ⊆ t ⇒ r DIFF t ⊆ r DIFF s
[SUBSET_RESTRICT_L] Theorem
⊢ ∀r s t. s ⊆ t ⇒ s ∩ r ⊆ t ∩ r
[SUBSET_RESTRICT_R] Theorem
⊢ ∀r s t. s ⊆ t ⇒ r ∩ s ⊆ r ∩ t
[SUBSET_TWO] Theorem
⊢ ∀N s t. N ⊆ {s; t} ∧ N ≠ ∅ ⇒ N = {s} ∨ N = {t} ∨ N = {s; t}
[TRACE_SIGMA_ALGEBRA] Theorem
⊢ ∀a E.
sigma_algebra a ∧ E ⊆ space a ⇒
sigma_algebra (E,{A ∩ E | A ∈ subsets a})
[UNION_BINARY] Theorem
⊢ ∀a b. a ∪ b = BIGUNION {binary a b i | i ∈ 𝕌(:num)}
[UNION_TO_3_DISJOINT_UNIONS] Theorem
⊢ ∀s t.
s ∪ t = s DIFF t ∪ s ∩ t ∪ (t DIFF s) ∧
disjoint {s DIFF t; s ∩ t; t DIFF s}
[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
[count1_def] Theorem
⊢ ∀n. count1 n = {m | m ≤ n}
[count1_numseg] Theorem
⊢ ∀n. count1 n = {0 .. n}
[disjoint_family_def] Theorem
⊢ ∀A. disjoint_family A ⇔ ∀i j. i ≠ j ⇒ DISJOINT (A i) (A j)
[disjoint_family_disjoint] Theorem
⊢ ∀A. disjoint_family (disjointed A)
[disjoint_family_on_def] Theorem
⊢ ∀A J.
disjoint_family_on A J ⇔
∀i j. i ∈ J ∧ j ∈ J ∧ i ≠ j ⇒ DISJOINT (A i) (A j)
[disjoint_family_on_iff_disjoint] Theorem
⊢ ∀a s.
INJ a s (IMAGE a s) ⇒
(disjoint_family_on a s ⇔ disjoint (IMAGE a s))
[disjoint_family_on_imp_disjoint] Theorem
⊢ ∀a s. disjoint_family_on a s ⇒ disjoint (IMAGE a s)
[disjointed_subset] Theorem
⊢ ∀A n. disjointed A n ⊆ A n
[finite_decomposition] Theorem
⊢ ∀c. FINITE c ⇒
∃f n.
(∀x. x < n ⇒ f x ∈ c) ∧ c = IMAGE f (count n) ∧
∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ f i ≠ f j
[finite_decomposition_simple] Theorem
⊢ ∀c. FINITE c ⇒ ∃f n. (∀x. x < n ⇒ f x ∈ c) ∧ c = IMAGE f (count n)
[finite_disjoint_decomposition] Theorem
⊢ ∀c. FINITE c ∧ disjoint c ⇒
∃f n.
(∀i. i < n ⇒ f i ∈ c) ∧ c = IMAGE f (count n) ∧
(∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ f i ≠ f j) ∧
∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)
[finite_disjoint_decomposition'] Theorem
⊢ ∀c. FINITE c ∧ disjoint c ⇒
∃f n.
(∀i. i < n ⇒ f i ∈ c) ∧ (∀i. n ≤ i ⇒ f i = ∅) ∧
c = IMAGE f (count n) ∧
BIGUNION c = BIGUNION (IMAGE f 𝕌(:num)) ∧
(∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ f i ≠ f j) ∧
∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)
[finite_enumeration_of_sets_has_max_non_empty] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. f x ∈ s) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
∃N. ∀n. n ≥ N ⇒ f n = ∅
[infinitely_often_lemma] Theorem
⊢ ∀P. ¬(∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n) ⇔ ∃m. ∀n. m ≤ n ⇒ ¬P n
[infinity_bound_lemma] Theorem
⊢ ∀N m. INFINITE N ⇒ ∃n. m ≤ n ∧ n ∈ N
[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}
[restrict_algebra_SUBSET] Theorem
⊢ ∀A sp.
sigma_algebra A ∧ sp ∈ subsets A ⇒
subsets (restrict_algebra A sp) ⊆ subsets A
[restrict_algebra_reduce] Theorem
⊢ ∀A. subset_class (space A) (subsets A) ⇒
restrict_algebra A (space A) = A
[restrict_algebra_reduce'] Theorem
⊢ ∀A. sigma_algebra A ⇒ restrict_algebra A (space A) = A
[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
[set_limsup_alt] Theorem
⊢ ∀E. limsup E =
BIGINTER (IMAGE (λn. BIGUNION (IMAGE E (from n))) 𝕌(:num))
[sigma_algebra_alt_eq] 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_eq_alt] Theorem
⊢ ∀sp sts. sigma_algebra (sp,sts) ⇔ sigma_algebra_alt sp sts
[sigma_algebra_iff2] 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_restrict_algebra] Theorem
⊢ ∀A sp.
sigma_algebra A ∧ sp ∈ subsets A ⇒
sigma_algebra (restrict_algebra A sp)
[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_eq] Theorem
⊢ ∀sp sts. sigma_algebra (sp,sts) ⇒ sigma_sets sp sts = sts
[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_sigma] Theorem
⊢ ∀sp A. A ⊆ POW sp ⇒ sigma_sets sp A = subsets (sigma sp A)
[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)
[tail_countable] Theorem
⊢ ∀A m. countable {A n | m ≤ n}
[tail_not_empty] Theorem
⊢ ∀A m. {A n | m ≤ n} ≠ ∅
[trivial_algebra_of_space] Theorem
⊢ ∀sp. algebra (sp,{∅; sp})
[trivial_algebra_of_two_points] Theorem
⊢ ∀h t. algebra ({h; t},{∅; {h}; {t}; {h; t}})
[trivial_algebra_of_two_sets] Theorem
⊢ ∀sp s. s ⊆ sp ⇒ algebra (sp,{∅; s; sp DIFF s; sp})
*)
end
HOL 4, Trindemossen-2