:: LPSPACE1 semantic presentation begin definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "V1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "V1" is :::"multi-closed"::: means :: LPSPACE1:def 1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) "V1")) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) "V1"))); end; :: deftheorem defines :::"multi-closed"::: LPSPACE1:def 1 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "V1")) "is" ($#v1_lpspace1 :::"multi-closed"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set (Var "V1"))))) ")" ))); theorem :: LPSPACE1:1 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "V1")) "is" ($#v1_rlsub_1 :::"linearly-closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "V1")) "is" ($#v1_ideal_1 :::"add-closed"::: ) ) & (Bool (Set (Var "V1")) "is" ($#v1_lpspace1 :::"multi-closed"::: ) ) ")" ) ")" ))) ; registrationlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v1_lpspace1 :::"multi-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")); end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "X1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_lpspace1 :::"multi-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func :::"Mult_"::: "X1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," "X1" ($#k2_zfmisc_1 :::":]"::: ) ) "," "X1" equals :: LPSPACE1:def 2 (Set (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" "X") ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," "X1" ($#k2_zfmisc_1 :::":]"::: ) )); end; :: deftheorem defines :::"Mult_"::: LPSPACE1:def 2 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_lpspace1 :::"multi-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_lpspace1 :::"Mult_"::: ) (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "X"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "X1")) ($#k2_zfmisc_1 :::":]"::: ) ))))); theorem :: LPSPACE1:2 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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"::: ) (Bool "for" (Set (Var "V1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "d1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "V1")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "V1")) "st" (Bool (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) ($#k1_realset1 :::"||"::: ) (Set (Var "V1")))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "V1")) ($#k2_zfmisc_1 :::":]"::: ) )))) "holds" (Bool "(" (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set (Var "d1")) "," (Set (Var "A")) "," (Set (Var "M")) "#)" ) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set (Var "d1")) "," (Set (Var "A")) "," (Set (Var "M")) "#)" ) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set (Var "d1")) "," (Set (Var "A")) "," (Set (Var "M")) "#)" ) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set (Var "d1")) "," (Set (Var "A")) "," (Set (Var "M")) "#)" ) "is" ($#v5_rlvect_1 :::"vector-distributive"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set (Var "d1")) "," (Set (Var "A")) "," (Set (Var "M")) "#)" ) "is" ($#v6_rlvect_1 :::"scalar-distributive"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set (Var "d1")) "," (Set (Var "A")) "," (Set (Var "M")) "#)" ) "is" ($#v7_rlvect_1 :::"scalar-associative"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set (Var "d1")) "," (Set (Var "A")) "," (Set (Var "M")) "#)" ) "is" ($#v8_rlvect_1 :::"scalar-unital"::: ) ) ")" )))))) ; theorem :: LPSPACE1:3 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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"::: ) (Bool "for" (Set (Var "V1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v1_lpspace1 :::"multi-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))) "holds" (Bool "(" (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "V1")) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set (Var "V1")) ")" ) "#)" ) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "V1")) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set (Var "V1")) ")" ) "#)" ) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "V1")) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set (Var "V1")) ")" ) "#)" ) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "V1")) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set (Var "V1")) ")" ) "#)" ) "is" ($#v5_rlvect_1 :::"vector-distributive"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "V1")) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set (Var "V1")) ")" ) "#)" ) "is" ($#v6_rlvect_1 :::"scalar-distributive"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "V1")) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set (Var "V1")) ")" ) "#)" ) "is" ($#v7_rlvect_1 :::"scalar-associative"::: ) ) & (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "V1")) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set (Var "V1")) ")" ) "#)" ) "is" ($#v8_rlvect_1 :::"scalar-unital"::: ) ) ")" ))) ; theorem :: LPSPACE1:4 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "V1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v1_lpspace1 :::"multi-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "V1")) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set (Var "V1")) ")" ) "#)" ) "st" (Bool (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "w2")) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set (Set (Var "w1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "u")))))))) ; theorem :: LPSPACE1:5 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "V1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v1_lpspace1 :::"multi-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "V1")) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set (Var "V1")) ")" ) "#)" ) "st" (Bool (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))))))) ; begin definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "A")) "," (Set (Const "B")) ")" ")" ); let "f", "g" be ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "A")) "," (Set (Const "B")) ")" ); :: original: :::"."::: redefine func "F" :::"."::: "(" "f" "," "g" ")" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "A" "," "B" ")" ); end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"multpfunc"::: "A" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) means :: LPSPACE1:def 3 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set it ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k7_rfunct_3 :::"(#)"::: ) (Set (Var "g"))))); end; :: deftheorem defines :::"multpfunc"::: LPSPACE1:def 3 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k7_rfunct_3 :::"(#)"::: ) (Set (Var "g"))))) ")" ))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"multrealpfunc"::: "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) means :: LPSPACE1:def 4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_rfunct_3 :::"(#)"::: ) (Set (Var "f")))))); end; :: deftheorem defines :::"multrealpfunc"::: LPSPACE1:def 4 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_rfunct_3 :::"(#)"::: ) (Set (Var "f")))))) ")" ))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"RealPFuncZero"::: "A" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) equals :: LPSPACE1:def 5 (Set "A" ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"RealPFuncZero"::: LPSPACE1:def 5 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_lpspace1 :::"RealPFuncZero"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"RealPFuncUnit"::: "A" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) equals :: LPSPACE1:def 6 (Set "A" ($#k8_funcop_1 :::"-->"::: ) (Num 1)); end; :: deftheorem defines :::"RealPFuncUnit"::: LPSPACE1:def 6 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_lpspace1 :::"RealPFuncUnit"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_funcop_1 :::"-->"::: ) (Num 1)))); theorem :: LPSPACE1:6 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))) ; theorem :: LPSPACE1:7 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))) ; theorem :: LPSPACE1:8 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_lpspace1 :::"RealPFuncZero"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_lpspace1 :::"RealPFuncUnit"::: ) (Set (Var "A"))))) ; theorem :: LPSPACE1:9 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" )) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )))) ; theorem :: LPSPACE1:10 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))) ; theorem :: LPSPACE1:11 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set "(" (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "h")) ")" )))) ; theorem :: LPSPACE1:12 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))) ; theorem :: LPSPACE1:13 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set "(" (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "h")) ")" )))) ; theorem :: LPSPACE1:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set "(" ($#k6_lpspace1 :::"RealPFuncUnit"::: ) (Set (Var "A")) ")" ) "," (Set (Var "f")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))))) ; theorem :: LPSPACE1:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set "(" ($#k5_lpspace1 :::"RealPFuncZero"::: ) (Set (Var "A")) ")" ) "," (Set (Var "f")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))))) ; theorem :: LPSPACE1:16 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_lpspace1 :::"RealPFuncZero"::: ) (Set (Var "A")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ))))) ; theorem :: LPSPACE1:17 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Num 1) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: LPSPACE1:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) "," (Set (Var "f")) ")" ))))) ; theorem :: LPSPACE1:19 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) "," (Set (Var "f")) ")" ))))) ; theorem :: LPSPACE1:20 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set "(" (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set "(" (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ")" )))) ; theorem :: LPSPACE1:21 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set "(" ($#k3_lpspace1 :::"multpfunc"::: ) (Set (Var "A")) ")" ) ($#k2_lpspace1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"RLSp_PFunct"::: "A" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: LPSPACE1:def 7 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k5_lpspace1 :::"RealPFuncZero"::: ) "A" ")" ) "," (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) "A" ")" ) "," (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) "A" ")" ) "#)" ); end; :: deftheorem defines :::"RLSp_PFunct"::: LPSPACE1:def 7 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_lpspace1 :::"RLSp_PFunct"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k5_lpspace1 :::"RealPFuncZero"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k4_lpspace1 :::"multrealpfunc"::: ) (Set (Var "A")) ")" ) "#)" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_lpspace1 :::"RLSp_PFunct"::: ) "A") -> ($#~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; begin theorem :: LPSPACE1: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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Set (Var "E")) ($#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_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k7_mesfunc5 :::"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 "r" be ($#m1_subset_1 :::"Real":::); :: original: :::"-->"::: redefine func "X" :::"-->"::: "r" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ); 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")); func :::"L1_Functions"::: "M" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) "X" ")" ) equals :: LPSPACE1:def 8 "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "ex" (Set (Var "ND")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "S" "st" (Bool "(" (Bool (Set "M" ($#k3_funct_2 :::"."::: ) (Set (Var "ND"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "ND")) ($#k3_subset_1 :::"`"::: ) )) & (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) "M") ")" )) "}" ; end; :: deftheorem defines :::"L1_Functions"::: LPSPACE1: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")) "holds" (Bool (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "ex" (Set (Var "ND")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k3_funct_2 :::"."::: ) (Set (Var "ND"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "ND")) ($#k3_subset_1 :::"`"::: ) )) & (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" )) "}" )))); theorem :: LPSPACE1: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 "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 ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))))))) ; theorem :: LPSPACE1:24 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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 "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (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")); cluster (Set ($#k9_lpspace1 :::"L1_Functions"::: ) "M") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v1_lpspace1 :::"multi-closed"::: ) ; 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")); func :::"RLSp_L1Funct"::: "M" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: LPSPACE1:def 9 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k9_lpspace1 :::"L1_Functions"::: ) "M" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) "X" ")" ) ")" ) "," (Set "(" ($#k9_lpspace1 :::"L1_Functions"::: ) "M" ")" ) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set "(" ($#k9_lpspace1 :::"L1_Functions"::: ) "M" ")" ) "," (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) "X" ")" ) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set "(" ($#k9_lpspace1 :::"L1_Functions"::: ) "M" ")" ) ")" ) "#)" ); end; :: deftheorem defines :::"RLSp_L1Funct"::: LPSPACE1: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")) "holds" (Bool (Set ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) (Set (Var "X")) ")" ) ")" ) "," (Set "(" ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")) ")" ) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set "(" ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k7_lpspace1 :::"RLSp_PFunct"::: ) (Set (Var "X")) ")" ) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set "(" ($#k9_lpspace1 :::"L1_Functions"::: ) (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")); cluster (Set ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) "M") -> ($#~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; begin theorem :: LPSPACE1: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 "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) (Set (Var "M")) ")" ) "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 :: LPSPACE1:26 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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 "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) (Set (Var "M")) ")" ) "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", "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); pred "f" :::"a.e.="::: "g" "," "M" means :: LPSPACE1:def 10 (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "S" "st" (Bool "(" (Bool (Set "M" ($#k3_funct_2 :::"."::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r2_relset_1 :::"="::: ) (Set "g" ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" ))) ")" )); end; :: deftheorem defines :::"a.e.="::: LPSPACE1: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 "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M"))) "iff" (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "M")) ($#k3_funct_2 :::"."::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "E")) ($#k3_subset_1 :::"`"::: ) ")" ))) ")" )) ")" ))))); theorem :: LPSPACE1: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")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) (Set (Var "M")) ")" ) "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 ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (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"))) ")" )) ")" )))))) ; theorem :: LPSPACE1: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"::: ) ) "holds" (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "f")) "," (Set (Var "M"))))))) ; theorem :: LPSPACE1: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"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M")))) "holds" (Bool (Set (Var "g")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "f")) "," (Set (Var "M"))))))) ; theorem :: LPSPACE1: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")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "h")) "," (Set (Var "M")))) "holds" (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "h")) "," (Set (Var "M"))))))) ; theorem :: LPSPACE1: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")) "," (Set (Var "f1")) "," (Set (Var "g")) "," (Set (Var "g1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "f1")) "," (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g1")) "," (Set (Var "M")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g1"))) "," (Set (Var "M"))))))) ; theorem :: LPSPACE1:32 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M")))) "holds" (Bool (Set (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (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")); func :::"AlmostZeroFunctions"::: "M" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) "M" ")" ) equals :: LPSPACE1:def 11 "{" (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 ($#k9_lpspace1 :::"L1_Functions"::: ) "M")) & (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set "X" ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) "," "M") ")" ) "}" ; end; :: deftheorem defines :::"AlmostZeroFunctions"::: LPSPACE1: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")) "holds" (Bool (Set ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) (Set (Var "M"))) ($#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 ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) "," (Set (Var "M"))) ")" ) "}" )))); theorem :: LPSPACE1:33 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ))) ; 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")); cluster (Set ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) "M") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v1_lpspace1 :::"multi-closed"::: ) ; end; theorem :: LPSPACE1: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")) "holds" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) (Set (Var "M")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) (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")); func :::"RLSp_AlmostZeroFunct"::: "M" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: LPSPACE1:def 12 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) "M" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) "M" ")" ) ")" ) "," (Set "(" ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) "M" ")" ) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set "(" ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) "M" ")" ) "," (Set "(" ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) "M" ")" ) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set "(" ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) "M" ")" ) ")" ) "#)" ); end; :: deftheorem defines :::"RLSp_AlmostZeroFunct"::: LPSPACE1: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")) "holds" (Bool (Set ($#k12_lpspace1 :::"RLSp_AlmostZeroFunct"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) (Set (Var "M")) ")" ) ")" ) "," (Set "(" ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) (Set (Var "M")) ")" ) ")" ")" ) "," (Set "(" ($#k1_ideal_1 :::"add|"::: ) "(" (Set "(" ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) (Set (Var "M")) ")" ) ")" ")" ) "," (Set "(" ($#k1_lpspace1 :::"Mult_"::: ) (Set "(" ($#k11_lpspace1 :::"AlmostZeroFunctions"::: ) (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")); cluster (Set ($#k10_lpspace1 :::"RLSp_L1Funct"::: ) "M") -> ($#~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 :: LPSPACE1: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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k12_lpspace1 :::"RLSp_AlmostZeroFunct"::: ) (Set (Var "M")) ")" ) "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 :: LPSPACE1:36 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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 "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k12_lpspace1 :::"RLSp_AlmostZeroFunct"::: ) (Set (Var "M")) ")" ) "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"::: ) ); func :::"a.e-eq-class"::: "(" "f" "," "M" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_lpspace1 :::"L1_Functions"::: ) "M" ")" ) equals :: LPSPACE1:def 13 "{" (Set (Var "g")) where g "is" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) "M")) & (Bool "f" ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) "M")) & (Bool "f" ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," "M") ")" ) "}" ; end; :: deftheorem defines :::"a.e-eq-class"::: LPSPACE1: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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "g")) where g "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M"))) ")" ) "}" ))))); theorem :: LPSPACE1: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"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M"))))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "f")) "," (Set (Var "M"))) "iff" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" )) ")" ))))) ; theorem :: LPSPACE1: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"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" )))))) ; theorem :: LPSPACE1: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 "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 ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M"))))) "holds" (Bool "(" (Bool (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) ")" )) "iff" (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M"))) ")" ))))) ; theorem :: LPSPACE1: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"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M"))))) "holds" (Bool "(" (Bool (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) ")" )) "iff" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" )) ")" ))))) ; theorem :: LPSPACE1: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 "f1")) "," (Set (Var "g")) "," (Set (Var "g1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "f1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f1")) "," (Set (Var "M")) ")" )) & (Bool (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "g1")) "," (Set (Var "M")) ")" ))) "holds" (Bool (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g1")) ")" ) "," (Set (Var "M")) ")" )))))) ; theorem :: LPSPACE1:42 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "g")) "," (Set (Var "M")) ")" ))) "holds" (Bool (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (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")); func :::"CosetSet"::: "M" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k9_lpspace1 :::"L1_Functions"::: ) "M" ")" ) equals :: LPSPACE1:def 14 "{" (Set "(" ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," "M" ")" ")" ) where f "is" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) "M")) "}" ; end; :: deftheorem defines :::"CosetSet"::: LPSPACE1:def 14 : (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 "(" ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" ")" ) where f "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (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")); func :::"addCoset"::: "M" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k14_lpspace1 :::"CosetSet"::: ) "M" ")" ) means :: LPSPACE1:def 15 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k14_lpspace1 :::"CosetSet"::: ) "M") (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 ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_valued_1 :::"+"::: ) (Set (Var "b")) ")" ) "," "M" ")" )))); end; :: deftheorem defines :::"addCoset"::: LPSPACE1:def 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 "b4")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k14_lpspace1 :::"CosetSet"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k15_lpspace1 :::"addCoset"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k14_lpspace1 :::"CosetSet"::: ) (Set (Var "M"))) (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 "b4")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_valued_1 :::"+"::: ) (Set (Var "b")) ")" ) "," (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")); func :::"zeroCoset"::: "M" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k14_lpspace1 :::"CosetSet"::: ) "M") means :: LPSPACE1:def 16 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set "X" ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) "M")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," "M" ")" )) ")" )); end; :: deftheorem defines :::"zeroCoset"::: LPSPACE1:def 16 : (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 "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k14_lpspace1 :::"CosetSet"::: ) (Set (Var "M"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k16_lpspace1 :::"zeroCoset"::: ) (Set (Var "M")))) "iff" (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_relset_1 :::"="::: ) (Set (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (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")); func :::"lmultCoset"::: "M" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k14_lpspace1 :::"CosetSet"::: ) "M" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k14_lpspace1 :::"CosetSet"::: ) "M" ")" ) means :: LPSPACE1:def 17 (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 ($#k14_lpspace1 :::"CosetSet"::: ) "M") (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 ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set "(" (Set (Var "z")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," "M" ")" ))))); end; :: deftheorem defines :::"lmultCoset"::: LPSPACE1:def 17 : (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 "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k14_lpspace1 :::"CosetSet"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k14_lpspace1 :::"CosetSet"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k17_lpspace1 :::"lmultCoset"::: ) (Set (Var "M")))) "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 ($#k14_lpspace1 :::"CosetSet"::: ) (Set (Var "M"))) (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 "b4")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set "(" (Set (Var "z")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (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")); func :::"Pre-L-Space"::: "M" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) means :: LPSPACE1:def 18 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k14_lpspace1 :::"CosetSet"::: ) "M")) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k15_lpspace1 :::"addCoset"::: ) "M")) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k16_lpspace1 :::"zeroCoset"::: ) "M")) & (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k17_lpspace1 :::"lmultCoset"::: ) "M")) ")" ); end; :: deftheorem defines :::"Pre-L-Space"::: LPSPACE1:def 18 : (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 "b4")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k14_lpspace1 :::"CosetSet"::: ) (Set (Var "M")))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b4"))) ($#r1_funct_2 :::"="::: ) (Set ($#k15_lpspace1 :::"addCoset"::: ) (Set (Var "M")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k16_lpspace1 :::"zeroCoset"::: ) (Set (Var "M")))) & (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "b4"))) ($#r1_funct_2 :::"="::: ) (Set ($#k17_lpspace1 :::"lmultCoset"::: ) (Set (Var "M")))) ")" ) ")" ))))); begin theorem :: LPSPACE1: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"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M")))) "holds" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "g")) ")" )))))) ; theorem :: LPSPACE1: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")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "(" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ))))) ; theorem :: LPSPACE1: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 "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "f")) ($#r1_lpspace1 :::"a.e.="::: ) (Set (Var "g")) "," (Set (Var "M")))) "holds" (Bool "(" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) ($#r1_lpspace1 :::"a.e.="::: ) (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "g"))) "," (Set (Var "M"))) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "g")) ")" ) ")" )) ")" ))))) ; theorem :: LPSPACE1: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"::: ) ) "st" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M")) ")" ) "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 ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) ")" ))))) ; theorem :: LPSPACE1: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")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" )))))) ; theorem :: LPSPACE1: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 "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M")) ")" ) "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 (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "g")) ")" )) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "g")) ")" ) ")" )) ")" )))))) ; 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")); func :::"L-1-Norm"::: "M" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) "M" ")" )) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: LPSPACE1:def 19 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) "M" ")" ) (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 (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" "M" "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" )) ")" ))); end; :: deftheorem defines :::"L-1-Norm"::: LPSPACE1:def 19 : (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 "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M")) ")" )) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k19_lpspace1 :::"L-1-Norm"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M")) ")" ) (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 (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" )) ")" ))) ")" ))))); 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")); func :::"L-1-Space"::: "M" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) equals :: LPSPACE1:def 20 (Set ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) "M" ")" )) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) "M" ")" )) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) "M" ")" )) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) "M" ")" )) "," (Set "(" ($#k19_lpspace1 :::"L-1-Norm"::: ) "M" ")" ) "#)" ); end; :: deftheorem defines :::"L-1-Space"::: LPSPACE1:def 20 : (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 ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M")) ")" )) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M")) ")" )) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M")) ")" )) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set "(" ($#k18_lpspace1 :::"Pre-L-Space"::: ) (Set (Var "M")) ")" )) "," (Set "(" ($#k19_lpspace1 :::"L-1-Norm"::: ) (Set (Var "M")) ")" ) "#)" ))))); theorem :: LPSPACE1: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 "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k20_lpspace1 :::"L-1-Space"::: ) (Set (Var "M")) ")" ) "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 ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" )) ")" )) & (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 (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )) ")" ) ")" ))))) ; theorem :: LPSPACE1: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")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k20_lpspace1 :::"L-1-Space"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k13_lpspace1 :::"a.e-eq-class"::: ) "(" (Set (Var "f")) "," (Set (Var "M")) ")" )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" )) ")" )))))) ; theorem :: LPSPACE1:51 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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 "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k20_lpspace1 :::"L-1-Space"::: ) (Set (Var "M")) ")" ) "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 :: LPSPACE1:52 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 "E")) "being" ($#m2_subset_1 :::"Element"::: ) "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 "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: LPSPACE1: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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_lpspace1 :::"L1_Functions"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" ) ($#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 :: LPSPACE1: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")) "holds" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "X")) ($#k8_lpspace1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: LPSPACE1: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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "g")) ")" ) ")" ")" ))))))) ; 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")); cluster (Set ($#k20_lpspace1 :::"L-1-Space"::: ) "M") -> ($#~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"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ; end;