proposition: Lemma is_RInt_gen_ext {Fa Fb : (R -> Prop) -> Prop} {FFa : Filter Fa} {FFb : Filter Fb} (f g : R -> V) (l : V) : filter_prod Fa Fb (fun ab => forall x, Rmin (fst ab) (snd ab) < x < Rmax (fst ab) (snd ab) -> f x = g x) -> is_RInt_gen f Fa Fb l -> is_RInt_gen g Fa Fb l.
proof: Proof. intros Heq. apply: filterlimi_ext_loc. apply: filter_imp Heq. intros [a b] Heq y. split. now apply is_RInt_ext. apply is_RInt_ext. intros x Hx. now apply sym_eq, Heq. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis