:: MEASURE6 semantic presentation begin theorem :: MEASURE6:1 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "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 ($#k11_funcop_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; theorem :: MEASURE6:2 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F"))))) ; theorem :: MEASURE6:3 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) & (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F")))))) ; definitionlet "x" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"R_EAL"::: "x" -> ($#m1_subset_1 :::"R_eal":::) equals :: MEASURE6:def 1 "x"; end; :: deftheorem defines :::"R_EAL"::: MEASURE6:def 1 : (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))); theorem :: MEASURE6:4 (Bool "for" (Set (Var "eps")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "eps")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "eps"))) ")" ))) ; theorem :: MEASURE6:5 (Bool "for" (Set (Var "eps")) "being" ($#m1_subset_1 :::"R_eal":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "eps"))) & (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "X")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set (Var "eps")))) ")" )))) ; theorem :: MEASURE6:6 (Bool "for" (Set (Var "eps")) "being" ($#m1_subset_1 :::"R_eal":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "eps"))) & (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Real":::))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "X")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set (Var "eps"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) ")" )))) ; theorem :: MEASURE6:7 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#v2_membered :::"ext-real-membered"::: ) ($#v3_membered :::"real-membered"::: ) ($#v6_xxreal_2 :::"interval"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: MEASURE6:8 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_measure5 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_measure5 :::".["::: ) )) ")" ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "A")))))) ; theorem :: MEASURE6:9 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_xxreal_1 :::".]"::: ) )) ")" ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "A")))))) ; theorem :: MEASURE6:10 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_xxreal_1 :::".]"::: ) )) ")" ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "A")))))) ; theorem :: MEASURE6:11 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_xxreal_1 :::".["::: ) )) ")" ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "A")))))) ; theorem :: MEASURE6:12 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_measure5 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_measure5 :::".["::: ) )) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A")))))) ; theorem :: MEASURE6:13 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_xxreal_1 :::".]"::: ) )) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A")))))) ; theorem :: MEASURE6:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_xxreal_1 :::".]"::: ) )) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A")))))) ; theorem :: MEASURE6:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_xxreal_1 :::".["::: ) )) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A")))))) ; theorem :: MEASURE6:16 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_measure5 :::"open_interval"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_measure5 :::"]."::: ) (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A")) ")" ) ($#k1_measure5 :::".["::: ) ))) ; theorem :: MEASURE6:17 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_measure5 :::"closed_interval"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_1 :::"[."::: ) (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A")) ")" ) ($#k1_xxreal_1 :::".]"::: ) ))) ; theorem :: MEASURE6:18 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_measure5 :::"right_open_interval"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_1 :::"[."::: ) (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A")) ")" ) ($#k2_xxreal_1 :::".["::: ) ))) ; theorem :: MEASURE6:19 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_measure5 :::"left_open_interval"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_1 :::"]."::: ) (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A")) ")" ) ($#k3_xxreal_1 :::".]"::: ) ))) ; theorem :: MEASURE6:20 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))))) ; theorem :: MEASURE6:21 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k9_member_1 :::"++"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "z")))) ")" )) ")" ))) ; theorem :: MEASURE6:22 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Interval":::) "st" (Bool (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "B")))) & (Bool "(" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "or" (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#m1_subset_1 :::"Interval":::))) ; definitionlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"++"::: redefine func "x" :::"++"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: MEASURE6:23 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_measure6 :::"++"::: ) (Set "(" (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: MEASURE6:24 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: MEASURE6:25 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: MEASURE6:26 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_measure5 :::"open_interval"::: ) ) "iff" (Bool (Set (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set (Var "A"))) "is" ($#v1_measure5 :::"open_interval"::: ) ) ")" ))) ; theorem :: MEASURE6:27 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_measure5 :::"closed_interval"::: ) ) "iff" (Bool (Set (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set (Var "A"))) "is" ($#v2_measure5 :::"closed_interval"::: ) ) ")" ))) ; theorem :: MEASURE6:28 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_measure5 :::"right_open_interval"::: ) ) "iff" (Bool (Set (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set (Var "A"))) "is" ($#v3_measure5 :::"right_open_interval"::: ) ) ")" ))) ; theorem :: MEASURE6:29 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_measure5 :::"left_open_interval"::: ) ) "iff" (Bool (Set (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set (Var "A"))) "is" ($#v4_measure5 :::"left_open_interval"::: ) ) ")" ))) ; theorem :: MEASURE6:30 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set (Var "A"))) "is" ($#m1_subset_1 :::"Interval":::)))) ; theorem :: MEASURE6:31 (Bool "for" (Set (Var "A")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "A")) ")" )))))) ; theorem :: MEASURE6:32 (Bool "for" (Set (Var "A")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "A")) ")" )))))) ; theorem :: MEASURE6:33 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Interval":::) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_measure5 :::"diameter"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_measure5 :::"diameter"::: ) (Set "(" (Set (Var "x")) ($#k2_measure6 :::"++"::: ) (Set (Var "A")) ")" ))))) ; begin notationlet "X" be ($#m1_hidden :::"set"::: ) ; synonym :::"without_zero"::: "X" for :::"with_non-empty_elements"::: ; antonym :::"with_zero"::: "X" for :::"with_non-empty_elements"::: ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; redefine attr "X" is :::"with_non-empty_elements"::: means :: MEASURE6:def 2 (Bool (Bool "not" (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) "X")); end; :: deftheorem defines :::"without_zero"::: MEASURE6:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_setfam_1 :::"without_zero"::: ) ) "iff" (Bool (Bool "not" (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" )); registration cluster (Set ($#k1_numbers :::"REAL"::: ) ) -> ($#v1_setfam_1 :::"with_zero"::: ) ; cluster (Set ($#k4_ordinal1 :::"omega"::: ) ) -> ($#v1_setfam_1 :::"with_zero"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"without_zero"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_zero"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#v2_membered :::"ext-real-membered"::: ) ($#v3_membered :::"real-membered"::: ) ($#v1_setfam_1 :::"without_zero"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#v2_membered :::"ext-real-membered"::: ) ($#v3_membered :::"real-membered"::: ) ($#v1_setfam_1 :::"with_zero"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: MEASURE6:34 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "F")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "F")) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ) & (Bool (Set (Var "F")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v3_finset_1 :::"centered"::: ) )) ; registrationlet "F" be ($#m1_hidden :::"set"::: ) ; cluster ($#v6_ordinal1 :::"c=-linear"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) -> ($#v3_finset_1 :::"centered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "F" ")" )); end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "f" ($#k7_relat_1 :::".:"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func :::"""::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) "Y" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) means :: MEASURE6:def 3 (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"""::: MEASURE6:def 3 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "Y")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_measure6 :::"""::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "y"))))) ")" )))); theorem :: MEASURE6:35 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k3_measure6 :::"""::: ) (Set (Var "f")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "S")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "S"))))))) ; theorem :: MEASURE6:36 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: MEASURE6:37 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "t")) ")" )))) ; theorem :: MEASURE6:38 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v2_relat_1 :::"non-zero"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "not" (Bool (Set (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ) "is" ($#v1_comseq_2 :::"bounded"::: ) ))) ; theorem :: MEASURE6:39 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ) "iff" (Bool (Set (Var "seq")) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" )) ; notationlet "X" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; synonym :::"with_max"::: "X" for :::"right_end"::: ; synonym :::"with_min"::: "X" for :::"left_end"::: ; end; definitionlet "X" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; redefine attr "X" is :::"right_end"::: means :: MEASURE6:def 4 (Bool "(" (Bool "X" "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set ($#k2_seq_4 :::"upper_bound"::: ) "X") ($#r2_hidden :::"in"::: ) "X") ")" ); redefine attr "X" is :::"left_end"::: means :: MEASURE6:def 5 (Bool "(" (Bool "X" "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set ($#k3_seq_4 :::"lower_bound"::: ) "X") ($#r2_hidden :::"in"::: ) "X") ")" ); end; :: deftheorem defines :::"with_max"::: MEASURE6:def 4 : (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_xxreal_2 :::"with_max"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set ($#k2_seq_4 :::"upper_bound"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )); :: deftheorem defines :::"with_min"::: MEASURE6:def 5 : (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_xxreal_2 :::"with_min"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set ($#k3_seq_4 :::"lower_bound"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#v2_membered :::"ext-real-membered"::: ) ($#v3_membered :::"real-membered"::: ) ($#v5_xxreal_2 :::"real-bounded"::: ) ($#v2_rcomp_1 :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; definitionlet "R" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); attr "R" is :::"open"::: means :: MEASURE6:def 6 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "R")) "holds" (Bool (Set (Var "X")) "is" ($#v3_rcomp_1 :::"open"::: ) )); attr "R" is :::"closed"::: means :: MEASURE6:def 7 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "R")) "holds" (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) )); end; :: deftheorem defines :::"open"::: MEASURE6:def 6 : (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_measure6 :::"open"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "X")) "is" ($#v3_rcomp_1 :::"open"::: ) )) ")" )); :: deftheorem defines :::"closed"::: MEASURE6:def 7 : (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_measure6 :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) )) ")" )); definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"--"::: redefine func :::"--"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: MEASURE6:40 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_measure6 :::"--"::: ) (Set (Var "X")))) ")" ))) ; theorem :: MEASURE6:41 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) "iff" (Bool (Set ($#k4_measure6 :::"--"::: ) (Set (Var "X"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) ")" )) ; theorem :: MEASURE6:42 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) "iff" (Bool (Set ($#k4_measure6 :::"--"::: ) (Set (Var "X"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" )) ; theorem :: MEASURE6:43 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k4_measure6 :::"--"::: ) (Set (Var "X")) ")" ) ")" )))) ; theorem :: MEASURE6:44 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k4_measure6 :::"--"::: ) (Set (Var "X")) ")" ) ")" )))) ; theorem :: MEASURE6:45 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) "iff" (Bool (Set ($#k4_measure6 :::"--"::: ) (Set (Var "X"))) "is" ($#v2_rcomp_1 :::"closed"::: ) ) ")" )) ; theorem :: MEASURE6:46 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Set (Var "q3")) ($#k7_real_1 :::"+"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "q3")) ($#k2_measure6 :::"++"::: ) (Set (Var "X")))) ")" )))) ; theorem :: MEASURE6:47 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k2_measure6 :::"++"::: ) (Set (Var "X"))))) ; theorem :: MEASURE6:48 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q3")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "q3")) ($#k2_measure6 :::"++"::: ) (Set "(" (Set (Var "p3")) ($#k2_measure6 :::"++"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q3")) ($#k7_real_1 :::"+"::: ) (Set (Var "p3")) ")" ) ($#k2_measure6 :::"++"::: ) (Set (Var "X")))))) ; theorem :: MEASURE6:49 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) "iff" (Bool (Set (Set (Var "q3")) ($#k2_measure6 :::"++"::: ) (Set (Var "X"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" ))) ; theorem :: MEASURE6:50 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) "iff" (Bool (Set (Set (Var "q3")) ($#k2_measure6 :::"++"::: ) (Set (Var "X"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) ")" ))) ; theorem :: MEASURE6:51 (Bool "for" (Set (Var "q3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set (Var "q3")) ($#k2_measure6 :::"++"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q3")) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X")) ")" ))))) ; theorem :: MEASURE6:52 (Bool "for" (Set (Var "q3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" (Set (Var "q3")) ($#k2_measure6 :::"++"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q3")) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X")) ")" ))))) ; theorem :: MEASURE6:53 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "q3")) ($#k2_measure6 :::"++"::: ) (Set (Var "X"))) "is" ($#v2_rcomp_1 :::"closed"::: ) ) ")" ))) ; definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Inv"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: MEASURE6:def 8 "{" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r3")) ")" ) where r3 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r3")) ($#r2_hidden :::"in"::: ) "X") "}" ; involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r3")) ")" ) where r3 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r3")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "}" )) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r3")) ")" ) where r3 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r3")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "}" )) ; end; :: deftheorem defines :::"Inv"::: MEASURE6:def 8 : (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k5_measure6 :::"Inv"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r3")) ")" ) where r3 "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "r3")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" )); theorem :: MEASURE6:54 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_measure6 :::"Inv"::: ) (Set (Var "X")))) ")" ))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k5_measure6 :::"Inv"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X" be ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k5_measure6 :::"Inv"::: ) "X") -> ($#v1_setfam_1 :::"without_zero"::: ) ; end; theorem :: MEASURE6:55 (Bool "for" (Set (Var "X")) "being" ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) & (Bool (Set (Var "X")) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) )) "holds" (Bool (Set ($#k5_measure6 :::"Inv"::: ) (Set (Var "X"))) "is" ($#v2_rcomp_1 :::"closed"::: ) )) ; theorem :: MEASURE6:56 (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v2_measure6 :::"closed"::: ) )) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "Z"))) "is" ($#v2_rcomp_1 :::"closed"::: ) )) ; definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Cl"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: MEASURE6:def 9 (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) ")" ) "}" ); projectivity (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "(" (Bool (Set (Var "b2")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) ")" ) "}" ))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "(" (Bool (Set (Var "b1")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) ")" ) "}" ))) ; end; :: deftheorem defines :::"Cl"::: MEASURE6:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k6_measure6 :::"Cl"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) ")" ) "}" ))); registrationlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k6_measure6 :::"Cl"::: ) "X") -> ($#v2_rcomp_1 :::"closed"::: ) ; end; theorem :: MEASURE6:57 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#v2_rcomp_1 :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k6_measure6 :::"Cl"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))))) ; theorem :: MEASURE6:58 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k6_measure6 :::"Cl"::: ) (Set (Var "X"))))) ; theorem :: MEASURE6:59 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_rcomp_1 :::"closed"::: ) ) "iff" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k6_measure6 :::"Cl"::: ) (Set (Var "X")))) ")" )) ; theorem :: MEASURE6:60 (Bool (Set ($#k6_measure6 :::"Cl"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: MEASURE6:61 (Bool (Set ($#k6_measure6 :::"Cl"::: ) (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: MEASURE6:62 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k6_measure6 :::"Cl"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_measure6 :::"Cl"::: ) (Set (Var "Y"))))) ; theorem :: MEASURE6:63 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "r3")) ($#r2_hidden :::"in"::: ) (Set ($#k6_measure6 :::"Cl"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "O")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r3")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool "not" (Bool (Set (Set (Var "O")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "X"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ")" ))) ; theorem :: MEASURE6:64 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r3")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r3")) ($#r2_hidden :::"in"::: ) (Set ($#k6_measure6 :::"Cl"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "r3"))) ")" )))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"bounded_below"::: redefine attr "f" is :::"bounded_below"::: means :: MEASURE6:def 10 (Bool (Set "f" ($#k7_relset_1 :::".:"::: ) "X") "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ); :: original: :::"bounded_above"::: redefine attr "f" is :::"bounded_above"::: means :: MEASURE6:def 11 (Bool (Set "f" ($#k7_relset_1 :::".:"::: ) "X") "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ); end; :: deftheorem defines :::"bounded_below"::: MEASURE6:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) ")" ))); :: deftheorem defines :::"bounded_above"::: MEASURE6:def 11 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "f" is :::"with_max"::: means :: MEASURE6:def 12 (Bool (Set "f" ($#k7_relset_1 :::".:"::: ) "X") "is" ($#v2_xxreal_2 :::"with_max"::: ) ); attr "f" is :::"with_min"::: means :: MEASURE6:def 13 (Bool (Set "f" ($#k7_relset_1 :::".:"::: ) "X") "is" ($#v1_xxreal_2 :::"with_min"::: ) ); end; :: deftheorem defines :::"with_max"::: MEASURE6:def 12 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_measure6 :::"with_max"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "is" ($#v2_xxreal_2 :::"with_max"::: ) ) ")" ))); :: deftheorem defines :::"with_min"::: MEASURE6:def 13 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_measure6 :::"with_min"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "is" ($#v1_xxreal_2 :::"with_min"::: ) ) ")" ))); theorem :: MEASURE6:65 (Bool "for" (Set (Var "X")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_measure6 :::"--"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MEASURE6:66 (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 ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_measure6 :::"with_min"::: ) ) "iff" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "f"))) "is" ($#v5_measure6 :::"with_max"::: ) ) ")" ))) ; theorem :: MEASURE6:67 (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 ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_measure6 :::"with_max"::: ) ) "iff" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "f"))) "is" ($#v6_measure6 :::"with_min"::: ) ) ")" ))) ; theorem :: MEASURE6:68 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k4_measure6 :::"--"::: ) (Set (Var "A")) ")" )))))) ; theorem :: MEASURE6:69 (Bool "for" (Set (Var "X")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set (Var "s")) ($#k9_valued_1 :::"+"::: ) (Set (Var "f")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_measure6 :::"++"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" )))))) ; theorem :: MEASURE6:70 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set (Var "q3")) ($#k9_valued_1 :::"+"::: ) (Set (Var "f")) ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "q3")) ")" ) ($#k2_measure6 :::"++"::: ) (Set (Var "A")) ")" ))))))) ; notationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); synonym :::"Inv"::: "f" for "f" :::"""::: ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"Inv"::: redefine func :::"Inv"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: MEASURE6:71 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k7_measure6 :::"Inv"::: ) (Set (Var "f")) ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k5_measure6 :::"Inv"::: ) (Set (Var "A")) ")" )))))) ; theorem :: MEASURE6:72 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_measure6 :::"--"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set (Var "a")))) ")" )))) ;