2012-01-29から1日間の記事一覧
まずは,区間の等分です.単調列での分割を帰納法で示した後,を固定した列により等分します. needs "Library/transc.ml";; g `!n f x i. (!j k. j <= k /\ k <= n ==> x j <= x k) /\ (!k. 1 <= k /\ k <= n ==> defint (x (k -1),x k) f (i k)) ==> defin…
まずは,区間の等分です.単調列での分割を帰納法で示した後,を固定した列により等分します. needs "Library/transc.ml";; g `!n f x i. (!j k. j <= k /\ k <= n ==> x j <= x k) /\ (!k. 1 <= k /\ k <= n ==> defint (x (k -1),x k) f (i k)) ==> defin…