2011-12-01から1日間の記事一覧
今回は,連続関数の性質です.まず,f:real->realがx:realにおいて連続であることは,中置き演算子 cont(locally continuous) により,f contl xと表され,thmとしては # REWRITE_CONV[contl]`f contl x`;; val it : thm = |- f contl x ( (\h. f (x + h) ) …
今回は,連続関数の性質です.まず,f:real->realがx:realにおいて連続であることは,中置き演算子 cont(locally continuous) により,f contl xと表され,thmとしては # REWRITE_CONV[contl]`f contl x`;; val it : thm = |- f contl x ( (\h. f (x + h) ) …