2012-02-12から1日間の記事一覧
次回からは,一変数級関数上の数列についてのJensenの不等式を証明します.
ある論文で紹介されていた排中律によるトリック?です. # g `!p:A->bool. ?x:A. (p x ==> !y. p y)`;; val it : goalstack = 1 subgoal (1 total) `!p. ?x. p x ==> (!y. p y)` # e(GEN_TAC);; val it : goalstack = 1 subgoal (1 total) `?x. p x ==> (!y.…