:: ALI2  semantic presentation begin  


definitionlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "M")) "," (Set (Const "M")); attr "f" is  :::"contraction":::  means :: ALI2:def 1 (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "L"))) & (Bool (Set (Var "L"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" "M" "holds"  (Bool (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "L"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_metric_1 :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )))  ")" )  ")" )); end; 





:: deftheorem    defines :::"contraction"::: ALI2:def 1 :  (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 "M")) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_ali2 :::"contraction"::: )  ) "iff" (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "L"))) & (Bool (Set (Var "L"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds"  (Bool (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "L"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_metric_1 :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )))  ")" )  ")" ))  ")" ))); 
 registrationlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV1_FUNCT_1() bbbadV1_PARTFUN1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "M")) bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "M") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "M"))   ($#v1_ali2 :::"contraction"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "M") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "M"))))); 
end; definitionlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::); mode Contraction of "M" is   ($#v1_ali2 :::"contraction"::: )    ($#m1_subset_1 :::"Function":::) "of" "M" "," "M"; end; 
theorem :: ALI2:1 (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 :::"Contraction":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M"))) "is"   ($#v1_compts_1 :::"compact"::: )  )) "holds"  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))  ")" )  ")" )))) ;