次回からは，が区間[0,1]で連続のとき の証明を進めます． 証明の流れは，区間を等分して，積分の平均値定理，絶対値との順序交換，リーマン和の極限といったものです． 本格的な積分の証明には，"Multivariate/realanalysis.ml"あたりが入用ですが，今回程…

今回は，床関数の性質の一つです．定義に近い形で進めるなら g `!x m. floor (x + &m) = floor x + &m`;; e(REPEAT GEN_TAC);; e(MAP_EVERY ASSUME_TAC [SPEC`x + &m`FLOOR; SPEC`x:real`FLOOR]);; e(SUBGOAL_TAC""`integer (floor x + &m)`[ASM_SIMP_TAC[IN…