:: WEIERSTR semantic presentation begin theorem :: WEIERSTR:1 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x1")) "," (Set (Var "r1")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x2")) "," (Set (Var "r2")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))))) ; theorem :: WEIERSTR:2 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_topmetr :::"being_ball-family"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_topmetr :::"being_ball-family"::: ) ) & (Bool "ex" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "G")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ))))) ")" )) ")" )))))) ; theorem :: WEIERSTR:3 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_topmetr :::"being_ball-family"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )))))) ; theorem :: WEIERSTR:4 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k6_funct_2 :::"""::: ) (Set (Var "B"))) "is" ($#v1_tops_2 :::"open"::: ) )))) ; theorem :: WEIERSTR:5 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "Q")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k6_funct_2 :::"""::: ) (Set (Var "Q"))) "is" ($#v1_finset_1 :::"finite"::: ) )))) ; theorem :: WEIERSTR:6 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_funct_2 :::".:"::: ) (Set (Var "P"))) "is" ($#v1_finset_1 :::"finite"::: ) )))) ; theorem :: WEIERSTR:7 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k6_funct_2 :::"""::: ) (Set (Var "F")))) & (Bool (Set (Var "B")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Var "P"))) & (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")))) & (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )))))) ; begin theorem :: WEIERSTR:8 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) "is" ($#v2_compts_1 :::"compact"::: ) )))) ; theorem :: WEIERSTR:9 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) "is" ($#v2_compts_1 :::"compact"::: ) )))) ; theorem :: WEIERSTR:10 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) "is" ($#v2_compts_1 :::"compact"::: ) ))) ; definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ); func :::"[#]"::: "P" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: WEIERSTR:def 1 "P"; end; :: deftheorem defines :::"[#]"::: WEIERSTR:def 1 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set ($#k1_weierstr :::"[#]"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "P")))); theorem :: WEIERSTR:11 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k1_weierstr :::"[#]"::: ) (Set (Var "P"))) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) )) ; theorem :: WEIERSTR:12 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k1_weierstr :::"[#]"::: ) (Set (Var "P"))) "is" ($#v2_rcomp_1 :::"closed"::: ) )) ; theorem :: WEIERSTR:13 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k1_weierstr :::"[#]"::: ) (Set (Var "P"))) "is" ($#v1_rcomp_1 :::"compact"::: ) )) ; definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ); func :::"upper_bound"::: "P" -> ($#m1_subset_1 :::"Real":::) equals :: WEIERSTR:def 2 (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_weierstr :::"[#]"::: ) "P" ")" )); func :::"lower_bound"::: "P" -> ($#m1_subset_1 :::"Real":::) equals :: WEIERSTR:def 3 (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_weierstr :::"[#]"::: ) "P" ")" )); end; :: deftheorem defines :::"upper_bound"::: WEIERSTR:def 2 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set ($#k2_weierstr :::"upper_bound"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_weierstr :::"[#]"::: ) (Set (Var "P")) ")" )))); :: deftheorem defines :::"lower_bound"::: WEIERSTR:def 3 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set ($#k3_weierstr :::"lower_bound"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_weierstr :::"[#]"::: ) (Set (Var "P")) ")" )))); theorem :: WEIERSTR:14 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ))) ")" ))))) ; theorem :: WEIERSTR:15 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ))) ")" ))))) ; begin definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); func :::"dist"::: "x" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) means :: WEIERSTR:def 4 (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "M" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "y")) "," "x" ")" ))); end; :: deftheorem defines :::"dist"::: WEIERSTR:def 4 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_weierstr :::"dist"::: ) (Set (Var "x")))) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ))) ")" )))); theorem :: WEIERSTR:16 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k4_weierstr :::"dist"::: ) (Set (Var "x"))) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: WEIERSTR:17 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "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 ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ))) ")" ))))) ; theorem :: WEIERSTR:18 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "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 ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool "(" (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ))) ")" ))))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Const "M")) ")" ); func :::"dist_max"::: "P" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) means :: WEIERSTR:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "M" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k7_relset_1 :::".:"::: ) "P" ")" )))); func :::"dist_min"::: "P" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) "M" ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) means :: WEIERSTR:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "M" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k7_relset_1 :::".:"::: ) "P" ")" )))); end; :: deftheorem defines :::"dist_max"::: WEIERSTR:def 5 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" )))) ")" )))); :: deftheorem defines :::"dist_min"::: WEIERSTR:def 6 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "x")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" )))) ")" )))); theorem :: WEIERSTR:19 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (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")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "p2")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ))) & (Bool (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "p2")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) ")" )))) ; theorem :: WEIERSTR:20 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (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 ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "p1")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "p2")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))))) ; theorem :: WEIERSTR:21 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (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 ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p1")))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p2"))))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "x2")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )))))) ; theorem :: WEIERSTR:22 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (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 ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "p1")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k4_weierstr :::"dist"::: ) (Set (Var "p2")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))))) ; theorem :: WEIERSTR:23 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (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 ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p1")))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p2"))))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "x2")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )))))) ; theorem :: WEIERSTR:24 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k5_weierstr :::"dist_max"::: ) (Set (Var "X"))) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: WEIERSTR:25 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")) ")" ))) ")" )))) ; theorem :: WEIERSTR:26 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool "(" (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")) ")" ))) ")" )))) ; theorem :: WEIERSTR:27 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool (Set ($#k6_weierstr :::"dist_min"::: ) (Set (Var "X"))) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: WEIERSTR:28 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")) ")" ))) ")" )))) ; theorem :: WEIERSTR:29 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool "(" (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")) ")" ))) ")" )))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); let "P", "Q" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Const "M")) ")" ); func :::"min_dist_min"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Real":::) equals :: WEIERSTR:def 7 (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k6_weierstr :::"dist_min"::: ) "P" ")" ) ($#k7_relset_1 :::".:"::: ) "Q" ")" )); func :::"max_dist_min"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Real":::) equals :: WEIERSTR:def 8 (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k6_weierstr :::"dist_min"::: ) "P" ")" ) ($#k7_relset_1 :::".:"::: ) "Q" ")" )); func :::"min_dist_max"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Real":::) equals :: WEIERSTR:def 9 (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k5_weierstr :::"dist_max"::: ) "P" ")" ) ($#k7_relset_1 :::".:"::: ) "Q" ")" )); func :::"max_dist_max"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Real":::) equals :: WEIERSTR:def 10 (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k5_weierstr :::"dist_max"::: ) "P" ")" ) ($#k7_relset_1 :::".:"::: ) "Q" ")" )); end; :: deftheorem defines :::"min_dist_min"::: WEIERSTR:def 7 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool (Set ($#k7_weierstr :::"min_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")) ")" ))))); :: deftheorem defines :::"max_dist_min"::: WEIERSTR:def 8 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool (Set ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k6_weierstr :::"dist_min"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")) ")" ))))); :: deftheorem defines :::"min_dist_max"::: WEIERSTR:def 9 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool (Set ($#k9_weierstr :::"min_dist_max"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_weierstr :::"lower_bound"::: ) (Set "(" (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")) ")" ))))); :: deftheorem defines :::"max_dist_max"::: WEIERSTR:def 10 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "holds" (Bool (Set ($#k10_weierstr :::"max_dist_max"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_weierstr :::"upper_bound"::: ) (Set "(" (Set "(" ($#k5_weierstr :::"dist_max"::: ) (Set (Var "P")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")) ")" ))))); theorem :: WEIERSTR:30 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_weierstr :::"min_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) ")" )))) ; theorem :: WEIERSTR:31 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_weierstr :::"min_dist_max"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) ")" )))) ; theorem :: WEIERSTR:32 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_weierstr :::"max_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) ")" )))) ; theorem :: WEIERSTR:33 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_weierstr :::"max_dist_max"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) ")" )))) ; theorem :: WEIERSTR:34 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_compts_1 :::"compact"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_compts_1 :::"compact"::: ) )) "holds" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool "(" (Bool (Set ($#k7_weierstr :::"min_dist_min"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" )) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_weierstr :::"max_dist_max"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) ")" )))) ;