:: MESFUNC2 semantic presentation begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"real-valued"::: redefine attr "f" is :::"real-valued"::: means :: MESFUNC2:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))); end; :: deftheorem defines :::"real-valued"::: MESFUNC2:def 1 : (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_valued_0 :::"real-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) ")" ))); theorem :: MESFUNC2:1 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set (Num 1) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")))))) ; theorem :: MESFUNC2:2 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "not" (Bool (Set (Var "f")) "is" bbbadV3_VALUED_0()) "or" "not" (Bool (Set (Var "g")) "is" bbbadV3_VALUED_0()) ")" )) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) ")" ))) ; theorem :: MESFUNC2:3 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "," (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV3_VALUED_0()) & (Bool (Set (Var "g")) "is" bbbadV3_VALUED_0()) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"Rational":::) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "p")) ")" ) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "g")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ")" ) ")" ")" ) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))))))))) ; begin theorem :: MESFUNC2:4 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k3_numbers :::"RAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_numbers :::"RAT"::: ) )) ")" )) ; theorem :: MESFUNC2:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "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 (Var "Z")) "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r2_wellord2 :::"are_equipotent"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "G"))))))) ; theorem :: MESFUNC2:6 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "," (Set (Var "S")) "st" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Rational":::) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "p")) ")" ) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "g")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ")" ) ")" ")" ) ")" )))))))))) ; theorem :: MESFUNC2:7 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV3_VALUED_0()) & (Bool (Set (Var "g")) "is" bbbadV3_VALUED_0()) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; theorem :: MESFUNC2:8 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set (Set (Var "f1")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "f2"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k7_mesfunc1 :::"-"::: ) (Set (Var "f2")) ")" ))))) ; theorem :: MESFUNC2:9 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set ($#k7_mesfunc1 :::"-"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")))))) ; theorem :: MESFUNC2:10 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV3_VALUED_0())) "holds" (Bool (Set (Set (Var "r")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f"))) "is" bbbadV3_VALUED_0())))) ; theorem :: MESFUNC2:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV3_VALUED_0()) & (Bool (Set (Var "g")) "is" bbbadV3_VALUED_0()) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; begin definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"max+"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC2:def 2 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_extreal2 :::"max"::: ) "(" (Set "(" "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set ($#k1_supinf_2 :::"0."::: ) ) ")" )) ")" ) ")" ); func :::"max-"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC2:def 3 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_extreal2 :::"max"::: ) "(" (Set "(" ($#k2_supinf_2 :::"-"::: ) (Set "(" "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) "," (Set ($#k1_supinf_2 :::"0."::: ) ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"max+"::: MESFUNC2:def 2 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_extreal2 :::"max"::: ) "(" (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set ($#k1_supinf_2 :::"0."::: ) ) ")" )) ")" ) ")" ) ")" ))); :: deftheorem defines :::"max-"::: MESFUNC2:def 3 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_extreal2 :::"max"::: ) "(" (Set "(" ($#k2_supinf_2 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) "," (Set ($#k1_supinf_2 :::"0."::: ) ) ")" )) ")" ) ")" ) ")" ))); theorem :: MESFUNC2:12 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))))) ; theorem :: MESFUNC2:13 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))))) ; theorem :: MESFUNC2:14 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k1_mesfunc2 :::"max+"::: ) (Set "(" ($#k7_mesfunc1 :::"-"::: ) (Set (Var "f")) ")" ))))) ; theorem :: MESFUNC2:15 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))))) ; theorem :: MESFUNC2:16 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))))) ; theorem :: MESFUNC2:17 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc1 :::"-"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ")" ))) ")" ))) ; theorem :: MESFUNC2:18 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) "or" (Bool (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ) & (Bool "(" (Bool (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ))) "or" (Bool (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ) ")" )))) ; theorem :: MESFUNC2:19 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))))) ; theorem :: MESFUNC2:20 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: MESFUNC2:21 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" )))) "holds" (Bool (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))))) ; theorem :: MESFUNC2:22 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))))) ; theorem :: MESFUNC2:23 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc1 :::"-"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ))))) ; theorem :: MESFUNC2:24 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ))))) ; begin theorem :: MESFUNC2:25 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; theorem :: MESFUNC2:26 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; theorem :: MESFUNC2:27 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) ) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; begin definitionlet "A", "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"chi"::: redefine func :::"chi"::: "(" "A" "," "X" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; theorem :: MESFUNC2:28 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_mesfunc2 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "X")) ")" ) "is" bbbadV3_VALUED_0())))) ; theorem :: MESFUNC2:29 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_mesfunc2 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "X")) ")" ) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "B")))))) ; begin 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"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_prob_2 :::"disjoint_valued"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" "S"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); mode Finite_Sep_Sequence of "S" is ($#v1_prob_2 :::"disjoint_valued"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" "S"; end; theorem :: MESFUNC2:30 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Sep_Sequence":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "G")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))))) "holds" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))))) ; theorem :: MESFUNC2:31 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); pred "f" :::"is_simple_func_in"::: "S" means :: MESFUNC2:def 4 (Bool "(" (Bool "f" "is" bbbadV3_VALUED_0()) & (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" "S" "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "y"))))) ")" ) ")" )) ")" ); end; :: deftheorem defines :::"is_simple_func_in"::: MESFUNC2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) "iff" (Bool "(" (Bool (Set (Var "f")) "is" bbbadV3_VALUED_0()) & (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "y"))))) ")" ) ")" )) ")" ) ")" )))); theorem :: MESFUNC2:32 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV3_VALUED_0())) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: MESFUNC2:33 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")))) "holds" (Bool (Set (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )) "is" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S"))))))) ; theorem :: MESFUNC2:34 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))))))) ;