:: MEASURE2 semantic presentation begin theorem :: MEASURE2: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")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "holds" (Bool (Set (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F"))) "is" bbbadV6_SUPINF_2()))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); mode :::"N_Measure_fam"::: "of" "S" -> ($#m1_subset_1 :::"N_Sub_set_fam":::) "of" "X" means :: MEASURE2:def 1 (Bool it ($#r1_tarski :::"c="::: ) "S"); end; :: deftheorem defines :::"N_Measure_fam"::: MEASURE2: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 "b3")) "being" ($#m1_subset_1 :::"N_Sub_set_fam":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Var "S"))) "iff" (Bool (Set (Var "b3")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) ")" )))); theorem :: MEASURE2: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 "T")) "being" ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "T" be ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Const "S")); :: original: :::"meet"::: redefine func :::"meet"::: "T" -> ($#m2_subset_1 :::"Element"::: ) "of" "S"; :: original: :::"union"::: redefine func :::"union"::: "T" -> ($#m2_subset_1 :::"Element"::: ) "of" "S"; end; theorem :: MEASURE2: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 "N")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ))))) ; theorem :: MEASURE2: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 "N")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_measure1 :::"\/"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ))))) ; theorem :: MEASURE2:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "N")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) "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 "r")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) ")" )) ")" )))))) ; theorem :: MEASURE2:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "N")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))))))) ; theorem :: MEASURE2:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "N")) "," (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 (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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 "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))))))) ; theorem :: MEASURE2: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 "N")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ))))) ; theorem :: MEASURE2: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 "N")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#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 (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ))))) ; theorem :: MEASURE2: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 "N")) "," (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 (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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 "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_measure1 :::"\/"::: ) (Set "(" (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))))))) ; theorem :: MEASURE2: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 "T")) "being" ($#m1_measure2 :::"N_Measure_fam"::: ) "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 (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set ($#k4_measure1 :::"rng"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "M")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_measure2 :::"union"::: ) (Set (Var "T")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" )))))))) ; theorem :: MEASURE2: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 "T")) "being" ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Var "S")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set ($#k4_measure1 :::"rng"::: ) (Set (Var "F")))))))) ; theorem :: MEASURE2:13 (Bool "for" (Set (Var "N")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "F")) ($#k1_funct_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 "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; theorem :: MEASURE2: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 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "T")) "being" ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "A")) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) ")" )) "holds" (Bool (Set ($#k2_measure2 :::"union"::: ) (Set (Var "T"))) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))))))) ; theorem :: MEASURE2: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 "T")) "being" ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Var "A")) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) ")" ))) "holds" (Bool (Set ($#k1_measure2 :::"meet"::: ) (Set (Var "T"))) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))))))) ; theorem :: MEASURE2: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 "T")) "being" ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "A")) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) ")" )) "holds" (Bool (Set ($#k1_measure2 :::"meet"::: ) (Set (Var "T"))) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "IT" be ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Const "S")); attr "IT" is :::"non-decreasing"::: means :: MEASURE2:def 2 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "S" "st" (Bool "(" (Bool "IT" ($#r1_hidden :::"="::: ) (Set ($#k4_measure1 :::"rng"::: ) (Set (Var "F")))) & (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"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"non-decreasing"::: MEASURE2: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 "IT")) "being" ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_measure2 :::"non-decreasing"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set ($#k4_measure1 :::"rng"::: ) (Set (Var "F")))) & (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"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" )) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV4_CARD_3() ($#v1_measure2 :::"non-decreasing"::: ) for ($#m1_measure2 :::"N_Measure_fam"::: ) "of" "S"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "IT" be ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Const "S")); attr "IT" is :::"non-increasing"::: means :: MEASURE2:def 3 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "S" "st" (Bool "(" (Bool "IT" ($#r1_hidden :::"="::: ) (Set ($#k4_measure1 :::"rng"::: ) (Set (Var "F")))) & (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")))) ")" ) ")" )); end; :: deftheorem defines :::"non-increasing"::: MEASURE2: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 "IT")) "being" ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_measure2 :::"non-increasing"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set ($#k4_measure1 :::"rng"::: ) (Set (Var "F")))) & (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")))) ")" ) ")" )) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV4_CARD_3() ($#v2_measure2 :::"non-increasing"::: ) for ($#m1_measure2 :::"N_Measure_fam"::: ) "of" "S"; end; theorem :: MEASURE2: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 "N")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "F")) ($#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 "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) "holds" (Bool (Set ($#k4_measure1 :::"rng"::: ) (Set (Var "F"))) "is" ($#v1_measure2 :::"non-decreasing"::: ) ($#m1_measure2 :::"N_Measure_fam"::: ) "of" (Set (Var "S")))))) ; theorem :: MEASURE2:18 (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "m")) "," (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")))) "holds" (Bool (Set (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))))) ; theorem :: MEASURE2:19 (Bool "for" (Set (Var "N")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))))) ; theorem :: MEASURE2: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 "N")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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 "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k4_measure1 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k4_measure1 :::"rng"::: ) (Set (Var "N")) ")" )))))) ; theorem :: MEASURE2:21 (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 "N")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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 "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#m1_subset_1 :::"Sep_Sequence":::) "of" (Set (Var "S")))))) ; theorem :: MEASURE2: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 "N")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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 "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_measure1 :::"\/"::: ) (Set "(" (Set (Var "N")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" )))) ; theorem :: MEASURE2:23 (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 (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k4_measure1 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" ) ")" ))))))) ;