proposition: Lemma ex_RInt_gen_ext {Fa Fb : (R -> Prop) -> Prop} {FFa : Filter Fa} {FFb : Filter Fb} (f g : R -> V) : filter_prod Fa Fb (fun ab => forall x, Rmin (fst ab) (snd ab) < x < Rmax (fst ab) (snd ab) -> f x = g x) -> ex_RInt_gen f Fa Fb -> ex_RInt_gen g Fa Fb.
proof: Proof. move => Heq. case => I HI. exists I. exact: (is_RInt_gen_ext f g). Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis