:: MEASURE8 semantic presentation begin theorem :: MEASURE8:1 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool (Set ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "seq"))))) ; theorem :: MEASURE8:2 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_mesfunc9 :::"summable"::: ) ) & (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc9 :::"Sum"::: ) (Set (Var "seq")))) ")" )) ; theorem :: MEASURE8:3 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xxreal_3 :::"+"::: ) (Set "(" (Set (Var "seq2")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "seq1")) ")" ) ($#k1_xxreal_3 :::"+"::: ) (Set "(" ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "seq2")) ")" ))) & (Bool (Set ($#k3_mesfunc9 :::"Sum"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_mesfunc9 :::"Sum"::: ) (Set (Var "seq1")) ")" ) ($#k1_xxreal_3 :::"+"::: ) (Set "(" ($#k3_mesfunc9 :::"Sum"::: ) (Set (Var "seq2")) ")" ))) ")" )) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "F" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_prob_2 :::"disjoint_valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," "F" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); mode :::"FinSequence"::: "of" "F" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) "X") means :: MEASURE8:def 1 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k4_prob_3 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) "F")); end; :: deftheorem defines :::"FinSequence"::: MEASURE8:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_measure8 :::"FinSequence"::: ) "of" (Set (Var "F"))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k4_prob_3 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) "X") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_prob_2 :::"disjoint_valued"::: ) for ($#m1_measure8 :::"FinSequence"::: ) "of" "F"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); mode Sep_FinSequence of "F" is ($#v1_prob_2 :::"disjoint_valued"::: ) ($#m1_measure8 :::"FinSequence"::: ) "of" "F"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); mode Sep_Sequence of "F" is ($#v1_prob_2 :::"disjoint_valued"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "F"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); mode :::"Set_Sequence"::: "of" "F" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: MEASURE8:def 2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) "F")); end; :: deftheorem defines :::"Set_Sequence"::: MEASURE8:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" )))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); mode :::"Covering"::: "of" "A" "," "F" -> ($#m2_measure8 :::"Set_Sequence"::: ) "of" "F" means :: MEASURE8:def 3 (Bool "A" ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) it ")" ))); end; :: deftheorem defines :::"Covering"::: MEASURE8:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m3_measure8 :::"Covering"::: ) "of" (Set (Var "A")) "," (Set (Var "F"))) "iff" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "b4")) ")" ))) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "FSets" be ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Const "F")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "FSets" :::"."::: "n" -> ($#m2_subset_1 :::"Element"::: ) "of" "F"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "Sets" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); mode :::"Covering"::: "of" "Sets" "," "F" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ")" ")" ) means :: MEASURE8:def 4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#m3_measure8 :::"Covering"::: ) "of" (Set "Sets" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "," "F")); end; :: deftheorem defines :::"Covering"::: MEASURE8:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Sets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m4_measure8 :::"Covering"::: ) "of" (Set (Var "Sets")) "," (Set (Var "F"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#m3_measure8 :::"Covering"::: ) "of" (Set (Set (Var "Sets")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "," (Set (Var "F")))) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"Measure":::) "of" (Set (Const "F")); let "FSets" be ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Const "F")); func :::"vol"::: "(" "M" "," "FSets" ")" -> ($#m1_subset_1 :::"ExtREAL_sequence":::) means :: MEASURE8:def 5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "M" ($#k1_mesfunc9 :::"."::: ) (Set "(" "FSets" ($#k1_measure8 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"vol"::: MEASURE8:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "FSets")) "being" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_measure8 :::"vol"::: ) "(" (Set (Var "M")) "," (Set (Var "FSets")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set (Var "FSets")) ($#k1_measure8 :::"."::: ) (Set (Var "n")) ")" )))) ")" )))))); theorem :: MEASURE8:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "FSets")) "being" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")) "holds" (Bool (Set ($#k2_measure8 :::"vol"::: ) "(" (Set (Var "M")) "," (Set (Var "FSets")) ")" ) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "Sets" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); let "Cvr" be ($#m4_measure8 :::"Covering"::: ) "of" (Set (Const "Sets")) "," (Set (Const "F")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "Cvr" :::"."::: "n" -> ($#m3_measure8 :::"Covering"::: ) "of" (Set "Sets" ($#k8_nat_1 :::"."::: ) "n") "," "F"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "Sets" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"Measure":::) "of" (Set (Const "F")); let "Cvr" be ($#m4_measure8 :::"Covering"::: ) "of" (Set (Const "Sets")) "," (Set (Const "F")); func :::"Volume"::: "(" "M" "," "Cvr" ")" -> ($#m1_subset_1 :::"ExtREAL_sequence":::) means :: MEASURE8:def 6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" ($#k2_measure8 :::"vol"::: ) "(" "M" "," (Set "(" "Cvr" ($#k3_measure8 :::"."::: ) (Set (Var "n")) ")" ) ")" ")" )))); end; :: deftheorem defines :::"Volume"::: MEASURE8:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Sets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "Cvr")) "being" ($#m4_measure8 :::"Covering"::: ) "of" (Set (Var "Sets")) "," (Set (Var "F")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k4_measure8 :::"Volume"::: ) "(" (Set (Var "M")) "," (Set (Var "Cvr")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b6")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" ($#k2_measure8 :::"vol"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "Cvr")) ($#k3_measure8 :::"."::: ) (Set (Var "n")) ")" ) ")" ")" )))) ")" ))))))); theorem :: MEASURE8:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "Sets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Cvr")) "being" ($#m4_measure8 :::"Covering"::: ) "of" (Set (Var "Sets")) "," (Set (Var "F")) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_measure8 :::"Volume"::: ) "(" (Set (Var "M")) "," (Set (Var "Cvr")) ")" ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n")))))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"Measure":::) "of" (Set (Const "F")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func :::"Svc"::: "(" "M" "," "A" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MEASURE8:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "CA")) "being" ($#m3_measure8 :::"Covering"::: ) "of" "A" "," "F" "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" ($#k2_measure8 :::"vol"::: ) "(" "M" "," (Set (Var "CA")) ")" ")" )))) ")" )); end; :: deftheorem defines :::"Svc"::: MEASURE8:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_measure8 :::"Svc"::: ) "(" (Set (Var "M")) "," (Set (Var "A")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "ex" (Set (Var "CA")) "being" ($#m3_measure8 :::"Covering"::: ) "of" (Set (Var "A")) "," (Set (Var "F")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" ($#k2_measure8 :::"vol"::: ) "(" (Set (Var "M")) "," (Set (Var "CA")) ")" ")" )))) ")" )) ")" )))))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"Measure":::) "of" (Set (Const "F")); cluster (Set ($#k5_measure8 :::"Svc"::: ) "(" "M" "," "A" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"Measure":::) "of" (Set (Const "F")); func :::"C_Meas"::: "M" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MEASURE8:def 8 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "holds" (Bool (Set it ($#k1_mesfunc9 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k5_measure8 :::"Svc"::: ) "(" "M" "," (Set (Var "A")) ")" ")" )))); end; :: deftheorem defines :::"C_Meas"::: MEASURE8:def 8 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_measure8 :::"C_Meas"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k5_measure8 :::"Svc"::: ) "(" (Set (Var "M")) "," (Set (Var "A")) ")" ")" )))) ")" ))))); definitionfunc :::"InvPairFunc"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: MEASURE8:def 9 (Set (Set ($#k1_nagata_2 :::"PairFunc"::: ) ) ($#k2_funct_1 :::"""::: ) ); end; :: deftheorem defines :::"InvPairFunc"::: MEASURE8:def 9 : (Bool (Set ($#k7_measure8 :::"InvPairFunc"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_nagata_2 :::"PairFunc"::: ) ) ($#k2_funct_1 :::"""::: ) )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "Sets" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); let "Cvr" be ($#m4_measure8 :::"Covering"::: ) "of" (Set (Const "Sets")) "," (Set (Const "F")); func :::"On"::: "Cvr" -> ($#m3_measure8 :::"Covering"::: ) "of" (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "Sets" ")" )) "," "F" means :: MEASURE8:def 10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_measure8 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "Cvr" ($#k3_measure8 :::"."::: ) (Set "(" (Set "(" ($#k4_funct_2 :::"pr1"::: ) (Set ($#k7_measure8 :::"InvPairFunc"::: ) ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_measure8 :::"."::: ) (Set "(" (Set "(" ($#k5_funct_2 :::"pr2"::: ) (Set ($#k7_measure8 :::"InvPairFunc"::: ) ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"On"::: MEASURE8:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Sets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cvr")) "being" ($#m4_measure8 :::"Covering"::: ) "of" (Set (Var "Sets")) "," (Set (Var "F")) (Bool "for" (Set (Var "b5")) "being" ($#m3_measure8 :::"Covering"::: ) "of" (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "Sets")) ")" )) "," (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_measure8 :::"On"::: ) (Set (Var "Cvr")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k1_measure8 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Cvr")) ($#k3_measure8 :::"."::: ) (Set "(" (Set "(" ($#k4_funct_2 :::"pr1"::: ) (Set ($#k7_measure8 :::"InvPairFunc"::: ) ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_measure8 :::"."::: ) (Set "(" (Set "(" ($#k5_funct_2 :::"pr2"::: ) (Set ($#k7_measure8 :::"InvPairFunc"::: ) ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" )))))); theorem :: MEASURE8:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "Sets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cvr")) "being" ($#m4_measure8 :::"Covering"::: ) "of" (Set (Var "Sets")) "," (Set (Var "F")) "holds" (Bool (Set (Set "(" ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" ($#k2_measure8 :::"vol"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k8_measure8 :::"On"::: ) (Set (Var "Cvr")) ")" ) ")" ")" ) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" ($#k4_measure8 :::"Volume"::: ) "(" (Set (Var "M")) "," (Set (Var "Cvr")) ")" ")" ) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "m"))))))))))) ; theorem :: MEASURE8:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "Sets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cvr")) "being" ($#m4_measure8 :::"Covering"::: ) "of" (Set (Var "Sets")) "," (Set (Var "F")) "holds" (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k5_measure8 :::"Svc"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "Sets")) ")" ) ")" ) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" ($#k4_measure8 :::"Volume"::: ) "(" (Set (Var "M")) "," (Set (Var "Cvr")) ")" ")" )))))))) ; theorem :: MEASURE8:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set "(" (Set (Var "A")) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "X")) ")" ) ")" ($#k14_funct_7 :::"followed_by"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set (Var "X")) ")" )) "is" ($#m3_measure8 :::"Covering"::: ) "of" (Set (Var "A")) "," (Set (Var "F")))))) ; theorem :: MEASURE8:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set "(" ($#k6_measure8 :::"C_Meas"::: ) (Set (Var "M")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "A")))))))) ; theorem :: MEASURE8:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) "holds" (Bool (Set ($#k6_measure8 :::"C_Meas"::: ) (Set (Var "M"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )))) ; theorem :: MEASURE8:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set "(" ($#k6_measure8 :::"C_Meas"::: ) (Set (Var "M")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: MEASURE8:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set "(" ($#k6_measure8 :::"C_Meas"::: ) (Set (Var "M")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k6_measure8 :::"C_Meas"::: ) (Set (Var "M")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "B")))))))) ; theorem :: MEASURE8:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "Sets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k6_measure8 :::"C_Meas"::: ) (Set (Var "M")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "Sets")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" (Set "(" ($#k6_measure8 :::"C_Meas"::: ) (Set (Var "M")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "Sets")) ")" ))))))) ; theorem :: MEASURE8:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) "holds" (Bool (Set ($#k6_measure8 :::"C_Meas"::: ) (Set (Var "M"))) "is" ($#m1_measure4 :::"C_Measure"::: ) "of" (Set (Var "X")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"Measure":::) "of" (Set (Const "F")); :: original: :::"C_Meas"::: redefine func :::"C_Meas"::: "M" -> ($#m1_measure4 :::"C_Measure"::: ) "of" "X"; end; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"Measure":::) "of" (Set (Const "F")); attr "M" is :::"completely-additive"::: means :: MEASURE8:def 11 (Bool "for" (Set (Var "FSets")) "being" ($#m1_subset_1 :::"Sep_Sequence":::) "of" "F" "st" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "FSets")) ")" )) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" "M" ($#k1_partfun1 :::"*"::: ) (Set (Var "FSets")) ")" )) ($#r1_hidden :::"="::: ) (Set "M" ($#k1_mesfunc9 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "FSets")) ")" ) ")" )))); end; :: deftheorem defines :::"completely-additive"::: MEASURE8:def 11 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_measure8 :::"completely-additive"::: ) ) "iff" (Bool "for" (Set (Var "FSets")) "being" ($#m1_subset_1 :::"Sep_Sequence":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "FSets")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "FSets")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "FSets")) ")" ) ")" )))) ")" )))); theorem :: MEASURE8:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "FSets")) "being" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")) "holds" (Bool (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "FSets"))) "is" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")))))) ; theorem :: MEASURE8:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "FSets")) "being" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")) "holds" (Bool (Set ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "FSets"))) "is" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")))))) ; theorem :: MEASURE8:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "CA")) "being" ($#m3_measure8 :::"Covering"::: ) "of" (Set (Var "A")) "," (Set (Var "F")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "FSets")) "being" ($#m1_subset_1 :::"Sep_Sequence":::) "of" (Set (Var "F")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "FSets")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "FSets")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "CA")) ($#k1_measure8 :::"."::: ) (Set (Var "n")))) ")" ) ")" )))))) ; theorem :: MEASURE8:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_measure8 :::"completely-additive"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_measure8 :::"C_Meas"::: ) (Set (Var "M")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "A")))))))) ; theorem :: MEASURE8:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "C")) "being" ($#m1_measure4 :::"C_Measure"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "C")) ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_xxreal_3 :::"+"::: ) (Set "(" (Set (Var "C")) ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A")) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "C")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "B")))) ")" )) "holds" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k1_measure4 :::"sigma_Field"::: ) (Set (Var "C"))))))) ; theorem :: MEASURE8:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) "holds" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set ($#k1_measure4 :::"sigma_Field"::: ) (Set "(" ($#k9_measure8 :::"C_Meas"::: ) (Set (Var "M")) ")" )))))) ; theorem :: MEASURE8:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "FSets")) "being" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "F")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "FSets"))) "is" ($#m1_subset_1 :::"ExtREAL_sequence":::)))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "FSets" be ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Const "F")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "F")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"*"::: redefine func "g" :::"*"::: "FSets" -> ($#m1_subset_1 :::"ExtREAL_sequence":::); end; theorem :: MEASURE8:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "SSets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "SSets"))) "is" ($#m1_subset_1 :::"ExtREAL_sequence":::)))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "SSets" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "S")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"*"::: redefine func "g" :::"*"::: "SSets" -> ($#m1_subset_1 :::"ExtREAL_sequence":::); end; theorem :: MEASURE8:23 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "m")))) ")" )) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "G")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n")))))) ; theorem :: MEASURE8:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_measure4 :::"C_Measure"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Sep_Sequence":::) "of" (Set "(" ($#k1_measure4 :::"sigma_Field"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k4_measure1 :::"rng"::: ) (Set (Var "seq")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_measure4 :::"sigma_Field"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "C")) ($#k1_mesfunc9 :::"."::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k4_measure1 :::"rng"::: ) (Set (Var "seq")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc9 :::"Sum"::: ) (Set "(" (Set (Var "C")) ($#k1_partfun1 :::"*"::: ) (Set (Var "seq")) ")" ))) ")" )))) ; theorem :: MEASURE8:25 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_measure4 :::"C_Measure"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set ($#k1_measure4 :::"sigma_Field"::: ) (Set (Var "C"))) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set (Var "seq"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_measure4 :::"sigma_Field"::: ) (Set (Var "C"))))))) ; theorem :: MEASURE8:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "SSets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "SSets")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "M")) ($#k11_measure8 :::"*"::: ) (Set (Var "SSets")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "SSets")) ")" ))))))) ; theorem :: MEASURE8:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "FSets")) "being" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "FSets")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool (Set (Set (Var "M")) ($#k10_measure8 :::"*"::: ) (Set (Var "FSets"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ))))) ; theorem :: MEASURE8:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "FSets")) "being" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "FSets")) "is" ($#v2_prob_1 :::"non-ascending"::: ) )) "holds" (Bool (Set (Set (Var "M")) ($#k10_measure8 :::"*"::: ) (Set (Var "FSets"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ))))) ; theorem :: MEASURE8:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "SSets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "SSets")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool (Set (Set (Var "M")) ($#k11_measure8 :::"*"::: ) (Set (Var "SSets"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ))))) ; theorem :: MEASURE8:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "SSets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "SSets")) "is" ($#v2_prob_1 :::"non-ascending"::: ) )) "holds" (Bool (Set (Set (Var "M")) ($#k11_measure8 :::"*"::: ) (Set (Var "SSets"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ))))) ; theorem :: MEASURE8:31 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "SSets")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "SSets")) "is" ($#v2_prob_1 :::"non-ascending"::: ) ) & (Bool (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set (Var "SSets")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) "holds" (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "M")) ($#k11_measure8 :::"*"::: ) (Set (Var "SSets")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "SSets")) ")" ))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "m" be ($#m1_subset_1 :::"Measure":::) "of" (Set (Const "F")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); pred "M" :::"is_extension_of"::: "m" means :: MEASURE8:def 12 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set "M" ($#k1_mesfunc9 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "m" ($#k1_mesfunc9 :::"."::: ) (Set (Var "A"))))); end; :: deftheorem defines :::"is_extension_of"::: MEASURE8:def 12 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_measure8 :::"is_extension_of"::: ) (Set (Var "m"))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "A"))))) ")" )))))); theorem :: MEASURE8:32 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) "st" (Bool (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set "(" ($#k9_prob_1 :::"sigma"::: ) (Set (Var "F")) ")" ) "st" (Bool (Set (Var "M")) ($#r1_measure8 :::"is_extension_of"::: ) (Set (Var "m"))))) "holds" (Bool (Set (Var "m")) "is" ($#v1_measure8 :::"completely-additive"::: ) )))) ; theorem :: MEASURE8:33 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "m")) "is" ($#v1_measure8 :::"completely-additive"::: ) )) "holds" (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set "(" ($#k9_prob_1 :::"sigma"::: ) (Set (Var "F")) ")" ) "st" (Bool "(" (Bool (Set (Var "M")) ($#r1_measure8 :::"is_extension_of"::: ) (Set (Var "m"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_measure4 :::"sigma_Meas"::: ) (Set "(" ($#k9_measure8 :::"C_Meas"::: ) (Set (Var "m")) ")" ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k9_prob_1 :::"sigma"::: ) (Set (Var "F")) ")" ))) ")" ))))) ; theorem :: MEASURE8:34 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "FSets")) "being" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set (Var "FSets")) ($#k1_measure8 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" )) "holds" (Bool (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "FSets")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))))))) ; theorem :: MEASURE8:35 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "m")) "is" ($#v1_measure8 :::"completely-additive"::: ) ) & (Bool "ex" (Set (Var "Aseq")) "being" ($#m2_measure8 :::"Set_Sequence"::: ) "of" (Set (Var "F")) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "m")) ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set (Var "Aseq")) ($#k1_measure8 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "Aseq")) ")" ))) ")" ))) "holds" (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set "(" ($#k9_prob_1 :::"sigma"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "M")) ($#r1_measure8 :::"is_extension_of"::: ) (Set (Var "m")))) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_measure4 :::"sigma_Meas"::: ) (Set "(" ($#k9_measure8 :::"C_Meas"::: ) (Set (Var "m")) ")" ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k9_prob_1 :::"sigma"::: ) (Set (Var "F")) ")" ))))))) ;