proposition: Lemma total_variation_continuous a b (f : R -> R) : a < b -> {within `[a,b], continuous f} -> BV a b f -> {within `[a,b], continuous (fine \o TV a ^~ f)}.
proof: Proof. move=> ab /(@continuous_within_itvP _ _ _ _ ab) [int [l r]] bdf. apply/continuous_within_itvP; (repeat split) => //. - move=> x /[dup] xab; rewrite in_itv /= => /andP [ax xb]. apply/left_right_continuousP; split. apply: (total_variation_left_continuous _ (ltW xb)) => //. by have /left_right_continuousP [] := int x xab. apply: (total_variation_right_continuous _ xb) => //; first exact: ltW. by have /left_right_continuousP [] := int x xab. - exact: (total_variation_right_continuous _ ab). - exact: (total_variation_left_continuous ab). Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)