:: RSSPACE3 semantic presentation begin definitionfunc :::"the_set_of_l1RealSequences"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) means :: RSSPACE3:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) )) & (Bool (Set ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x"))) "is" ($#v2_series_1 :::"absolutely_summable"::: ) ) ")" ) ")" )); end; :: deftheorem defines :::"the_set_of_l1RealSequences"::: RSSPACE3:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) )) & (Bool (Set ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x"))) "is" ($#v2_series_1 :::"absolutely_summable"::: ) ) ")" ) ")" )) ")" )); theorem :: RSSPACE3:1 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Var "rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq"))) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "c")) ")" ))) ")" )))) ; registration cluster (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registration cluster (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) -> ($#v1_rlsub_1 :::"linearly-closed"::: ) ; end; registration cluster (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "#)" ) -> ($#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"::: ) ; end; definitionfunc :::"l_norm"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: RSSPACE3:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x")) ")" ) ")" )))); end; :: deftheorem defines :::"l_norm"::: RSSPACE3:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_rsspace3 :::"l_norm"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x")) ")" ) ")" )))) ")" )); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); let "A" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Const "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "X")); let "N" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" "X" "," "Z" "," "A" "," "M" "," "N" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: RSSPACE3:2 (Bool "for" (Set (Var "l")) "being" ($#l1_normsp_1 :::"NORMSTR"::: ) "st" (Bool (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "l"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "l"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "l"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "l"))) "#)" ) "is" ($#l1_rlvect_1 :::"RealLinearSpace":::))) "holds" (Bool (Set (Var "l")) "is" ($#l1_rlvect_1 :::"RealLinearSpace":::))) ; theorem :: RSSPACE3:3 (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Var "rseq")) "is" ($#v2_series_1 :::"absolutely_summable"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "rseq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: RSSPACE3:4 (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "rseq")) "is" ($#v2_series_1 :::"absolutely_summable"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "rseq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: RSSPACE3:5 (Bool (Set ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set ($#k2_rsspace3 :::"l_norm"::: ) ) "#)" ) "is" ($#l1_rlvect_1 :::"RealLinearSpace":::)) ; definitionfunc :::"l1_Space"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) equals :: RSSPACE3:def 3 (Set ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set ($#k2_rsspace3 :::"l_norm"::: ) ) "#)" ); end; :: deftheorem defines :::"l1_Space"::: RSSPACE3:def 3 : (Bool (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set ($#k2_rsspace3 :::"l_norm"::: ) ) "#)" )); begin theorem :: RSSPACE3:6 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_rsspace3 :::"the_set_of_l1RealSequences"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) )) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Real_Sequence":::)) & (Bool (Set ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x"))) "is" ($#v2_series_1 :::"absolutely_summable"::: ) ) ")" ) ")" ) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k3_rsspace3 :::"l1_Space"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_rsspace :::"Zeroseq"::: ) )) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k2_rsspace :::"seq_id"::: ) (Set (Var "u")))) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) "holds" (Bool (Set (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "u")) ")" ) ($#k1_series_1 :::"+"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "v")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) "holds" (Bool (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "u")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "u")) ")" ))) & (Bool (Set ($#k2_rsspace :::"seq_id"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "u")) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) "holds" (Bool (Set (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "u")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "v")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) "holds" (Bool (Set ($#k2_rsspace :::"seq_id"::: ) (Set (Var "v"))) "is" ($#v2_series_1 :::"absolutely_summable"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "v")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "v")) ")" ) ")" ))) ")" ) ")" ) ; theorem :: RSSPACE3:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k3_rsspace3 :::"l1_Space"::: ) ))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k3_rsspace3 :::"l1_Space"::: ) )))) "implies" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) ))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ))) ")" ))) ; registration cluster (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"dist"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Real":::) equals :: RSSPACE3:def 4 (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" "x" ($#k5_algstr_0 :::"-"::: ) "y" ")" ) ($#k1_normsp_0 :::".||"::: ) ); end; :: deftheorem defines :::"dist"::: RSSPACE3:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_rsspace3 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )))); definitionlet "NRM" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) ; let "seqt" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "NRM")); attr "seqt" is :::"CCauchy"::: means :: RSSPACE3:def 5 (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "k1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n1")) "," (Set (Var "m1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k1"))) & (Bool (Set (Var "m1")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k1")))) "holds" (Bool (Set ($#k4_rsspace3 :::"dist"::: ) "(" (Set "(" "seqt" ($#k1_normsp_1 :::"."::: ) (Set (Var "n1")) ")" ) "," (Set "(" "seqt" ($#k1_normsp_1 :::"."::: ) (Set (Var "m1")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1")))))); end; :: deftheorem defines :::"CCauchy"::: RSSPACE3:def 5 : (Bool "for" (Set (Var "NRM")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) (Bool "for" (Set (Var "seqt")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "NRM")) "holds" (Bool "(" (Bool (Set (Var "seqt")) "is" ($#v1_rsspace3 :::"CCauchy"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "k1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n1")) "," (Set (Var "m1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k1"))) & (Bool (Set (Var "m1")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k1")))) "holds" (Bool (Set ($#k4_rsspace3 :::"dist"::: ) "(" (Set "(" (Set (Var "seqt")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n1")) ")" ) "," (Set "(" (Set (Var "seqt")) ($#k1_normsp_1 :::"."::: ) (Set (Var "m1")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1")))))) ")" ))); notationlet "NRM" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) ; let "seqt" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "NRM")); synonym :::"Cauchy_sequence_by_Norm"::: "seqt" for :::"CCauchy"::: ; end; theorem :: RSSPACE3:8 (Bool "for" (Set (Var "NRM")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "NRM")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))) ; theorem :: RSSPACE3:9 (Bool "for" (Set (Var "vseq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) "st" (Bool (Bool (Set (Var "vseq")) "is" ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: ) )) "holds" (Bool (Set (Var "vseq")) "is" ($#v3_normsp_1 :::"convergent"::: ) )) ;