:: KOLMOG01 semantic presentation begin theorem :: KOLMOG01:1 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: KOLMOG01:2 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "not" (Bool (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "or" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: KOLMOG01:3 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k9_prob_1 :::"sigma"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "Omega")) ($#k2_tarski :::"}"::: ) )))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Sigma")); let "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); func :::"Indep"::: "(" "B" "," "P" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "Sigma" means :: KOLMOG01:def 1 (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "Sigma" "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "B" "holds" (Bool (Set "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k8_subset_1 :::"/\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "P" ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "P" ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" )))) ")" )); end; :: deftheorem defines :::"Indep"::: KOLMOG01:def 1 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_kolmog01 :::"Indep"::: ) "(" (Set (Var "B")) "," (Set (Var "P")) ")" )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k8_subset_1 :::"/\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" )))) ")" )) ")" )))))); theorem :: KOLMOG01:4 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "B")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "holds" (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_prob_1 :::"/\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" )))) ")" ) & (Bool (Set (Var "f")) "is" bbbadV1_PROB_2())) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "b")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "f")) ")" ) ")" ))))))))) ; theorem :: KOLMOG01:5 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma")) "holds" (Bool (Set ($#k1_kolmog01 :::"Indep"::: ) "(" (Set (Var "B")) "," (Set (Var "P")) ")" ) "is" ($#m1_dynkin :::"Dynkin_System"::: ) "of" (Set (Var "Omega"))))))) ; theorem :: KOLMOG01:6 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_kolmog01 :::"Indep"::: ) "(" (Set (Var "B")) "," (Set (Var "P")) ")" ))) "holds" (Bool (Set ($#k9_prob_1 :::"sigma"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_kolmog01 :::"Indep"::: ) "(" (Set (Var "B")) "," (Set (Var "P")) ")" ))))))) ; theorem :: KOLMOG01:7 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_kolmog01 :::"Indep"::: ) "(" (Set (Var "B")) "," (Set (Var "P")) ")" )) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_prob_1 :::"Event"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_prob_2 :::"are_independent_respect_to"::: ) (Set (Var "P")))) ")" ))))) ; theorem :: KOLMOG01:8 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_kolmog01 :::"Indep"::: ) "(" (Set (Var "B")) "," (Set (Var "P")) ")" ))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k1_kolmog01 :::"Indep"::: ) "(" (Set (Var "A")) "," (Set (Var "P")) ")" )))))) ; theorem :: KOLMOG01:9 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "A")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma"))) & (Bool (Set (Var "A")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) )) "holds" (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_kolmog01 :::"Indep"::: ) "(" (Set (Var "B")) "," (Set (Var "P")) ")" ))) "holds" (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "sB")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set ($#k9_prob_1 :::"sigma"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Var "sB")))) "holds" (Bool (Set ($#k9_prob_1 :::"sigma"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_kolmog01 :::"Indep"::: ) "(" (Set (Var "sB")) "," (Set (Var "P")) ")" ))))))))) ; theorem :: KOLMOG01:10 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "E")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma"))) & (Bool (Set (Var "E")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) ) & (Bool (Set (Var "F")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma"))) & (Bool (Set (Var "F")) "is" ($#v2_finsub_1 :::"intersection_stable"::: ) ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_prob_1 :::"Event"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_prob_2 :::"are_independent_respect_to"::: ) (Set (Var "P"))) ")" )) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_prob_1 :::"Event"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k9_prob_1 :::"sigma"::: ) (Set (Var "E")))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k9_prob_1 :::"sigma"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) ($#r1_prob_2 :::"are_independent_respect_to"::: ) (Set (Var "P")))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); mode :::"ManySortedSigmaField"::: "of" "I" "," "Sigma" -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "Sigma" ")" ) means :: KOLMOG01:def 2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k13_prob_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"SigmaField":::) "of" "Omega")); end; :: deftheorem defines :::"ManySortedSigmaField"::: KOLMOG01:def 2 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "Sigma")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b4")) ($#k13_prob_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")))) ")" ))))); definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); let "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set (Const "Sigma")); pred "A" :::"is_independent_wrt"::: "P" means :: KOLMOG01:def 3 (Bool "for" (Set (Var "e")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" "I" "st" (Bool (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set "(" (Set "(" "P" ($#k1_partfun1 :::"*"::: ) "A" ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "e")) ")" )) ($#r1_hidden :::"="::: ) (Set "P" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" "A" ($#k4_finseqop :::"*"::: ) (Set (Var "e")) ")" ) ")" ) ")" )))); end; :: deftheorem defines :::"is_independent_wrt"::: KOLMOG01:def 3 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_kolmog01 :::"is_independent_wrt"::: ) (Set (Var "P"))) "iff" (Bool "for" (Set (Var "e")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set "(" (Set "(" (Set (Var "P")) ($#k1_partfun1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "e")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "A")) ($#k4_finseqop :::"*"::: ) (Set (Var "e")) ")" ) ")" ) ")" )))) ")" )))))); definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "I" be ($#m1_hidden :::"set"::: ) ; let "J" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "I")); let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); mode :::"SigmaSection"::: "of" "J" "," "F" -> ($#m1_subset_1 :::"Function":::) "of" "J" "," "Sigma" means :: KOLMOG01:def 4 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "J")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set "F" ($#k13_prob_1 :::"."::: ) (Set (Var "i"))))); end; :: deftheorem defines :::"SigmaSection"::: KOLMOG01:def 4 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set (Var "b6")) "is" ($#m2_kolmog01 :::"SigmaSection"::: ) "of" (Set (Var "J")) "," (Set (Var "F"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "J")))) "holds" (Bool (Set (Set (Var "b6")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k13_prob_1 :::"."::: ) (Set (Var "i"))))) ")" ))))))); definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); let "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); pred "F" :::"is_independent_wrt"::: "P" means :: KOLMOG01:def 5 (Bool "for" (Set (Var "E")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "I" (Bool "for" (Set (Var "A")) "being" ($#m2_kolmog01 :::"SigmaSection"::: ) "of" (Set (Var "E")) "," "F" "holds" (Bool (Set (Var "A")) ($#r1_kolmog01 :::"is_independent_wrt"::: ) "P"))); end; :: deftheorem defines :::"is_independent_wrt"::: KOLMOG01:def 5 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_kolmog01 :::"is_independent_wrt"::: ) (Set (Var "P"))) "iff" (Bool "for" (Set (Var "E")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#m2_kolmog01 :::"SigmaSection"::: ) "of" (Set (Var "E")) "," (Set (Var "F")) "holds" (Bool (Set (Var "A")) ($#r1_kolmog01 :::"is_independent_wrt"::: ) (Set (Var "P"))))) ")" )))))); definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); let "J" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "I")); :: original: :::"|"::: redefine func "F" :::"|"::: "J" -> ($#m1_subset_1 :::"Function":::) "of" "J" "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "Sigma" ")" ); end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "J" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "I")); let "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "J")) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Const "Sigma")) ")" ); :: original: :::"Union"::: redefine func :::"Union"::: "F" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "Omega"; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); let "J" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "I")); func :::"sigUn"::: "(" "F" "," "J" ")" -> ($#m1_subset_1 :::"SigmaField":::) "of" "Omega" equals :: KOLMOG01:def 6 (Set ($#k9_prob_1 :::"sigma"::: ) (Set "(" ($#k3_kolmog01 :::"Union"::: ) (Set "(" "F" ($#k2_kolmog01 :::"|"::: ) "J" ")" ) ")" )); end; :: deftheorem defines :::"sigUn"::: KOLMOG01:def 6 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k4_kolmog01 :::"sigUn"::: ) "(" (Set (Var "F")) "," (Set (Var "J")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_prob_1 :::"sigma"::: ) (Set "(" ($#k3_kolmog01 :::"Union"::: ) (Set "(" (Set (Var "F")) ($#k2_kolmog01 :::"|"::: ) (Set (Var "J")) ")" ) ")" )))))))); definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); func :::"futSigmaFields"::: "(" "F" "," "I" ")" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) "Omega" ")" ) means :: KOLMOG01:def 7 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "Omega" "holds" (Bool "(" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "E")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "I" "st" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k4_kolmog01 :::"sigUn"::: ) "(" "F" "," (Set "(" "I" ($#k6_subset_1 :::"\"::: ) (Set (Var "E")) ")" ) ")" ))) ")" )); end; :: deftheorem defines :::"futSigmaFields"::: KOLMOG01:def 7 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "Omega")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_kolmog01 :::"futSigmaFields"::: ) "(" (Set (Var "F")) "," (Set (Var "I")) ")" )) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "ex" (Set (Var "E")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k4_kolmog01 :::"sigUn"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "I")) ($#k6_subset_1 :::"\"::: ) (Set (Var "E")) ")" ) ")" ))) ")" )) ")" )))))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); cluster (Set ($#k5_kolmog01 :::"futSigmaFields"::: ) "(" "F" "," "I" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); func :::"tailSigmaField"::: "(" "F" "," "I" ")" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "Omega" equals :: KOLMOG01:def 8 (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k5_kolmog01 :::"futSigmaFields"::: ) "(" "F" "," "I" ")" ")" )); end; :: deftheorem defines :::"tailSigmaField"::: KOLMOG01:def 8 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) "holds" (Bool (Set ($#k6_kolmog01 :::"tailSigmaField"::: ) "(" (Set (Var "F")) "," (Set (Var "I")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k5_kolmog01 :::"futSigmaFields"::: ) "(" (Set (Var "F")) "," (Set (Var "I")) ")" ")" ))))))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); cluster (Set ($#k6_kolmog01 :::"tailSigmaField"::: ) "(" "F" "," "I" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "J" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "I")); let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); func :::"MeetSections"::: "(" "J" "," "F" ")" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "Omega" means :: KOLMOG01:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Omega" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "I"(Bool "ex" (Set (Var "f")) "being" ($#m2_kolmog01 :::"SigmaSection"::: ) "of" (Set (Var "E")) "," "F" "st" (Bool "(" (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) "J") & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" ))) ")" ))) ")" )); end; :: deftheorem defines :::"MeetSections"::: KOLMOG01:def 9 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k7_kolmog01 :::"MeetSections"::: ) "(" (Set (Var "J")) "," (Set (Var "F")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b6"))) "iff" (Bool "ex" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I"))(Bool "ex" (Set (Var "f")) "being" ($#m2_kolmog01 :::"SigmaSection"::: ) "of" (Set (Var "E")) "," (Set (Var "F")) "st" (Bool "(" (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" ))) ")" ))) ")" )) ")" ))))))); theorem :: KOLMOG01:11 (Bool "for" (Set (Var "Omega")) "," (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k9_prob_1 :::"sigma"::: ) (Set "(" ($#k7_kolmog01 :::"MeetSections"::: ) "(" (Set (Var "J")) "," (Set (Var "F")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_kolmog01 :::"sigUn"::: ) "(" (Set (Var "F")) "," (Set (Var "J")) ")" )))))) ; theorem :: KOLMOG01:12 (Bool "for" (Set (Var "I")) "," (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) (Bool "for" (Set (Var "J")) "," (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "F")) ($#r2_kolmog01 :::"is_independent_wrt"::: ) (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r1_subset_1 :::"misses"::: ) (Set (Var "K")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k7_kolmog01 :::"MeetSections"::: ) "(" (Set (Var "J")) "," (Set (Var "F")) ")" )) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k7_kolmog01 :::"MeetSections"::: ) "(" (Set (Var "K")) "," (Set (Var "F")) ")" ))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k3_finsub_1 :::"/\"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))))))))) ; theorem :: KOLMOG01:13 (Bool "for" (Set (Var "Omega")) "," (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k7_kolmog01 :::"MeetSections"::: ) "(" (Set (Var "J")) "," (Set (Var "F")) ")" ) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Sigma"))))))) ; registrationlet "I", "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); let "J" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "I")); cluster (Set ($#k7_kolmog01 :::"MeetSections"::: ) "(" "J" "," "F" ")" ) -> ($#v2_finsub_1 :::"intersection_stable"::: ) ; end; theorem :: KOLMOG01:14 (Bool "for" (Set (Var "I")) "," (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) (Bool "for" (Set (Var "J")) "," (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "F")) ($#r2_kolmog01 :::"is_independent_wrt"::: ) (Set (Var "P"))) & (Bool (Set (Var "J")) ($#r1_subset_1 :::"misses"::: ) (Set (Var "K")))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_prob_1 :::"Event"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k4_kolmog01 :::"sigUn"::: ) "(" (Set (Var "F")) "," (Set (Var "J")) ")" )) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k4_kolmog01 :::"sigUn"::: ) "(" (Set (Var "F")) "," (Set (Var "K")) ")" ))) "holds" (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "u")) ($#k5_prob_1 :::"/\"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "u")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ))))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "F" be ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Const "I")) "," (Set (Const "Sigma")); func :::"finSigmaFields"::: "(" "F" "," "I" ")" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "Omega" means :: KOLMOG01:def 10 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Omega" "holds" (Bool "(" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "E")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "I" "st" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k4_kolmog01 :::"sigUn"::: ) "(" "F" "," (Set (Var "E")) ")" ))) ")" )); end; :: deftheorem defines :::"finSigmaFields"::: KOLMOG01:def 10 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_kolmog01 :::"finSigmaFields"::: ) "(" (Set (Var "F")) "," (Set (Var "I")) ")" )) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "ex" (Set (Var "E")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k4_kolmog01 :::"sigUn"::: ) "(" (Set (Var "F")) "," (Set (Var "E")) ")" ))) ")" )) ")" )))))); theorem :: KOLMOG01:15 (Bool "for" (Set (Var "I")) "," (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) "holds" (Bool (Set ($#k6_kolmog01 :::"tailSigmaField"::: ) "(" (Set (Var "F")) "," (Set (Var "I")) ")" ) "is" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")))))) ; theorem :: KOLMOG01:16 (Bool "for" (Set (Var "Omega")) "," (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "F")) "being" ($#m1_kolmog01 :::"ManySortedSigmaField"::: ) "of" (Set (Var "I")) "," (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "F")) ($#r2_kolmog01 :::"is_independent_wrt"::: ) (Set (Var "P"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k6_kolmog01 :::"tailSigmaField"::: ) "(" (Set (Var "F")) "," (Set (Var "I")) ")" )) & (Bool (Bool "not" (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Num 1))))))) ;