2011-12-13から1日間の記事一覧
今回は の証明です. let limits_num_pinfinity = define `!x:num->real. limits_num_pinfinity x = !K:real. &0 (?N:num. !n. n>=N ==> K g`!x. limits_num_pinfinity x==>limits_num_pinfinity (\n. (sum(1..n)x)/ &n)`;; e(REWRITE_TAC[limits_num_pinfin…