proposition: Lemma wlength_sigma_finite (f : R -> R) : sigma_finite [set: (ocitv_type R)] (wlength f).
proof: Proof. exists (fun k => `](- k%:R), k%:R]%classic). apply/esym; rewrite -subTset => /= x _ /=. exists `|(floor `|x|%R + 1)%R|%N; rewrite //= in_itv/=. rewrite !natr_absz intr_norm intrD -RfloorE. suff: `|x| < `|Rfloor `|x| + 1| by rewrite ltr_norml => /andP[-> /ltW->]. rewrite [ltRHS]ger0_norm//. by rewrite (le_lt_trans _ (lt_succ_Rfloor _))// ?ler_norm. by rewrite addr_ge0// -Rfloor0 le_Rfloor. move=> k; split => //; rewrite wlength_itv /= -EFinB. by case: ifP; rewrite ltey. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) HB(structures) mathcomp.classical(mathcomp_extra boolp classical_sets) mathcomp.classical(functions fsbigop cardinality) reals ereal signed topology numfun normedtype sequences esum real_interval measure realfun