:: METRIC_6 semantic presentation begin theorem :: METRIC_6:1 (Bool "for" (Set (Var "X")) "being" ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; theorem :: METRIC_6:2 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "G")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))))) ; theorem :: METRIC_6:3 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set (Var "G")) "is" ($#v3_metric_1 :::"discerning"::: ) ) & (Bool (Set (Var "G")) "is" ($#v4_metric_1 :::"symmetric"::: ) ) & (Bool (Set (Var "G")) "is" ($#v5_metric_1 :::"triangle"::: ) ) ")" ) ")" ))) ; theorem :: METRIC_6:4 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool "(" (Bool (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" (Set (Var "X"))) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" (Set (Var "X"))) "is" ($#v3_metric_1 :::"discerning"::: ) ) & (Bool (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" (Set (Var "X"))) "is" ($#v4_metric_1 :::"symmetric"::: ) ) & (Bool (Set "the" ($#u1_metric_1 :::"distance"::: ) "of" (Set (Var "X"))) "is" ($#v5_metric_1 :::"triangle"::: ) ) ")" )) ; theorem :: METRIC_6:5 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_metric_1 :::"Reflexive"::: ) ) & (Bool (Set (Var "G")) "is" ($#v3_metric_1 :::"discerning"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "G")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ))) ")" ) ")" ) ")" ))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"bounded_metric"::: "(" "A" "," "G" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "A" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_6:def 1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "G" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" "G" ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" )))); end; :: deftheorem defines :::"bounded_metric"::: METRIC_6:def 1 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_metric_6 :::"bounded_metric"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" )) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" )))) ")" ))); theorem :: METRIC_6:6 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "G")) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_metric_6 :::"bounded_metric"::: ) "(" (Set (Var "A")) "," (Set (Var "G")) ")" ) ($#r1_pcomps_1 :::"is_metric_of"::: ) (Set (Var "A"))))) ; theorem :: METRIC_6:7 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "S" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); pred "S" :::"is_convergent_in_metrspace_to"::: "x" means :: METRIC_6:def 2 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set "(" "S" ($#k2_tbsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," "x" ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))); end; :: deftheorem defines :::"is_convergent_in_metrspace_to"::: METRIC_6:def 2 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set "(" (Set (Var "S")) ($#k2_tbsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "V" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); redefine attr "V" is :::"bounded"::: means :: METRIC_6:def 3 (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::)(Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "V" ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) ")" ))); end; :: deftheorem defines :::"bounded"::: METRIC_6:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ) "iff" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::)(Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) ")" ))) ")" ))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "S" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "S" is :::"bounded"::: means :: METRIC_6:def 4 (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::)(Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "S") ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) ")" ))); end; :: deftheorem defines :::"bounded"::: METRIC_6:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_metric_6 :::"bounded"::: ) ) "iff" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::)(Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) ")" ))) ")" ))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "V" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "S" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); pred "V" :::"contains_almost_all_sequence"::: "S" means :: METRIC_6:def 5 (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set "S" ($#k2_tbsp_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) "V"))); end; :: deftheorem defines :::"contains_almost_all_sequence"::: METRIC_6:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r2_metric_6 :::"contains_almost_all_sequence"::: ) (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "S")) ($#k2_tbsp_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Var "V"))))) ")" )))); theorem :: METRIC_6:8 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_metric_6 :::"bounded"::: ) ) "iff" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::)(Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "S")) ($#k2_tbsp_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) ")" ) ")" ))) ")" ))) ; theorem :: METRIC_6:9 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "S")) "is" ($#v2_tbsp_1 :::"convergent"::: ) )))) ; theorem :: METRIC_6:10 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_tbsp_1 :::"convergent"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x")))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "S" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func :::"dist_to_point"::: "(" "S" "," "x" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: METRIC_6:def 6 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set "(" "S" ($#k2_tbsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," "x" ")" ))); end; :: deftheorem defines :::"dist_to_point"::: METRIC_6:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_metric_6 :::"dist_to_point"::: ) "(" (Set (Var "S")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set "(" (Set (Var "S")) ($#k2_tbsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "x")) ")" ))) ")" ))))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "S", "T" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); func :::"sequence_of_dist"::: "(" "S" "," "T" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: METRIC_6:def 7 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set "(" "S" ($#k2_tbsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" "T" ($#k2_tbsp_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ))); end; :: deftheorem defines :::"sequence_of_dist"::: METRIC_6:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_metric_6 :::"sequence_of_dist"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set "(" (Set (Var "S")) ($#k2_tbsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "T")) ($#k2_tbsp_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ))) ")" )))); theorem :: METRIC_6:11 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k1_tbsp_1 :::"lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: METRIC_6:12 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x"))) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_tbsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k1_tbsp_1 :::"lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" )))) ; theorem :: METRIC_6:13 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_tbsp_1 :::"convergent"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x"))) & (Bool (Set ($#k1_tbsp_1 :::"lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))) ; theorem :: METRIC_6:14 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x"))) "iff" (Bool "(" (Bool (Set ($#k2_metric_6 :::"dist_to_point"::: ) "(" (Set (Var "S")) "," (Set (Var "x")) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k2_metric_6 :::"dist_to_point"::: ) "(" (Set (Var "S")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )))) ; theorem :: METRIC_6:15 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x")))) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r2_metric_6 :::"contains_almost_all_sequence"::: ) (Set (Var "S"))))))) ; theorem :: METRIC_6:16 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r2_metric_6 :::"contains_almost_all_sequence"::: ) (Set (Var "S"))) ")" )) "holds" (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "V")) ($#r2_metric_6 :::"contains_almost_all_sequence"::: ) (Set (Var "S"))))))) ; theorem :: METRIC_6:17 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "V")) ($#r2_metric_6 :::"contains_almost_all_sequence"::: ) (Set (Var "S"))) ")" )) "holds" (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x")))))) ; theorem :: METRIC_6:18 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r2_metric_6 :::"contains_almost_all_sequence"::: ) (Set (Var "S")))) ")" )))) ; theorem :: METRIC_6:19 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "V")) ($#r2_metric_6 :::"contains_almost_all_sequence"::: ) (Set (Var "S")))) ")" )))) ; theorem :: METRIC_6:20 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r2_metric_6 :::"contains_almost_all_sequence"::: ) (Set (Var "S"))) ")" ) "iff" (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "V")) ($#r2_metric_6 :::"contains_almost_all_sequence"::: ) (Set (Var "S")))) ")" )))) ; theorem :: METRIC_6:21 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_tbsp_1 :::"convergent"::: ) ) & (Bool (Set (Var "T")) "is" ($#v2_tbsp_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set "(" ($#k1_tbsp_1 :::"lim"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k1_tbsp_1 :::"lim"::: ) (Set (Var "T")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_metric_6 :::"sequence_of_dist"::: ) "(" (Set (Var "S")) "," (Set (Var "T")) ")" ")" ))))) ; theorem :: METRIC_6:22 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x"))) & (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))))) ; theorem :: METRIC_6:23 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v2_tbsp_1 :::"convergent"::: ) ))) ; theorem :: METRIC_6:24 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "," (Set (Var "S1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x"))) & (Bool (Set (Var "S1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S")))) "holds" (Bool (Set (Var "S1")) ($#r1_metric_6 :::"is_convergent_in_metrspace_to"::: ) (Set (Var "x")))))) ; theorem :: METRIC_6:25 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "," (Set (Var "S1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_tbsp_1 :::"Cauchy"::: ) ) & (Bool (Set (Var "S1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "S")))) "holds" (Bool (Set (Var "S1")) "is" ($#v3_tbsp_1 :::"Cauchy"::: ) ))) ; theorem :: METRIC_6:26 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v3_tbsp_1 :::"Cauchy"::: ) ))) ; theorem :: METRIC_6:27 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_tbsp_1 :::"convergent"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v1_metric_6 :::"bounded"::: ) ))) ; theorem :: METRIC_6:28 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_tbsp_1 :::"Cauchy"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v1_metric_6 :::"bounded"::: ) ))) ; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")) -> ($#v2_tbsp_1 :::"convergent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")) ($#v3_tbsp_1 :::"Cauchy"::: ) -> ($#v1_metric_6 :::"bounded"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")) ($#v2_tbsp_1 :::"convergent"::: ) ($#v3_tbsp_1 :::"Cauchy"::: ) ($#v1_metric_6 :::"bounded"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: METRIC_6:29 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "V")) "being" ($#v6_tbsp_1 :::"bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) ")" ))))) ;