:: MEASURE3 semantic presentation begin theorem :: MEASURE3:1 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F1")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F2")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F2"))))) ; theorem :: MEASURE3:2 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F1")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F2")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F2"))))) ; notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); synonym :::"N_Sub_fam"::: "of" "S" for :::"N_Measure_fam"::: "of" "S"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Const "S")); :: original: :::"rng"::: redefine func :::"rng"::: "F" -> ($#m1_measure2 :::"N_Measure_fam"::: ) "of" "S"; end; theorem :: MEASURE3:3 (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )))))))) ; theorem :: MEASURE3:4 (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 "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) "holds" (Bool (Set ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )))))) ; theorem :: MEASURE3:5 (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 "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) "holds" (Bool (Set ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "G")) ")" ) ")" )))))) ; theorem :: MEASURE3:6 (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 "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "G")) ")" ) ")" ) ")" ))))))) ; theorem :: MEASURE3:7 (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 "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "G")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ) ")" ) ")" ))))))) ; theorem :: MEASURE3:8 (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 "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "G")) ")" ) ")" ) ")" ))))))) ; theorem :: MEASURE3:9 (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 "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) "is" ($#m1_subset_1 :::"Real":::)) & (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" ) ")" )) "is" ($#m1_subset_1 :::"Real":::)) & (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "G")) ")" ) ")" )) "is" ($#m1_subset_1 :::"Real":::)) ")" ))))) ; theorem :: MEASURE3:10 (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 "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) "holds" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "G")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" ) ")" ) ")" ))))))) ; theorem :: MEASURE3:11 (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 "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) "holds" (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "G")) ")" ) ")" ) ")" ))))))) ; theorem :: MEASURE3:12 (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" ) ")" ))))))) ; theorem :: MEASURE3:13 (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 :::"Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Sep_Sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ) ")" ))))))) ; theorem :: MEASURE3:14 (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 :::"Measure":::) "of" (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Sep_Sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" ))) ")" )) "holds" (Bool (Set (Var "M")) "is" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); pred "M" :::"is_complete"::: "S" means :: MEASURE3:def 1 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set "M" ($#k12_supinf_2 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))) "holds" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "S"))); end; :: deftheorem defines :::"is_complete"::: MEASURE3:def 1 : (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")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_measure3 :::"is_complete"::: ) (Set (Var "S"))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))) "holds" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))) ")" )))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); mode :::"thin"::: "of" "M" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: MEASURE3:def 2 (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "S") & (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set "M" ($#k12_supinf_2 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" )); end; :: deftheorem defines :::"thin"::: MEASURE3:def 2 : (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 "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_measure3 :::"thin"::: ) "of" (Set (Var "M"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "b4")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" )) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); func :::"COM"::: "(" "S" "," "M" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" "X" means :: MEASURE3:def 3 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "S") & (Bool "ex" (Set (Var "C")) "being" ($#m1_measure3 :::"thin"::: ) "of" "M" "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C"))))) ")" )) ")" )); end; :: deftheorem defines :::"COM"::: MEASURE3:def 3 : (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 "b4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_measure3 :::"COM"::: ) "(" (Set (Var "S")) "," (Set (Var "M")) ")" )) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool "ex" (Set (Var "C")) "being" ($#m1_measure3 :::"thin"::: ) "of" (Set (Var "M")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C"))))) ")" )) ")" )) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "A" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_measure3 :::"COM"::: ) "(" (Set (Const "S")) "," (Set (Const "M")) ")" ); func :::"MeasPart"::: "A" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" "X" means :: MEASURE3:def 4 (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) "A") & (Bool (Set "A" ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) "is" ($#m1_measure3 :::"thin"::: ) "of" "M") ")" ) ")" )); end; :: deftheorem defines :::"MeasPart"::: MEASURE3:def 4 : (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 "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_measure3 :::"COM"::: ) "(" (Set (Var "S")) "," (Set (Var "M")) ")" ) (Bool "for" (Set (Var "b5")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_measure3 :::"MeasPart"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) "is" ($#m1_measure3 :::"thin"::: ) "of" (Set (Var "M"))) ")" ) ")" )) ")" )))))); theorem :: MEASURE3:15 (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k2_measure3 :::"COM"::: ) "(" (Set (Var "S")) "," (Set (Var "M")) ")" ")" ) (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_measure3 :::"MeasPart"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))))))))) ; theorem :: MEASURE3:16 (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k2_measure3 :::"COM"::: ) "(" (Set (Var "S")) "," (Set (Var "M")) ")" ")" ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) (Bool "ex" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "H")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))))))))) ; theorem :: MEASURE3:17 (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_measure3 :::"thin"::: ) "of" (Set (Var "M"))) ")" )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ))))))) ; theorem :: MEASURE3:18 (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 "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool "ex" (Set (Var "C")) "being" ($#m1_measure3 :::"thin"::: ) "of" (Set (Var "M")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C"))))) ")" )) ")" ) ")" )) "holds" (Bool (Set (Var "D")) "is" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); cluster (Set ($#k2_measure3 :::"COM"::: ) "(" "S" "," "M" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_prob_1 :::"compl-closed"::: ) ($#v3_measure1 :::"sigma-additive"::: ) ; end; theorem :: MEASURE3:19 (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 "B1")) "," (Set (Var "B2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B1")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "B2")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_measure3 :::"thin"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "B1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B2")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C2"))))) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B2"))))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); func :::"COM"::: "M" -> ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set "(" ($#k2_measure3 :::"COM"::: ) "(" "S" "," "M" ")" ")" ) means :: MEASURE3:def 5 (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool "for" (Set (Var "C")) "being" ($#m1_measure3 :::"thin"::: ) "of" "M" "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set "M" ($#k12_supinf_2 :::"."::: ) (Set (Var "B")))))); end; :: deftheorem defines :::"COM"::: MEASURE3:def 5 : (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 "b4")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set "(" ($#k2_measure3 :::"COM"::: ) "(" (Set (Var "S")) "," (Set (Var "M")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_measure3 :::"COM"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "for" (Set (Var "C")) "being" ($#m1_measure3 :::"thin"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "b4")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B")))))) ")" ))))); theorem :: MEASURE3:20 (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")) "holds" (Bool (Set ($#k4_measure3 :::"COM"::: ) (Set (Var "M"))) ($#r1_measure3 :::"is_complete"::: ) (Set ($#k2_measure3 :::"COM"::: ) "(" (Set (Var "S")) "," (Set (Var "M")) ")" ))))) ;