:: LPSPACE2 semantic presentation begin theorem :: LPSPACE2:1 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "m")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) ; theorem :: LPSPACE2:2 (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 "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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "(" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "iff" (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" )))))) ; definitionlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; attr "r" is :::"geq_than_1"::: means :: LPSPACE2:def 1 (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) "r"); end; :: deftheorem defines :::"geq_than_1"::: LPSPACE2:def 1 : (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "r")) "is" ($#v1_lpspace2 :::"geq_than_1"::: ) ) "iff" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" )); registration cluster ($#v1_xreal_0 :::"real"::: ) ($#v1_lpspace2 :::"geq_than_1"::: ) -> ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_xxreal_0 :::"ext-real"::: ) bbbadV1_XCMPLX_0() ($#v1_xreal_0 :::"real"::: ) ($#v1_lpspace2 :::"geq_than_1"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: LPSPACE2:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "b")) ($#k4_power :::"to_power"::: ) (Set (Var "p"))))) ; theorem :: LPSPACE2:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: LPSPACE2:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k4_power :::"to_power"::: ) (Set (Var "c")) ")" )))) ; theorem :: LPSPACE2:6 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "a")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "b"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" )))))) ; theorem :: LPSPACE2:7 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "a")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "b")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" )))))) ; theorem :: LPSPACE2:8 (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 ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Num 1)) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))))) ; theorem :: LPSPACE2:9 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "seq1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq2")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "k")))) & (Bool (Set (Set (Var "seq2")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq1")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) "iff" (Bool (Set (Var "seq2")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" ))) ; theorem :: LPSPACE2:10 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ))) ; theorem :: LPSPACE2:11 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq2")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#k4_power :::"to_power"::: ) (Set (Var "k")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq2")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; begin theorem :: LPSPACE2:12 (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: LPSPACE2:13 (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 ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "D")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "D"))))))) ; registrationlet "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 ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> ($#v6_supinf_2 :::"nonnegative"::: ) ; end; theorem :: LPSPACE2:14 (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 ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))))) ; theorem :: LPSPACE2:15 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (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 ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"Lp_Functions"::: "(" "M" "," "k" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) "X" ")" ) equals :: LPSPACE2:def 2 "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "ex" (Set (Var "Ef")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "S" "st" (Bool "(" (Bool (Set "M" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "Ef")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Ef"))) & (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "Ef"))) & (Bool (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) "k") ($#r3_mesfunc6 :::"is_integrable_on"::: ) "M") ")" )) "}" ; end; :: deftheorem defines :::"Lp_Functions"::: LPSPACE2:def 2 : (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "ex" (Set (Var "Ef")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "Ef")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Ef"))) & (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "Ef"))) & (Bool (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" )) "}" ))))); theorem :: LPSPACE2:16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "b")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "k")))) & (Bool (Set (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "b")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "b")) ")" ) ")" ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "k")))) & (Bool (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "b")) ")" ) ")" ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "k")))) ")" )) ; theorem :: LPSPACE2:17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k3_power :::"to_power"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "k")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k4_power :::"to_power"::: ) (Set (Var "k")) ")" )))) ; theorem :: LPSPACE2:18 (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 ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "b")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "b")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "b"))))))) ; theorem :: LPSPACE2:19 (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 ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "b")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "b")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "b"))))))) ; theorem :: LPSPACE2:20 (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 ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")))))))) ; theorem :: LPSPACE2:21 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k4_power :::"to_power"::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "k")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "b")) ")" ) ($#k4_power :::"to_power"::: ) (Set (Var "k")) ")" ) ")" )))) ; theorem :: LPSPACE2:22 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "g")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "g")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" )) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" )))))) ; theorem :: LPSPACE2:23 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) ")" ))))) ; theorem :: LPSPACE2:24 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k4_power :::"to_power"::: ) (Set (Var "k")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "g")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))))))) ; theorem :: LPSPACE2:25 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))))))) ; theorem :: LPSPACE2:26 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )))))))) ; theorem :: LPSPACE2: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))))))) ; theorem :: LPSPACE2: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))))))) ; registrationlet "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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); cluster (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v1_lpspace1 :::"multi-closed"::: ) ; end; registrationlet "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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); cluster (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) "X" ")" ) ")" ) "," (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ")" ) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ")" ) "," (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ")" ) ")" ) "#)" ) -> ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end; 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"RLSp_LpFunct"::: "(" "M" "," "k" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: LPSPACE2:def 3 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) "X" ")" ) ")" ) "," (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ")" ) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ")" ) "," (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ")" ) ")" ) "#)" ); end; :: deftheorem defines :::"RLSp_LpFunct"::: LPSPACE2:def 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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) (Set (Var "X")) ")" ) ")" ) "," (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) ")" ) "#)" )))))); begin theorem :: LPSPACE2: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")))))))))) ; theorem :: LPSPACE2: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u"))))))))))) ; theorem :: LPSPACE2: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool "(" (Bool (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool "ex" (Set (Var "v")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ))) & (Bool (Set (Var "g")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "v")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M"))) ")" )) ")" ))))))) ; 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"AlmostZeroLpFunctions"::: "(" "M" "," "k" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" "M" "," "k" ")" ")" ) equals :: LPSPACE2:def 4 "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" )) & (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set "X" ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) "," "M") ")" ) "}" ; end; :: deftheorem defines :::"AlmostZeroLpFunctions"::: LPSPACE2: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) "," (Set (Var "M"))) ")" ) "}" ))))); registrationlet "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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); cluster (Set ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" "M" "," "k" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v1_lpspace1 :::"multi-closed"::: ) ; end; theorem :: LPSPACE2:32 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) ")" ))))) ; 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"RLSp_AlmostZeroLpFunct"::: "(" "M" "," "k" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: LPSPACE2:def 5 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" "M" "," "k" ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" "M" "," "k" ")" ")" ) ")" ) "," (Set "(" ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" "M" "," "k" ")" ")" ) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set "(" ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" "M" "," "k" ")" ")" ) "," (Set "(" ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" "M" "," "k" ")" ")" ) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set "(" ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" "M" "," "k" ")" ")" ) ")" ) "#)" ); end; :: deftheorem defines :::"RLSp_AlmostZeroLpFunct"::: LPSPACE2:def 5 : (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k4_lpspace2 :::"RLSp_AlmostZeroLpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) ")" ) "," (Set "(" ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set "(" ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set "(" ($#k3_lpspace2 :::"AlmostZeroLpFunctions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) ")" ) "#)" )))))); registrationlet "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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); cluster (Set ($#k2_lpspace2 :::"RLSp_LpFunct"::: ) "(" "M" "," "k" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end; theorem :: LPSPACE2: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_lpspace2 :::"RLSp_AlmostZeroLpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "u")))))))))) ; theorem :: LPSPACE2:34 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_lpspace2 :::"RLSp_AlmostZeroLpFunct"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u"))))))))))) ; 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"a.e-eq-class_Lp"::: "(" "f" "," "M" "," "k" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ")" ) equals :: LPSPACE2:def 6 "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" )) & (Bool "f" ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "h")) "," "M") ")" ) "}" ; end; :: deftheorem defines :::"a.e-eq-class_Lp"::: LPSPACE2:def 6 : (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "h")) "," (Set (Var "M"))) ")" ) "}" )))))); theorem :: LPSPACE2:35 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ))))))) ; theorem :: LPSPACE2:36 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "f")) "," (Set (Var "M")))) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))))))) ; theorem :: LPSPACE2:37 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "f")) "," (Set (Var "M"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) ")" )))))) ; theorem :: LPSPACE2:38 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))))))) ; theorem :: LPSPACE2:39 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "g")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M")))))))) ; theorem :: LPSPACE2:40 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "g")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M")))))))) ; theorem :: LPSPACE2:41 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M")))) "holds" (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))))))) ; theorem :: LPSPACE2:42 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M")))) "holds" (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))))))) ; theorem :: LPSPACE2:43 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))))))) ; theorem :: LPSPACE2:44 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "," (Set (Var "g")) "," (Set (Var "g1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")))) & (Bool (Set (Var "f1")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "g")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g1")))) & (Bool (Set (Var "g1")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool (Bool "not" (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f1")) "," (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g1")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g1")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))))))) ; theorem :: LPSPACE2:45 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "," (Set (Var "g")) "," (Set (Var "g1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "f1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f1")) "," (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g1")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g1")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))))))) ; theorem :: LPSPACE2:46 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "g")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool (Bool "not" (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" )))))))) ; theorem :: LPSPACE2:47 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" )))))))) ; 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"CosetSet"::: "(" "M" "," "k" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" ")" ) equals :: LPSPACE2:def 7 "{" (Set "(" ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," "M" "," "k" ")" ")" ) where f "is" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" "M" "," "k" ")" )) "}" ; end; :: deftheorem defines :::"CosetSet"::: LPSPACE2:def 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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k6_lpspace2 :::"CosetSet"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) where f "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) "}" ))))); 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"addCoset"::: "(" "M" "," "k" ")" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k6_lpspace2 :::"CosetSet"::: ) "(" "M" "," "k" ")" ")" ) means :: LPSPACE2:def 8 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_lpspace2 :::"CosetSet"::: ) "(" "M" "," "k" ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_valued_1 :::"+"::: ) (Set (Var "b")) ")" ) "," "M" "," "k" ")" )))); end; :: deftheorem defines :::"addCoset"::: LPSPACE2:def 8 : (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k6_lpspace2 :::"CosetSet"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k7_lpspace2 :::"addCoset"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_lpspace2 :::"CosetSet"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "b5")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_valued_1 :::"+"::: ) (Set (Var "b")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" )))) ")" )))))); 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"zeroCoset"::: "(" "M" "," "k" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_lpspace2 :::"CosetSet"::: ) "(" "M" "," "k" ")" ) equals :: LPSPACE2:def 9 (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" "X" ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," "M" "," "k" ")" ); end; :: deftheorem defines :::"zeroCoset"::: LPSPACE2:def 9 : (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k8_lpspace2 :::"zeroCoset"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" )))))); 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"lmultCoset"::: "(" "M" "," "k" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k6_lpspace2 :::"CosetSet"::: ) "(" "M" "," "k" ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k6_lpspace2 :::"CosetSet"::: ) "(" "M" "," "k" ")" ")" ) means :: LPSPACE2:def 10 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_lpspace2 :::"CosetSet"::: ) "(" "M" "," "k" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "z")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," "M" "," "k" ")" ))))); end; :: deftheorem defines :::"lmultCoset"::: LPSPACE2:def 10 : (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k6_lpspace2 :::"CosetSet"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k6_lpspace2 :::"CosetSet"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k9_lpspace2 :::"lmultCoset"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_lpspace2 :::"CosetSet"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "b5")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "z")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" ))))) ")" )))))); 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"Pre-Lp-Space"::: "(" "M" "," "k" ")" -> ($#v1_rlvect_1 :::"strict"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) means :: LPSPACE2:def 11 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_lpspace2 :::"CosetSet"::: ) "(" "M" "," "k" ")" )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k7_lpspace2 :::"addCoset"::: ) "(" "M" "," "k" ")" )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k8_lpspace2 :::"zeroCoset"::: ) "(" "M" "," "k" ")" )) & (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k9_lpspace2 :::"lmultCoset"::: ) "(" "M" "," "k" ")" )) ")" ); end; :: deftheorem defines :::"Pre-Lp-Space"::: LPSPACE2:def 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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "b5")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lpspace2 :::"CosetSet"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k7_lpspace2 :::"addCoset"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k8_lpspace2 :::"zeroCoset"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k9_lpspace2 :::"lmultCoset"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) ")" ) ")" )))))); registrationlet "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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); cluster (Set ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" "M" "," "k" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ; end; registrationlet "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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); cluster (Set ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" "M" "," "k" ")" ) -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_rlvect_1 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end; begin theorem :: LPSPACE2:48 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M")))) "holds" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "g")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" ))))))) ; theorem :: LPSPACE2:49 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" )) ")" )))))) ; theorem :: LPSPACE2:50 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) ")" )))))) ; theorem :: LPSPACE2:51 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) ")" ))))))) ; theorem :: LPSPACE2:52 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M"))) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "g")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" )) ")" ))))))) ; 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"Lp-Norm"::: "(" "M" "," "k" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" "M" "," "k" ")" ")" )) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: LPSPACE2:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" "M" "," "k" ")" ")" ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" "M" "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) "k" ")" ) ")" )) & (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) "k" ")" ))) ")" )) ")" ))); end; :: deftheorem defines :::"Lp-Norm"::: LPSPACE2:def 12 : (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" )) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k11_lpspace2 :::"Lp-Norm"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" )) & (Bool (Set (Set (Var "b5")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "k")) ")" ))) ")" )) ")" ))) ")" )))))); 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::); func :::"Lp-Space"::: "(" "M" "," "k" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) equals :: LPSPACE2:def 13 (Set ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" "M" "," "k" ")" ")" )) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" "M" "," "k" ")" ")" )) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" "M" "," "k" ")" ")" )) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" "M" "," "k" ")" ")" )) "," (Set "(" ($#k11_lpspace2 :::"Lp-Norm"::: ) "(" "M" "," "k" ")" ")" ) "#)" ); end; :: deftheorem defines :::"Lp-Space"::: LPSPACE2:def 13 : (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k12_lpspace2 :::"Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" )) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" )) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" )) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set "(" ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" )) "," (Set "(" ($#k11_lpspace2 :::"Lp-Norm"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "#)" )))))); theorem :: LPSPACE2:53 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k12_lpspace2 :::"Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "holds" (Bool "(" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" )) ")" )) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "k")) ")" ))) ")" )) ")" ) ")" )))))) ; theorem :: LPSPACE2:54 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k12_lpspace2 :::"Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "y")))) "implies" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")))) ")" & "(" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) "implies" (Bool (Set (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")))) ")" ")" )))))))) ; theorem :: LPSPACE2:55 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k12_lpspace2 :::"Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "k")) ")" ))) ")" )) ")" ))))))) ; theorem :: LPSPACE2:56 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M"))))))) ; theorem :: LPSPACE2:57 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) "," (Set (Var "M")))))))) ; theorem :: LPSPACE2:58 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: LPSPACE2:59 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "m")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "m")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "n")) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" )))))) ; theorem :: LPSPACE2:60 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "m")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "m")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "n")) ")" ))) "holds" (Bool "ex" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "m")) ")" ) ")" )) & (Bool "ex" (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "g")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "n")) ")" ) ")" )) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "r1")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "m")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" ) ")" ))) ")" )) ")" ))))))) ; theorem :: LPSPACE2:61 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "m")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "m")) ")" )) & (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "m")) ")" ) ")" )) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "g")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "m")) ")" ) ")" )) & (Bool (Set (Var "r3")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "m")) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "r3")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "m")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "r1")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "m")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "m")) ")" ) ")" ))))))))) ; registrationlet "k" be ($#v1_lpspace2 :::"geq_than_1"::: ) ($#m1_subset_1 :::"Real":::); let "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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); cluster (Set ($#k12_lpspace2 :::"Lp-Space"::: ) "(" "M" "," "k" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ; end; begin theorem :: LPSPACE2:62 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Sq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k12_lpspace2 :::"Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) (Bool "ex" (Set (Var "Fsq")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "Fsq")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Set (Var "Fsq")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Sq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "Sq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "Fsq")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "Fsq")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "Sq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "k")) ")" ))) ")" )) ")" )))))))) ; theorem :: LPSPACE2:63 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Sq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k12_lpspace2 :::"Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) (Bool "ex" (Set (Var "Fsq")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "Fsq")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool (Set (Set (Var "Fsq")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Sq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "Sq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lpspace2 :::"a.e-eq-class_Lp"::: ) "(" (Set "(" (Set (Var "Fsq")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "M")) "," (Set (Var "k")) ")" )) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "Fsq")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")) ")" ) ")" )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "Sq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "k")) ")" ))) ")" )) ")" )))))))) ; theorem :: LPSPACE2:64 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "Sq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Sq0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_normsp_0 :::"||."::: ) (Set "(" (Set (Var "Sq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "Sq0")) ")" ) ($#k4_normsp_0 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set "(" (Set (Var "Sq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "Sq0")) ")" ) ($#k4_normsp_0 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "Sq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "Sq"))) ($#r1_hidden :::"="::: ) (Set (Var "Sq0"))) ")" )))) ; theorem :: LPSPACE2:65 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "Sq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Sq")) "is" ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: ) )) "holds" (Bool "ex" (Set (Var "N")) "being" bbbadV5_VALUED_0() ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "N")) ($#k1_recdef_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "Sq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "j")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "Sq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "N")) ($#k1_recdef_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k4_power :::"to_power"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "i")) ")" ))))))) ; theorem :: LPSPACE2:66 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v2_xxreal_0 :::"positive"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) ")" )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_lpspace2 :::"Lp_Functions"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )))))))) ; theorem :: LPSPACE2: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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )))) ; theorem :: LPSPACE2:68 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "k"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))))))) ; theorem :: LPSPACE2:69 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) )) "holds" (Bool (Set ($#k5_seqfunc :::"abs"::: ) (Set (Var "F"))) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ))) ; theorem :: LPSPACE2:70 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#v1_lpspace2 :::"geq_than_1"::: ) ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Sq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k12_lpspace2 :::"Lp-Space"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "st" (Bool (Bool (Set (Var "Sq")) "is" ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: ) )) "holds" (Bool (Set (Var "Sq")) "is" ($#v3_normsp_1 :::"convergent"::: ) )))))) ; registrationlet "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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "k" be ($#v1_lpspace2 :::"geq_than_1"::: ) ($#m1_subset_1 :::"Real":::); cluster (Set ($#k12_lpspace2 :::"Lp-Space"::: ) "(" "M" "," "k" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lopban_1 :::"complete"::: ) ; end; begin theorem :: LPSPACE2:71 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k14_lpspace1 :::"CosetSet"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lpspace2 :::"CosetSet"::: ) "(" (Set (Var "M")) "," (Num 1) ")" ))))) ; theorem :: LPSPACE2:72 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k15_lpspace1 :::"addCoset"::: ) (Set (Var "M"))) ($#r1_funct_2 :::"="::: ) (Set ($#k7_lpspace2 :::"addCoset"::: ) "(" (Set (Var "M")) "," (Num 1) ")" ))))) ; theorem :: LPSPACE2:73 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k16_lpspace1 :::"zeroCoset"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k8_lpspace2 :::"zeroCoset"::: ) "(" (Set (Var "M")) "," (Num 1) ")" ))))) ; theorem :: LPSPACE2:74 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k17_lpspace1 :::"lmultCoset"::: ) (Set (Var "M"))) ($#r1_funct_2 :::"="::: ) (Set ($#k9_lpspace2 :::"lmultCoset"::: ) "(" (Set (Var "M")) "," (Num 1) ")" ))))) ; theorem :: LPSPACE2:75 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k10_lpspace2 :::"Pre-Lp-Space"::: ) "(" (Set (Var "M")) "," (Num 1) ")" ))))) ; theorem :: LPSPACE2:76 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k19_lpspace1 :::"L-1-Norm"::: ) (Set (Var "M"))) ($#r1_funct_2 :::"="::: ) (Set ($#k11_lpspace2 :::"Lp-Norm"::: ) "(" (Set (Var "M")) "," (Num 1) ")" ))))) ; theorem :: LPSPACE2:77 (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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k20_lpspace1 :::"L-1-Space"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k12_lpspace2 :::"Lp-Space"::: ) "(" (Set (Var "M")) "," (Num 1) ")" ))))) ;