2011-12-15から1日間の記事一覧
今回は Example(11)のmy_thm02の応用として を証明します.まずは g`!x a. (\n. x n - x (n-1) ) tends_num_real a ==> (\n. (x n - x 0) / &n ) tends_num_real a`;; e(REPEAT STRIP_TAC THEN SIMP_TAC[SEQ] THEN REPEAT STRIP_TAC);; let lemma02 = SPECL[…
今回は Example(11)のmy_thm02の応用として を証明します.まずは g`!x a. (\n. x n - x (n-1) ) tends_num_real a ==> (\n. (x n - x 0) / &n ) tends_num_real a`;; e(REPEAT STRIP_TAC THEN SIMP_TAC[SEQ] THEN REPEAT STRIP_TAC);; let lemma02 = SPECL[…