2012-02-08から1日間の記事一覧
落穂ひろい気味ですが,先のthm15から&0 積分の第一平均値定理を得るための補題の証明です. let INTEGRAL_CONST_LE = prove (`!c g a b. a <= b /\ integrable (a,b) g /\ (!x. a <= x /\ x <= b ==> c <= g x) ==> c * (b - a) <= integral (a,b) g`, GEN_…
落穂ひろい気味ですが,先のthm15から&0 積分の第一平均値定理を得るための補題の証明です. let INTEGRAL_CONST_LE = prove (`!c g a b. a <= b /\ integrable (a,b) g /\ (!x. a <= x /\ x <= b ==> c <= g x) ==> c * (b - a) <= integral (a,b) g`, GEN_…