■ 前件の導入 # g`a==>b`;; Warning: Free variables in goal: a, b val it : goalstack = 1 subgoal (1 total)`a ==> b`# e(DISCH_THEN(fun t->ALL_TAC));; val it : goalstack = 1 subgoal (1 total)`b` ■ 仮定の導入 # g`a==>b`;; Warning: Free variable…

■ 今更ですが，0 # LE_0;; val it : thm = |- !n. 0 で賄えることに気付きました． # g`!n. sum(0..n)(\k. &k)= &n*( &n+ &1)/ &2`;; val it : goalstack = 1 subgoal (1 total)`!n. sum (0..n) (\k. &k) = &n * (&n + &1) / &2`# e INDUCT_TAC;; val it : g…

IMAGEの用例です． # IMAGE;; val it : thm = |- !s f. IMAGE f s = {y | ?x. x IN s /\ y = f x} # g`y IN (IMAGE (\x. x+ &1) {x| &0 &1 &1 # e (REWRITE_TAC[IMAGE;IN_ELIM_THM]);; val it : goalstack = 1 subgoal (1 total)`(?x. &0 &1 # e EQ_TAC;; va…

今回は微分法です． # diffl;; val it : thm = |- !f x l. (f diffl l) x ((\h. (f (x + h) - f x) / h) tends_real_real l) (&0) イプシロンデルタでは # REWRITE_RULE[LIM; REAL_SUB_RZERO] diffl;; val it : thm = |- !f x l. (f diffl l) x (!e. &0 ==> …