proposition: Lemma filterdiff_ext_lin {F} {FF : Filter F} (f : U -> V) (l1 l2 : U -> V) : filterdiff f F l1 -> (forall y, l1 y = l2 y) -> filterdiff f F l2.
proof: Proof. intros [Hl1 Hf1] Hl ; split => [ | x Hx eps]. + split. - intros x y ; rewrite -!Hl. by apply linear_plus. - intros k x ; rewrite -!Hl. by apply linear_scal. - destruct (linear_norm _ Hl1) as [M Hm]. exists M ; split. by apply Hm. move => x ; now rewrite -Hl. + move: (Hf1 x Hx eps). apply filter_imp => y. by rewrite !Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv