proposition: Lemma is_RInt_gen_scal {Fa Fb : (R -> Prop) -> Prop} {FFa : Filter Fa} {FFb : Filter Fb} (f : R -> V) (k : R) (l : V) : is_RInt_gen f Fa Fb l -> is_RInt_gen (fun y => scal k (f y)) Fa Fb (scal k l).
proof: Proof. intros H P HP. move /filterlim_scal_r in HP. specialize (H _ HP). unfold filtermapi in H |- *. apply: filter_imp H. move => [a b] /= [y [Hy1 Hy2]]. exists (scal k y). apply: conj Hy2. exact: is_RInt_scal. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis