proposition: Lemma is_RInt_fct_extend_pair (f : R -> U * V) (a b : R) lu lv : is_RInt (fun t => fst (f t)) a b lu -> is_RInt (fun t => snd (f t)) a b lv -> is_RInt f a b (lu,lv).
proof: Proof. move => H1 H2. apply filterlim_locally => eps. generalize (proj1 (filterlim_locally _ _) H1 eps) => {H1} ; intros [d1 H1]. generalize (proj1 (filterlim_locally _ _) H2 eps) => {H2} ; intros [d2 H2]. simpl in H1, H2. exists (mkposreal _ (Rmin_stable_in_posreal d1 d2)) => /= ptd Hstep Hptd. rewrite (Riemann_sum_pair f ptd) ; simpl. split. apply H1 => //. by apply Rlt_le_trans with (2 := Rmin_l d1 d2). apply H2 => //. by apply Rlt_le_trans with (2 := Rmin_r d1 d2). Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy