2012-02-09から1日間の記事一覧
これで積分の第一平均値定理が通常の形で証明できます. let CONT_ATTAINS3 = prove (`!f:real->real a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?L. (!x. a <= x /\ x <= b ==> L <= f x) /\ (?x1. a <= x1 /\ x1 <= b /\ f x1 = L)) /\ (?…
これで積分の第一平均値定理が通常の形で証明できます. let CONT_ATTAINS3 = prove (`!f:real->real a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?L. (!x. a <= x /\ x <= b ==> L <= f x) /\ (?x1. a <= x1 /\ x1 <= b /\ f x1 = L)) /\ (?…