:: METRIC_2 semantic presentation begin definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); pred "x" :::"tolerates"::: "y" means :: METRIC_2:def 1 (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" "x" "," "y" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"tolerates"::: METRIC_2:def 1 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_metric_2 :::"tolerates"::: ) (Set (Var "y"))) "iff" (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))); definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); :: original: :::"tolerates"::: redefine pred "x" :::"tolerates"::: "y"; reflexivity (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")) "holds" (Bool ((Set (Const "M")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_metric_1 :::"symmetric"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); :: original: :::"tolerates"::: redefine pred "x" :::"tolerates"::: "y"; symmetry (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")) "st" (Bool (Bool ((Set (Const "M")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "M")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); func "x" :::"-neighbour"::: -> ($#m1_subset_1 :::"Subset":::) "of" "M" equals :: METRIC_2:def 2 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" "M" : (Bool "x" ($#r1_metric_2 :::"tolerates"::: ) (Set (Var "y"))) "}" ; end; :: deftheorem defines :::"-neighbour"::: METRIC_2:def 2 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) : (Bool (Set (Var "x")) ($#r1_metric_2 :::"tolerates"::: ) (Set (Var "y"))) "}" ))); definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; mode :::"equivalence_class"::: "of" "M" -> ($#m1_subset_1 :::"Subset":::) "of" "M" means :: METRIC_2:def 3 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ))); end; :: deftheorem defines :::"equivalence_class"::: METRIC_2:def 3 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_metric_2 :::"equivalence_class"::: ) "of" (Set (Var "M"))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ))) ")" ))); theorem :: METRIC_2:1 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) ($#r3_metric_2 :::"tolerates"::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r3_metric_2 :::"tolerates"::: ) (Set (Var "z")))) "holds" (Bool (Set (Var "x")) ($#r3_metric_2 :::"tolerates"::: ) (Set (Var "z"))))) ; theorem :: METRIC_2:2 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) )) "iff" (Bool (Set (Var "y")) ($#r3_metric_2 :::"tolerates"::: ) (Set (Var "x"))) ")" ))) ; theorem :: METRIC_2:3 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ))) "holds" (Bool (Set (Var "p")) ($#r3_metric_2 :::"tolerates"::: ) (Set (Var "q"))))) ; theorem :: METRIC_2:4 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) )))) ; theorem :: METRIC_2:5 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "y")) ($#k1_metric_2 :::"-neighbour"::: ) ))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) )))) ; theorem :: METRIC_2:6 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) )) & (Bool (Set (Var "x")) ($#r3_metric_2 :::"tolerates"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "y")) ($#k1_metric_2 :::"-neighbour"::: ) )))) ; theorem :: METRIC_2:7 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_metric_2 :::"-neighbour"::: ) )))) ; theorem :: METRIC_2:8 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_metric_2 :::"-neighbour"::: ) )) "iff" (Bool (Set (Var "x")) ($#r3_metric_2 :::"tolerates"::: ) (Set (Var "y"))) ")" ))) ; theorem :: METRIC_2:9 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "y")) ($#k1_metric_2 :::"-neighbour"::: ) )) "iff" (Bool (Set (Var "x")) ($#r3_metric_2 :::"tolerates"::: ) (Set (Var "y"))) ")" ))) ; registrationlet "M" be ($#l1_metric_1 :::"PseudoMetricSpace":::); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_metric_2 :::"equivalence_class"::: ) "of" "M"; end; theorem :: METRIC_2:10 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: METRIC_2:11 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v7_metric_1 :::"discerning"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_metric_2 :::"tolerates"::: ) (Set (Var "y"))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ))) ; theorem :: METRIC_2:12 (Bool "for" (Set (Var "M")) "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 "M")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) )) "iff" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; theorem :: METRIC_2:13 (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 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: METRIC_2:14 (Bool "for" (Set (Var "M")) "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 "M")) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#m1_metric_2 :::"equivalence_class"::: ) "of" (Set (Var "M"))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; func "M" :::"-neighbour"::: -> ($#m1_hidden :::"set"::: ) equals :: METRIC_2:def 4 "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Subset":::) "of" "M" : (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "}" ; end; :: deftheorem defines :::"-neighbour"::: METRIC_2:def 4 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) : (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "}" )); registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster (Set "M" ($#k2_metric_2 :::"-neighbour"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: METRIC_2:15 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ))) ")" ))) ; theorem :: METRIC_2:16 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "x")) ($#k1_metric_2 :::"-neighbour"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )))) ; theorem :: METRIC_2:17 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )) "iff" (Bool (Set (Var "V")) "is" ($#m1_metric_2 :::"equivalence_class"::: ) "of" (Set (Var "M"))) ")" ))) ; theorem :: METRIC_2: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 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )))) ; theorem :: METRIC_2:19 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))) ; theorem :: METRIC_2:20 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "q2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p1")) "," (Set (Var "q1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p2")) "," (Set (Var "q2")) ")" ))))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "V", "Q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "M")) ($#k2_metric_2 :::"-neighbour"::: ) ); let "v" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); pred "V" "," "Q" :::"is_dst"::: "v" means :: METRIC_2:def 5 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "V") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "Q")) "holds" (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) "v")); end; :: deftheorem defines :::"is_dst"::: METRIC_2:def 5 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "v")))) ")" )))); theorem :: METRIC_2:21 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )) ")" )))) ; theorem :: METRIC_2:22 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v")))) "holds" (Bool (Set (Var "Q")) "," (Set (Var "V")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v")))))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "V", "Q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "M")) ($#k2_metric_2 :::"-neighbour"::: ) ); func :::"ev_eq_1"::: "(" "V" "," "Q" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: METRIC_2:def 6 "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "V" "," "Q" ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) "}" ; end; :: deftheorem defines :::"ev_eq_1"::: METRIC_2:def 6 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) "holds" (Bool (Set ($#k3_metric_2 :::"ev_eq_1"::: ) "(" (Set (Var "V")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) "}" ))); theorem :: METRIC_2:23 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_metric_2 :::"ev_eq_1"::: ) "(" (Set (Var "V")) "," (Set (Var "Q")) ")" )) "iff" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) ")" )))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "v" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"ev_eq_2"::: "(" "v" "," "M" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: METRIC_2:def 7 "{" (Set (Var "W")) where W "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "M" ($#k2_metric_2 :::"-neighbour"::: ) ) "st" (Bool "(" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "V")) "," (Set (Var "Q")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) "v") ")" )) "}" ; end; :: deftheorem defines :::"ev_eq_2"::: METRIC_2:def 7 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k4_metric_2 :::"ev_eq_2"::: ) "(" (Set (Var "v")) "," (Set (Var "M")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "W")) where W "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) "st" (Bool "(" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "V")) "," (Set (Var "Q")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) ")" )) "}" ))); theorem :: METRIC_2:24 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set ($#k4_metric_2 :::"ev_eq_2"::: ) "(" (Set (Var "v")) "," (Set (Var "M")) ")" )) "iff" (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) "st" (Bool "(" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "V")) "," (Set (Var "Q")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) ")" )) ")" )))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; func :::"real_in_rel"::: "M" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: METRIC_2:def 8 "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "M" ($#k2_metric_2 :::"-neighbour"::: ) ) "st" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v")))) "}" ; end; :: deftheorem defines :::"real_in_rel"::: METRIC_2:def 8 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k5_metric_2 :::"real_in_rel"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) "st" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v")))) "}" )); theorem :: METRIC_2:25 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k5_metric_2 :::"real_in_rel"::: ) (Set (Var "M")))) "iff" (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) "st" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v")))) ")" ))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; func :::"elem_in_rel_1"::: "M" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) equals :: METRIC_2:def 9 "{" (Set (Var "V")) where V "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "M" ($#k2_metric_2 :::"-neighbour"::: ) ) : (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "M" ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))))) "}" ; end; :: deftheorem defines :::"elem_in_rel_1"::: METRIC_2:def 9 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k6_metric_2 :::"elem_in_rel_1"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "V")) where V "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) : (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))))) "}" )); theorem :: METRIC_2:26 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k6_metric_2 :::"elem_in_rel_1"::: ) (Set (Var "M")))) "iff" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))))) ")" ))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; func :::"elem_in_rel_2"::: "M" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) equals :: METRIC_2:def 10 "{" (Set (Var "Q")) where Q "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "M" ($#k2_metric_2 :::"-neighbour"::: ) ) : (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "M" ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))))) "}" ; end; :: deftheorem defines :::"elem_in_rel_2"::: METRIC_2:def 10 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k7_metric_2 :::"elem_in_rel_2"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "Q")) where Q "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) : (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))))) "}" )); theorem :: METRIC_2:27 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) "holds" (Bool "(" (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k7_metric_2 :::"elem_in_rel_2"::: ) (Set (Var "M")))) "iff" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))))) ")" ))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; func :::"elem_in_rel"::: "M" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: METRIC_2:def 11 "{" (Set (Var "VQ")) where VQ "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "M" ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "VQ")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "V")) "," (Set (Var "Q")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) ")" ))) "}" ; end; :: deftheorem defines :::"elem_in_rel"::: METRIC_2:def 11 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k8_metric_2 :::"elem_in_rel"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "VQ")) where VQ "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) : (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "VQ")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "V")) "," (Set (Var "Q")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) ")" ))) "}" )); theorem :: METRIC_2:28 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "VQ")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "VQ")) ($#r2_hidden :::"in"::: ) (Set ($#k8_metric_2 :::"elem_in_rel"::: ) (Set (Var "M")))) "iff" (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "VQ")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "V")) "," (Set (Var "Q")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) ")" ))) ")" ))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; func :::"set_in_rel"::: "M" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) equals :: METRIC_2:def 12 "{" (Set (Var "VQv")) where VQv "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) : (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "M" ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "VQv")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "V")) "," (Set (Var "Q")) "," (Set (Var "v")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) ")" ))) "}" ; end; :: deftheorem defines :::"set_in_rel"::: METRIC_2:def 12 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool (Set ($#k9_metric_2 :::"set_in_rel"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "VQv")) where VQv "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) : (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "VQv")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "V")) "," (Set (Var "Q")) "," (Set (Var "v")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) ")" ))) "}" )); theorem :: METRIC_2:29 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "VQv")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "VQv")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_2 :::"set_in_rel"::: ) (Set (Var "M")))) "iff" (Bool "ex" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) )(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "VQv")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "V")) "," (Set (Var "Q")) "," (Set (Var "v")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v"))) ")" ))) ")" ))) ; theorem :: METRIC_2:30 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) "holds" (Bool (Set ($#k6_metric_2 :::"elem_in_rel_1"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k7_metric_2 :::"elem_in_rel_2"::: ) (Set (Var "M"))))) ; theorem :: METRIC_2:31 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) "holds" (Bool (Set ($#k9_metric_2 :::"set_in_rel"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_mcart_1 :::"[:"::: ) (Set "(" ($#k6_metric_2 :::"elem_in_rel_1"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k7_metric_2 :::"elem_in_rel_2"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k5_metric_2 :::"real_in_rel"::: ) (Set (Var "M")) ")" ) ($#k9_mcart_1 :::":]"::: ) ))) ; theorem :: METRIC_2:32 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v1"))) & (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v2")))) "holds" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2")))))) ; theorem :: METRIC_2:33 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "V")) "," (Set (Var "Q")) ($#r4_metric_2 :::"is_dst"::: ) (Set (Var "v")))))) ; definitionlet "M" be ($#l1_metric_1 :::"PseudoMetricSpace":::); func :::"nbourdist"::: "M" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: METRIC_2:def 13 (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "M" ($#k2_metric_2 :::"-neighbour"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "V")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))); end; :: deftheorem defines :::"nbourdist"::: METRIC_2:def 13 : (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_metric_2 :::"nbourdist"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "V")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))) ")" ))); theorem :: METRIC_2:34 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k10_metric_2 :::"nbourdist"::: ) (Set (Var "M")) ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "V")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))) ")" ))) ; theorem :: METRIC_2:35 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_metric_2 :::"nbourdist"::: ) (Set (Var "M")) ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "V")) "," (Set (Var "Q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_metric_2 :::"nbourdist"::: ) (Set (Var "M")) ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "Q")) "," (Set (Var "V")) ")" )))) ; theorem :: METRIC_2:36 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "Q")) "," (Set (Var "W")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_metric_2 :::"nbourdist"::: ) (Set (Var "M")) ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k10_metric_2 :::"nbourdist"::: ) (Set (Var "M")) ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "V")) "," (Set (Var "Q")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k10_metric_2 :::"nbourdist"::: ) (Set (Var "M")) ")" ) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "Q")) "," (Set (Var "W")) ")" ")" ))))) ; definitionlet "M" be ($#l1_metric_1 :::"PseudoMetricSpace":::); func :::"Eq_classMetricSpace"::: "M" -> ($#l1_metric_1 :::"MetrSpace":::) equals :: METRIC_2:def 14 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set "(" "M" ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" ($#k10_metric_2 :::"nbourdist"::: ) "M" ")" ) "#)" ); end; :: deftheorem defines :::"Eq_classMetricSpace"::: METRIC_2:def 14 : (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"PseudoMetricSpace":::) "holds" (Bool (Set ($#k11_metric_2 :::"Eq_classMetricSpace"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set "(" (Set (Var "M")) ($#k2_metric_2 :::"-neighbour"::: ) ")" ) "," (Set "(" ($#k10_metric_2 :::"nbourdist"::: ) (Set (Var "M")) ")" ) "#)" ))); registrationlet "M" be ($#l1_metric_1 :::"PseudoMetricSpace":::); cluster (Set ($#k11_metric_2 :::"Eq_classMetricSpace"::: ) "M") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ; end;