:: HEINE  semantic presentation begin  
















theorem :: HEINE:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#m1_topmetr :::"SubSpace"::: )   "of" (Set   ($#k8_metric_1 :::"RealSpace"::: )  )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) "holds"  (Bool (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "y")) ")" )))))) ; 
 



theorem :: HEINE:2 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is" bbbadV5_VALUED_0()) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "seq")))  ($#r1_tarski :::"c="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 definitionlet "seq" be   ($#m1_subset_1 :::"Real_Sequence":::); let "k" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func "k" :::"to_power"::: "seq" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: HEINE:def 1 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set "k"  ($#k4_power :::"to_power"::: )  (Set  "(" "seq"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )))); end; 






:: deftheorem    defines :::"to_power"::: HEINE:def 1 :  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k1_heine :::"to_power"::: )  (Set (Var "seq")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k4_power :::"to_power"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" )))); 
 
theorem :: HEINE:3 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_limfunc1 :::"divergent_to+infty"::: )  )) "holds"  (Bool (Set (Num 2)  ($#k1_heine :::"to_power"::: )  (Set (Var "seq"))) "is"   ($#v1_limfunc1 :::"divergent_to+infty"::: )  )) ; 
 
theorem :: HEINE:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is"   ($#v1_compts_1 :::"compact"::: )  )) ;