:: BOR_CANT semantic presentation begin definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "x", "y" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"IFGT"::: redefine func :::"IFGT"::: "(" "x" "," "y" "," "a" "," "b" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; theorem :: BOR_CANT:1 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "k")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: BOR_CANT:2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Num 1) ($#k7_real_1 :::"+"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) ; definitionlet "s" be ($#m1_subset_1 :::"Real_Sequence":::); func :::"JSum"::: "s" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: BOR_CANT:def 1 (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set (Var "d")) ")" ) ")" ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" )))); end; :: deftheorem defines :::"JSum"::: BOR_CANT:def 1 : (Bool "for" (Set (Var "s")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_bor_cant :::"JSum"::: ) (Set (Var "s")))) "iff" (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")) ")" ) ")" ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" )))) ")" )); theorem :: BOR_CANT: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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" ($#k2_bor_cant :::"JSum"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ")" )))))))) ; theorem :: BOR_CANT: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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" ($#k2_bor_cant :::"JSum"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))))))) ; definitionlet "n1", "n2" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Special_Function"::: "(" "n1" "," "n2" ")" -> ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: BOR_CANT:def 2 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_bor_cant :::"IFGT"::: ) "(" (Set (Var "n")) "," "n1" "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) "n2" ")" ) "," (Set (Var "n")) ")" ))); end; :: deftheorem defines :::"Special_Function"::: BOR_CANT:def 2 : (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_bor_cant :::"Special_Function"::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_bor_cant :::"IFGT"::: ) "(" (Set (Var "n")) "," (Set (Var "n1")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n2")) ")" ) "," (Set (Var "n")) ")" ))) ")" ))); definitionlet "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Special_Function2"::: "k" -> ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: BOR_CANT:def 3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) "k"))); end; :: deftheorem defines :::"Special_Function2"::: BOR_CANT:def 3 : (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_bor_cant :::"Special_Function2"::: ) (Set (Var "k")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))))) ")" ))); definitionlet "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Special_Function3"::: "k" -> ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: BOR_CANT:def 4 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_bor_cant :::"IFGT"::: ) "(" (Set (Var "n")) "," "k" "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ))); end; :: deftheorem defines :::"Special_Function3"::: BOR_CANT:def 4 : (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_bor_cant :::"Special_Function3"::: ) (Set (Var "k")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_bor_cant :::"IFGT"::: ) "(" (Set (Var "n")) "," (Set (Var "k")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ))) ")" ))); definitionlet "n1", "n2" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Special_Function4"::: "(" "n1" "," "n2" ")" -> ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: BOR_CANT:def 5 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_bor_cant :::"IFGT"::: ) "(" (Set (Var "n")) "," (Set "(" "n1" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) "n2" ")" ) "," (Set (Var "n")) ")" ))); end; :: deftheorem defines :::"Special_Function4"::: BOR_CANT:def 5 : (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_bor_cant :::"Special_Function4"::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_bor_cant :::"IFGT"::: ) "(" (Set (Var "n")) "," (Set "(" (Set (Var "n1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n2")) ")" ) "," (Set (Var "n")) ")" ))) ")" ))); registrationlet "n1", "n2" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k3_bor_cant :::"Special_Function"::: ) "(" "n1" "," "n2" ")" ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set ($#k6_bor_cant :::"Special_Function4"::: ) "(" "n1" "," "n2" ")" ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k4_bor_cant :::"Special_Function2"::: ) "n") -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; registrationlet "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 "s" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Sigma")); cluster (Set "A" ($#k9_nat_1 :::"^\"::: ) "s") -> "Sigma" ($#v5_relat_1 :::"-valued"::: ) ; end; theorem :: BOR_CANT: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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n")) "," (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n1"))) & (Bool (Set (Var "B")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "A")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k3_bor_cant :::"Special_Function"::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k1_valued_0 :::"^\"::: ) (Set "(" (Set "(" (Set (Var "n1")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k9_real_1 :::"-"::: ) (Set (Var "n1")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n1"))) & (Bool (Set (Var "C")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "A")) ($#k1_partfun1 :::"*"::: ) (Set (Var "e")))) & (Bool (Set (Var "B")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "C")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k3_bor_cant :::"Special_Function"::: ) "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "B")) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "C")) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n1")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set "(" (Set (Var "C")) ($#k1_valued_0 :::"^\"::: ) (Set "(" (Set "(" (Set (Var "n1")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k9_real_1 :::"-"::: ) (Set (Var "n1")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" )))) ")" ) ")" ))))) ; 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 "Prob" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); let "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Sigma")); pred "A" :::"is_all_independent_wrt"::: "Prob" means :: BOR_CANT:def 6 (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" "Sigma" "st" (Bool (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "A" ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "e")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_prob_2 :::"."::: ) (Set (Var "n")))) ")" ) ")" ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" "Prob" ($#k8_prob_1 :::"*"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "Prob" ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "B")) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" ))))); end; :: deftheorem defines :::"is_all_independent_wrt"::: BOR_CANT:def 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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_bor_cant :::"is_all_independent_wrt"::: ) (Set (Var "Prob"))) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "A")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "e")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_prob_2 :::"."::: ) (Set (Var "n")))) ")" ) ")" ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "B")) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" ))))) ")" ))))); theorem :: BOR_CANT: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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n")) "," (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n1"))) & (Bool (Set (Var "A")) ($#r1_bor_cant :::"is_all_independent_wrt"::: ) (Set (Var "Prob")))) "holds" (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n1")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set "(" (Set (Var "A")) ($#k1_valued_0 :::"^\"::: ) (Set "(" (Set "(" (Set (Var "n1")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k9_real_1 :::"-"::: ) (Set (Var "n1")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k1_valued_0 :::"^\"::: ) (Set "(" (Set "(" (Set (Var "n1")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k9_real_1 :::"-"::: ) (Set (Var "n1")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" )))))))) ; theorem :: BOR_CANT: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 "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A")) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_subset_1 :::"`"::: ) )))))) ; theorem :: BOR_CANT: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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A")) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" ) ")" )))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); func :::"Union_Shift_Seq"::: "A" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: BOR_CANT:def 7 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" "A" ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"Union_Shift_Seq"::: BOR_CANT:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_bor_cant :::"Union_Shift_Seq"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" )))) ")" ))); registrationlet "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 "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Sigma")); cluster (Set ($#k7_bor_cant :::"Union_Shift_Seq"::: ) "A") -> "Sigma" ($#v5_relat_1 :::"-valued"::: ) ; 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 "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Sigma")); func :::"@lim_sup"::: "A" -> ($#m1_prob_1 :::"Event"::: ) "of" "Sigma" equals :: BOR_CANT:def 8 (Set ($#k2_prob_2 :::"@Intersection"::: ) (Set "(" ($#k7_bor_cant :::"Union_Shift_Seq"::: ) "A" ")" )); end; :: deftheorem defines :::"@lim_sup"::: BOR_CANT:def 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 "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "holds" (Bool (Set ($#k8_bor_cant :::"@lim_sup"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_prob_2 :::"@Intersection"::: ) (Set "(" ($#k7_bor_cant :::"Union_Shift_Seq"::: ) (Set (Var "A")) ")" )))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); func :::"Intersect_Shift_Seq"::: "A" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: BOR_CANT:def 9 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" "A" ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"Intersect_Shift_Seq"::: BOR_CANT:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" (Set (Var "A")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" )))) ")" ))); registrationlet "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 "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Sigma")); cluster (Set ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) "A") -> "Sigma" ($#v5_relat_1 :::"-valued"::: ) ; 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 "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Sigma")); func :::"@lim_inf"::: "A" -> ($#m1_prob_1 :::"Event"::: ) "of" "Sigma" equals :: BOR_CANT:def 10 (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) "A" ")" )); end; :: deftheorem defines :::"@lim_inf"::: BOR_CANT:def 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 "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "holds" (Bool (Set ($#k10_bor_cant :::"@lim_inf"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) (Set (Var "A")) ")" )))))); theorem :: BOR_CANT: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 "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_bor_cant :::"Union_Shift_Seq"::: ) (Set (Var "A")) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_subset_1 :::"`"::: ) )))))) ; theorem :: BOR_CANT: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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_bor_cant :::"is_all_independent_wrt"::: ) (Set (Var "Prob")))) "holds" (Bool (Set (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))))))) ; theorem :: BOR_CANT:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A"))) ($#r2_funct_2 :::"="::: ) (Set ($#k7_bor_cant :::"Union_Shift_Seq"::: ) (Set (Var "A")))) & (Bool (Set ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A"))) ($#r2_funct_2 :::"="::: ) (Set ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) (Set (Var "A")))) ")" ))) ; theorem :: BOR_CANT:12 (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 "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set ($#k6_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A"))) ($#r2_funct_2 :::"="::: ) (Set ($#k7_bor_cant :::"Union_Shift_Seq"::: ) (Set (Var "A")))) & (Bool (Set ($#k5_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A"))) ($#r2_funct_2 :::"="::: ) (Set ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) (Set (Var "A")))) ")" )))) ; 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 "Prob" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); let "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Sigma")); func :::"Sum_Shift_Seq"::: "(" "Prob" "," "A" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: BOR_CANT:def 11 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" "Prob" ($#k8_prob_1 :::"*"::: ) (Set "(" "A" ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" ) ")" )))); end; :: deftheorem defines :::"Sum_Shift_Seq"::: BOR_CANT:def 11 : (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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k11_bor_cant :::"Sum_Shift_Seq"::: ) "(" (Set (Var "Prob")) "," (Set (Var "A")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" ) ")" )))) ")" )))))); theorem :: BOR_CANT:13 (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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k8_bor_cant :::"@lim_sup"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k11_bor_cant :::"Sum_Shift_Seq"::: ) "(" (Set (Var "Prob")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k11_bor_cant :::"Sum_Shift_Seq"::: ) "(" (Set (Var "Prob")) "," (Set (Var "A")) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" ))))) ; theorem :: BOR_CANT:14 (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")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "A")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")))) ")" )) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" ($#k7_bor_cant :::"Union_Shift_Seq"::: ) (Set (Var "A")) ")" ))) "iff" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")))) ")" ))) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_prob_2 :::"@Intersection"::: ) (Set "(" ($#k7_bor_cant :::"Union_Shift_Seq"::: ) (Set (Var "A")) ")" ))) "iff" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_prob_2 :::"."::: ) (Set (Var "n")))) ")" ))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) (Set (Var "A")) ")" ))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")))))) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) (Set (Var "A")) ")" ))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_prob_2 :::"."::: ) (Set (Var "k")))))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n")))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_prob_2 :::"."::: ) (Set (Var "k"))))))) ")" )) ")" ) ")" ))) ; theorem :: BOR_CANT:15 (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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_bor_cant :::"@lim_sup"::: ) (Set (Var "A")))) & (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k10_bor_cant :::"@lim_inf"::: ) (Set (Var "A")))) & (Bool (Set ($#k10_bor_cant :::"@lim_inf"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_bor_cant :::"@lim_sup"::: ) (Set (Var "A")) ")" ) ($#k3_subset_1 :::"`"::: ) )) & (Bool (Set (Set "(" (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k10_bor_cant :::"@lim_inf"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k8_bor_cant :::"@lim_sup"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))))) ; theorem :: BOR_CANT:16 (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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "implies" (Bool "(" (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" & "(" (Bool (Bool (Set (Var "A")) ($#r1_bor_cant :::"is_all_independent_wrt"::: ) (Set (Var "Prob"))) & (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" )) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) "implies" (Bool "(" (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ")" ))))) ; theorem :: BOR_CANT:17 (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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Bool "not" (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) )) & (Bool (Set (Var "A")) ($#r1_bor_cant :::"is_all_independent_wrt"::: ) (Set (Var "Prob")))) "holds" (Bool "(" (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))))) ; theorem :: BOR_CANT:18 (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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "A")) ($#r1_bor_cant :::"is_all_independent_wrt"::: ) (Set (Var "Prob")))) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool "(" (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Set (Var "Prob")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ))))) ; theorem :: BOR_CANT:19 (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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n1")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k1_valued_0 :::"^\"::: ) (Set "(" (Set (Var "n1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "n1")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n1")) ")" )))))))) ; theorem :: BOR_CANT:20 (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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k9_bor_cant :::"Intersect_Shift_Seq"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k7_bor_cant :::"Union_Shift_Seq"::: ) (Set (Var "A")) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" ) ")" )))))))) ; theorem :: BOR_CANT:21 (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 "Prob")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A"))) ($#r1_bor_cant :::"is_all_independent_wrt"::: ) (Set (Var "Prob")))) "implies" (Bool (Set (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "A")) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set (Var "A")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")))) ")" & "(" (Bool (Bool (Set (Var "A")) ($#r1_bor_cant :::"is_all_independent_wrt"::: ) (Set (Var "Prob")))) "implies" (Bool (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "Prob")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A")) ")" ) ($#k1_prob_2 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set "(" (Set (Var "Prob")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")))) ")" ")" )))))) ;