:: CSSPACE3 semantic presentation begin definitionfunc :::"the_set_of_l1ComplexSequences"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) means :: CSSPACE3: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_csspace :::"the_set_of_ComplexSequences"::: ) )) & (Bool (Set ($#k2_csspace :::"seq_id"::: ) (Set (Var "x"))) "is" ($#v2_comseq_3 :::"absolutely_summable"::: ) ) ")" ) ")" )); end; :: deftheorem defines :::"the_set_of_l1ComplexSequences"::: CSSPACE3:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) )) "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_csspace :::"the_set_of_ComplexSequences"::: ) )) & (Bool (Set ($#k2_csspace :::"seq_id"::: ) (Set (Var "x"))) "is" ($#v2_comseq_3 :::"absolutely_summable"::: ) ) ")" ) ")" )) ")" )); theorem :: CSSPACE3:1 (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (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 ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Var "rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" ($#k3_comseq_2 :::"lim"::: ) (Set (Var "seq")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )) ")" )))) ; registration cluster (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registration cluster (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) -> ($#v6_clvect_1 :::"linearly-closed"::: ) ; end; registration cluster (Set ($#g1_clvect_1 :::"CLSStruct"::: ) "(#" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set "(" ($#k10_csspace :::"Zero_"::: ) "(" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_csspace :::"Add_"::: ) "(" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_csspace :::"Mult_"::: ) "(" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")" ")" ) "#)" ) -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_clvect_1 :::"vector-distributive"::: ) ($#v3_clvect_1 :::"scalar-distributive"::: ) ($#v4_clvect_1 :::"scalar-associative"::: ) ($#v5_clvect_1 :::"scalar-unital"::: ) ; end; definitionfunc :::"cl_norm"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: CSSPACE3:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" ($#k2_csspace :::"seq_id"::: ) (Set (Var "x")) ")" ) ($#k55_valued_1 :::".|"::: ) )))); end; :: deftheorem defines :::"cl_norm"::: CSSPACE3:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_csspace3 :::"cl_norm"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" ($#k2_csspace :::"seq_id"::: ) (Set (Var "x")) ")" ) ($#k55_valued_1 :::".|"::: ) )))) ")" )); 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 ($#k2_numbers :::"COMPLEX"::: ) ) "," (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 ($#g2_clvect_1 :::"CNORMSTR"::: ) "(#" "X" "," "Z" "," "A" "," "M" "," "N" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: CSSPACE3:2 (Bool "for" (Set (Var "l")) "being" ($#l2_clvect_1 :::"CNORMSTR"::: ) "st" (Bool (Bool (Set ($#g1_clvect_1 :::"CLSStruct"::: ) "(#" (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_clvect_1 :::"Mult"::: ) "of" (Set (Var "l"))) "#)" ) "is" ($#l1_clvect_1 :::"ComplexLinearSpace":::))) "holds" (Bool (Set (Var "l")) "is" ($#l1_clvect_1 :::"ComplexLinearSpace":::))) ; theorem :: CSSPACE3:3 (Bool "for" (Set (Var "cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "cseq")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_complex1 :::"0c"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Var "cseq")) "is" ($#v2_comseq_3 :::"absolutely_summable"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "cseq")) ($#k55_valued_1 :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: CSSPACE3:4 (Bool "for" (Set (Var "cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool (Bool (Set (Var "cseq")) "is" ($#v2_comseq_3 :::"absolutely_summable"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "cseq")) ($#k55_valued_1 :::".|"::: ) )) ($#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 "cseq")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_complex1 :::"0c"::: ) )))) ; definitionfunc :::"Complex_l1_Space"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_clvect_1 :::"CNORMSTR"::: ) equals :: CSSPACE3:def 3 (Set ($#g2_clvect_1 :::"CNORMSTR"::: ) "(#" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set "(" ($#k10_csspace :::"Zero_"::: ) "(" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_csspace :::"Add_"::: ) "(" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_csspace :::"Mult_"::: ) "(" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")" ")" ) "," (Set ($#k2_csspace3 :::"cl_norm"::: ) ) "#)" ); end; :: deftheorem defines :::"Complex_l1_Space"::: CSSPACE3:def 3 : (Bool (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g2_clvect_1 :::"CNORMSTR"::: ) "(#" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set "(" ($#k10_csspace :::"Zero_"::: ) "(" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_csspace :::"Add_"::: ) "(" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_csspace :::"Mult_"::: ) "(" (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) ) "," (Set ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")" ")" ) "," (Set ($#k2_csspace3 :::"cl_norm"::: ) ) "#)" )); theorem :: CSSPACE3:5 (Bool (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) "is" ($#l1_clvect_1 :::"ComplexLinearSpace":::)) ; begin theorem :: CSSPACE3:6 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_csspace3 :::"the_set_of_l1ComplexSequences"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) )) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Complex_Sequence":::)) & (Bool (Set ($#k2_csspace :::"seq_id"::: ) (Set (Var "x"))) "is" ($#v2_comseq_3 :::"absolutely_summable"::: ) ) ")" ) ")" ) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_csspace :::"CZeroseq"::: ) )) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k2_csspace :::"seq_id"::: ) (Set (Var "u")))) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) "holds" (Bool (Set (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_csspace :::"seq_id"::: ) (Set (Var "u")) ")" ) ($#k1_series_1 :::"+"::: ) (Set "(" ($#k2_csspace :::"seq_id"::: ) (Set (Var "v")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k25_valued_1 :::"(#)"::: ) (Set "(" ($#k2_csspace :::"seq_id"::: ) (Set (Var "u")) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k31_valued_1 :::"-"::: ) (Set "(" ($#k2_csspace :::"seq_id"::: ) (Set (Var "u")) ")" ))) & (Bool (Set ($#k2_csspace :::"seq_id"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "u")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k31_valued_1 :::"-"::: ) (Set "(" ($#k2_csspace :::"seq_id"::: ) (Set (Var "u")) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) "holds" (Bool (Set (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_csspace :::"seq_id"::: ) (Set (Var "u")) ")" ) ($#k46_valued_1 :::"-"::: ) (Set "(" ($#k2_csspace :::"seq_id"::: ) (Set (Var "v")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) "holds" (Bool (Set ($#k2_csspace :::"seq_id"::: ) (Set (Var "v"))) "is" ($#v2_comseq_3 :::"absolutely_summable"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "v")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" ($#k2_csspace :::"seq_id"::: ) (Set (Var "v")) ")" ) ($#k55_valued_1 :::".|"::: ) ))) ")" ) ")" ) ; theorem :: CSSPACE3:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Complex":::) "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_csspace3 :::"Complex_l1_Space"::: ) ))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k3_csspace3 :::"Complex_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 "p")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "p")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ))) ")" ))) ; registration cluster (Set ($#k3_csspace3 :::"Complex_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"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_clvect_1 :::"vector-distributive"::: ) ($#v3_clvect_1 :::"scalar-distributive"::: ) ($#v4_clvect_1 :::"scalar-associative"::: ) ($#v5_clvect_1 :::"scalar-unital"::: ) ($#v8_clvect_1 :::"ComplexNormSpace-like"::: ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_clvect_1 :::"CNORMSTR"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"dist"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Real":::) equals :: CSSPACE3:def 4 (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" "x" ($#k5_algstr_0 :::"-"::: ) "y" ")" ) ($#k1_normsp_0 :::".||"::: ) ); end; :: deftheorem defines :::"dist"::: CSSPACE3:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_clvect_1 :::"CNORMSTR"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_csspace3 :::"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 "CNRM" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_clvect_1 :::"CNORMSTR"::: ) ; let "seqt" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "CNRM")); attr "seqt" is :::"CCauchy"::: means :: CSSPACE3: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_csspace3 :::"dist"::: ) "(" (Set "(" "seqt" ($#k3_funct_2 :::"."::: ) (Set (Var "n1")) ")" ) "," (Set "(" "seqt" ($#k3_funct_2 :::"."::: ) (Set (Var "m1")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1")))))); end; :: deftheorem defines :::"CCauchy"::: CSSPACE3:def 5 : (Bool "for" (Set (Var "CNRM")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_clvect_1 :::"CNORMSTR"::: ) (Bool "for" (Set (Var "seqt")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "CNRM")) "holds" (Bool "(" (Bool (Set (Var "seqt")) "is" ($#v1_csspace3 :::"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_csspace3 :::"dist"::: ) "(" (Set "(" (Set (Var "seqt")) ($#k3_funct_2 :::"."::: ) (Set (Var "n1")) ")" ) "," (Set "(" (Set (Var "seqt")) ($#k3_funct_2 :::"."::: ) (Set (Var "m1")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1")))))) ")" ))); notationlet "CNRM" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_clvect_1 :::"CNORMSTR"::: ) ; let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "CNRM")); synonym :::"Cauchy_sequence_by_Norm"::: "seq" for :::"CCauchy"::: ; end; theorem :: CSSPACE3:8 (Bool "for" (Set (Var "NRM")) "being" ($#l2_clvect_1 :::"ComplexNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "NRM")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_csspace3 :::"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")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k3_funct_2 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))) ; theorem :: CSSPACE3:9 (Bool "for" (Set (Var "vseq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k3_csspace3 :::"Complex_l1_Space"::: ) ) "st" (Bool (Bool (Set (Var "vseq")) "is" ($#v1_csspace3 :::"Cauchy_sequence_by_Norm"::: ) )) "holds" (Bool (Set (Var "vseq")) "is" ($#v9_clvect_1 :::"convergent"::: ) )) ;