:: UNIFORM1 semantic presentation begin theorem :: UNIFORM1:1 (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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ))) ; definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "f" is :::"uniformly_continuous"::: means :: UNIFORM1:def 1 (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 "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "u1")) "," (Set (Var "u2")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set "(" "f" ($#k10_funct_2 :::"/."::: ) (Set (Var "u1")) ")" ) "," (Set "(" "f" ($#k10_funct_2 :::"/."::: ) (Set (Var "u2")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ) ")" ))); end; :: deftheorem defines :::"uniformly_continuous"::: UNIFORM1:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_uniform1 :::"uniformly_continuous"::: ) ) "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 "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "u1")) "," (Set (Var "u2")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set "(" (Set (Var "f")) ($#k10_funct_2 :::"/."::: ) (Set (Var "u1")) ")" ) "," (Set "(" (Set (Var "f")) ($#k10_funct_2 :::"/."::: ) (Set (Var "u2")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ) ")" ))) ")" ))); theorem :: UNIFORM1:2 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P"))) "is" ($#v3_pre_topc :::"open"::: ) ))))))) ; theorem :: UNIFORM1:3 (Bool "for" (Set (Var "N")) "," (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "u"))))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "w")))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "u")) "," (Set (Var "w")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "u1")) "," (Set (Var "w1")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) ")" ) ")" )))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: UNIFORM1:4 (Bool "for" (Set (Var "N")) "," (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "u"))))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "w")))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "u")) "," (Set (Var "w")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "u1")) "," (Set (Var "w1")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) ")" ) ")" ))))))) ; theorem :: UNIFORM1:5 (Bool "for" (Set (Var "N")) "," (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "M")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "f")) "is" ($#v1_uniform1 :::"uniformly_continuous"::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) )))) ; theorem :: UNIFORM1:6 (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N")) ")" ) "st" (Bool (Bool (Set (Var "G")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N")) ")" )) & (Bool (Set (Var "G")) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N"))) "is" ($#v1_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "w1")) "," (Set (Var "w2")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "ex" (Set (Var "Ga")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N")) ")" ) "st" (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set (Var "Ga"))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set (Var "Ga"))) & (Bool (Set (Var "Ga")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" )) ")" ) ")" )))) ; begin theorem :: UNIFORM1:7 (Bool "for" (Set (Var "N")) "," (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "M")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r1_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "N"))) "is" ($#v1_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v1_uniform1 :::"uniformly_continuous"::: ) )))) ; theorem :: UNIFORM1:8 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_topmetr :::"Closed-Interval-MSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "," (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "f")) "is" ($#v1_uniform1 :::"uniformly_continuous"::: ) )))) ; theorem :: UNIFORM1:9 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_topmetr :::"Closed-Interval-MSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "," (Set "(" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ($#k1_topmetr :::"|"::: ) (Set (Var "Q")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "f")) "is" ($#v1_uniform1 :::"uniformly_continuous"::: ) )))))) ; begin theorem :: UNIFORM1:10 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "g")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_topmetr :::"Closed-Interval-MSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "," (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" )))) ; theorem :: UNIFORM1:11 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "r")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "r")) ")" )))) ; theorem :: UNIFORM1:12 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "r1")) ($#k9_real_1 :::"-"::: ) (Set (Var "r2")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "s2")) ($#k9_real_1 :::"-"::: ) (Set (Var "s1"))))) ; definitionlet "IT" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); attr "IT" is :::"decreasing"::: means :: UNIFORM1:def 2 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "IT")) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "IT")) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))); end; :: deftheorem defines :::"decreasing"::: UNIFORM1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_uniform1 :::"decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "IT")))) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "IT")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))) ")" )); theorem :: UNIFORM1:13 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Num 5) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ))) & (Bool (Set (Var "h")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q"))))) "holds" (Bool (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))))) ")" ) ")" )))))) ; theorem :: UNIFORM1:14 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Num 5) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ))) & (Bool (Set (Var "h")) "is" ($#v2_uniform1 :::"decreasing"::: ) ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q"))))) "holds" (Bool (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))))) ")" ) ")" )))))) ;