:: MEASURE1 semantic presentation begin theorem :: MEASURE1:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_enumset1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: MEASURE1:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))))) ; theorem :: MEASURE1:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k1_enumset1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))))) ; scheme :: MEASURE1:sch 1 DomsetFamEx{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "B"))]) ")" ) ")" ))) provided (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "B"))]) ")" )) proof end; notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); synonym "X" :::"\"::: "S" for :::"COMPLEMENT"::: "S"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set "X" ($#k7_setfam_1 :::"\"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MEASURE1:4 (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")) "holds" (Bool "(" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "X")) ($#k7_setfam_1 :::"\"::: ) (Set (Var "S")) ")" ) ")" ))) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k6_setfam_1 :::"meet"::: ) (Set "(" (Set (Var "X")) ($#k7_setfam_1 :::"\"::: ) (Set (Var "S")) ")" ) ")" ))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); redefine attr "IT" is :::"compl-closed"::: means :: MEASURE1:def 1 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set "X" ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) "IT")); end; :: deftheorem defines :::"compl-closed"::: MEASURE1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_prob_1 :::"compl-closed"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_finsub_1 :::"cup-closed"::: ) ($#v1_prob_1 :::"compl-closed"::: ) -> ($#v2_finsub_1 :::"cap-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); cluster ($#v2_finsub_1 :::"cap-closed"::: ) ($#v1_prob_1 :::"compl-closed"::: ) -> ($#v1_finsub_1 :::"cup-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); end; theorem :: MEASURE1:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_setfam_1 :::"\"::: ) (Set (Var "S")))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v2_finsub_1 :::"cap-closed"::: ) ($#v1_prob_1 :::"compl-closed"::: ) -> ($#v3_finsub_1 :::"diff-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); end; theorem :: MEASURE1:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "S")))))) ; theorem :: MEASURE1:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"nonnegative"::: redefine attr "F" is :::"nonnegative"::: means :: MEASURE1:def 2 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set "F" ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))))); end; :: deftheorem defines :::"nonnegative"::: MEASURE1:def 2 : (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 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))))) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); attr "F" is :::"additive"::: means :: MEASURE1:def 3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "S" "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set "F" ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k12_supinf_2 :::"."::: ) (Set (Var "A")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" "F" ($#k12_supinf_2 :::"."::: ) (Set (Var "B")) ")" )))); end; :: deftheorem defines :::"additive"::: MEASURE1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_measure1 :::"additive"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B")) ")" )))) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); cluster ($#v1_relat_1 :::"Relation-like"::: ) "S" ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1("S") bbbadV1_FUNCT_2("S" "," (Set ($#k7_numbers :::"ExtREAL"::: ) )) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v10_valued_0 :::"zeroed"::: ) bbbadV6_SUPINF_2() ($#v2_measure1 :::"additive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "S" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); mode Measure of "S" is ($#v10_valued_0 :::"zeroed"::: ) bbbadV6_SUPINF_2() ($#v2_measure1 :::"additive"::: ) ($#m1_subset_1 :::"Function":::) "of" "S" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; theorem :: MEASURE1:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B")))))))) ; theorem :: MEASURE1:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "B")) ($#k2_finsub_1 :::"\"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")) ")" ))))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_finsub_1 :::"cap-closed"::: ) ($#v1_prob_1 :::"compl-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finsub_1 :::"cup-closed"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); let "A", "B" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Const "S")); :: original: :::"\/"::: redefine func "A" :::"\/"::: "B" -> ($#m2_subset_1 :::"Element"::: ) "of" "S"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "A", "B" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Const "S")); :: original: :::"/\"::: redefine func "A" :::"/\"::: "B" -> ($#m2_subset_1 :::"Element"::: ) "of" "S"; :: original: :::"\"::: redefine func "A" :::"\"::: "B" -> ($#m2_subset_1 :::"Element"::: ) "of" "S"; end; theorem :: MEASURE1:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k1_measure1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B")) ")" ))))))) ; theorem :: MEASURE1:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) ")" ) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"Measure":::) "of" (Set (Const "S")); mode :::"measure_zero"::: "of" "M" -> ($#m2_subset_1 :::"Element"::: ) "of" "S" means :: MEASURE1:def 4 (Bool (Set "M" ($#k12_supinf_2 :::"."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )); end; :: deftheorem defines :::"measure_zero"::: MEASURE1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) "iff" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ))))); theorem :: MEASURE1:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_measure1 :::"measure_zero"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_measure1 :::"measure_zero"::: ) "of" (Set (Var "M")))))))) ; theorem :: MEASURE1:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_measure1 :::"measure_zero"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k1_measure1 :::"\/"::: ) (Set (Var "B"))) "is" ($#m1_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) & (Bool (Set (Set (Var "A")) ($#k2_measure1 :::"/\"::: ) (Set (Var "B"))) "is" ($#m1_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) & (Bool (Set (Set (Var "A")) ($#k3_measure1 :::"\"::: ) (Set (Var "B"))) "is" ($#m1_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) ")" ))))) ; theorem :: MEASURE1:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_measure1 :::"measure_zero"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k1_measure1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k2_measure1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k3_measure1 :::"\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")))) ")" )))))) ; theorem :: MEASURE1:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "st" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: MEASURE1:16 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) "st" (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_hidden :::"="::: ) (Set (Var "A")))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV4_CARD_3() for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode N_Sub_set_fam of "X" is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV4_CARD_3() ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end; theorem :: MEASURE1:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "F")) ($#k1_prob_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_prob_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "C"))) ")" ) ")" )))) ; theorem :: MEASURE1:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_enumset1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"N_Sub_set_fam":::) "of" (Set (Var "X"))))) ; theorem :: MEASURE1:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_prob_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ) ")" )))) ; theorem :: MEASURE1:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"N_Sub_set_fam":::) "of" (Set (Var "X"))))) ; theorem :: MEASURE1:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"N_Sub_set_fam":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "X")) ($#k7_setfam_1 :::"\"::: ) (Set (Var "S"))) "is" ($#m1_subset_1 :::"N_Sub_set_fam":::) "of" (Set (Var "X"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "IT" is :::"sigma-additive"::: means :: MEASURE1:def 5 (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"N_Sub_set_fam":::) "of" "X" "st" (Bool (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) "IT")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "M"))) ($#r2_hidden :::"in"::: ) "IT")); end; :: deftheorem defines :::"sigma-additive"::: MEASURE1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_measure1 :::"sigma-additive"::: ) ) "iff" (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"N_Sub_set_fam":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "M"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_prob_1 :::"compl-closed"::: ) ($#v3_measure1 :::"sigma-additive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_prob_1 :::"compl-closed"::: ) ($#v4_prob_1 :::"sigma-multiplicative"::: ) -> ($#v3_measure1 :::"sigma-additive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); cluster ($#v1_prob_1 :::"compl-closed"::: ) ($#v3_measure1 :::"sigma-additive"::: ) -> ($#v4_prob_1 :::"sigma-multiplicative"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_prob_1 :::"compl-closed"::: ) ($#v4_prob_1 :::"sigma-multiplicative"::: ) -> for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); end; theorem :: MEASURE1:22 (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")) "holds" (Bool "(" (Bool "(" (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) & (Bool "(" "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"N_Sub_set_fam":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "M"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) ")" ) "iff" (Bool (Set (Var "S")) "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")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "S" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," "S") ($#v1_prob_2 :::"disjoint_valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," "S" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); mode Sep_Sequence of "S" is ($#v1_prob_2 :::"disjoint_valued"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "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" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end; theorem :: MEASURE1: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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "holds" (Bool (Set ($#k4_measure1 :::"rng"::: ) (Set (Var "F"))) "is" ($#m1_subset_1 :::"N_Sub_set_fam":::) "of" (Set (Var "X")))))) ; theorem :: MEASURE1:24 (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k4_measure1 :::"rng"::: ) (Set (Var "F")) ")" )) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")))))) ; theorem :: MEASURE1:25 (Bool "for" (Set (Var "Y")) "," (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "S")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) "is" bbbadV6_SUPINF_2())) "holds" (Bool (Set (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F"))) "is" bbbadV6_SUPINF_2())))) ; theorem :: MEASURE1:26 (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 "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"R_eal":::) (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ")" )))))) ; theorem :: MEASURE1:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" & "(" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ")" ))))) ; theorem :: MEASURE1:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#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 "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); attr "F" is :::"sigma-additive"::: means :: MEASURE1:def 6 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Sep_Sequence":::) "of" "S" "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" "F" ($#k1_partfun1 :::"*"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set "F" ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k4_measure1 :::"rng"::: ) (Set (Var "s")) ")" ) ")" )))); end; :: deftheorem defines :::"sigma-additive"::: MEASURE1:def 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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_measure1 :::"sigma-additive"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Sep_Sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" (Set (Var "F")) ($#k1_partfun1 :::"*"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k4_measure1 :::"rng"::: ) (Set (Var "s")) ")" ) ")" )))) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); cluster ($#v1_relat_1 :::"Relation-like"::: ) "S" ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1("S") bbbadV1_FUNCT_2("S" "," (Set ($#k7_numbers :::"ExtREAL"::: ) )) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v10_valued_0 :::"zeroed"::: ) bbbadV6_SUPINF_2() ($#v4_measure1 :::"sigma-additive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "S" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); mode sigma_Measure of "S" is ($#v10_valued_0 :::"zeroed"::: ) bbbadV6_SUPINF_2() ($#v4_measure1 :::"sigma-additive"::: ) ($#m1_subset_1 :::"Function":::) "of" "S" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_prob_1 :::"compl-closed"::: ) ($#v3_measure1 :::"sigma-additive"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finsub_1 :::"cup-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "X" ")" )); end; theorem :: MEASURE1: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")) "holds" (Bool (Set (Var "M")) "is" ($#m1_subset_1 :::"Measure":::) "of" (Set (Var "S")))))) ; theorem :: MEASURE1: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 "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k1_measure1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B")) ")" ))))))) ; theorem :: MEASURE1:31 (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")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B")))))))) ; theorem :: MEASURE1:32 (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")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "B")) ($#k3_measure1 :::"\"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")) ")" ))))))) ; theorem :: MEASURE1:33 (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")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k1_measure1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B")) ")" ))))))) ; theorem :: MEASURE1:34 (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 ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) ")" ) ")" )))) ; theorem :: MEASURE1:35 (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_subset_1 :::"N_Sub_set_fam":::) "of" (Set (Var "X")) "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")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" )) "holds" (Bool "(" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "T"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); mode :::"measure_zero"::: "of" "M" -> ($#m2_subset_1 :::"Element"::: ) "of" "S" means :: MEASURE1:def 7 (Bool (Set "M" ($#k12_supinf_2 :::"."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )); end; :: deftheorem defines :::"measure_zero"::: MEASURE1:def 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 "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) "iff" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ))))); theorem :: MEASURE1:36 (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 (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M")))))))) ; theorem :: MEASURE1:37 (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")) "," (Set (Var "B")) "being" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k1_measure1 :::"\/"::: ) (Set (Var "B"))) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) & (Bool (Set (Set (Var "A")) ($#k2_measure1 :::"/\"::: ) (Set (Var "B"))) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) & (Bool (Set (Set (Var "A")) ($#k3_measure1 :::"\"::: ) (Set (Var "B"))) "is" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M"))) ")" ))))) ; theorem :: MEASURE1:38 (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 (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m2_measure1 :::"measure_zero"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k1_measure1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k2_measure1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k3_measure1 :::"\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")))) ")" )))))) ;