2011-12-10から1日間の記事一覧
極限値が実数aの場合です. let my_thm02 = prove (`!x a. x tends_num_real a ==> (\n. sum(1..n)x / &n) tends_num_real a`, let lemma01,lemma02,lemma03 = CONV_RULE (REWRITE_CONV[SEQ; REAL_SUB_RZERO; SUM_SUB_NUMSEG; SUM_CONST_NUMSEG; ARITH_RULE`…