proposition: Lemma is_domin_linear {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> W) (g : T -> U) (l : U -> V) : is_linear l -> is_domin F f g -> is_domin F f (fun t => l (g t)).
proof: Proof. intros [_ _ [M [Hm Hn]]] H eps. assert (He : 0 < eps / M). apply Rdiv_lt_0_compat with (2 := Hm). apply cond_pos. specialize (H (mkposreal _ He)). move: H ; apply filter_imp => /= x Hx. apply Rle_trans with (1 := Hn _). evar_last. apply Rmult_le_compat_l with (2 := Hx). now apply Rlt_le. field. now apply Rgt_not_eq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv