proposition: Lemma domin_trans {T} {Ku Kv Kw : AbsRing} {U : NormedModule Ku} {V : NormedModule Kv} {W : NormedModule Kw} : forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> U) (g : T -> V) (h : T -> W), is_domin F f g -> is_domin F g h -> is_domin F f h.
proof: Proof. intros F FF f g h Hfg Hgh eps. apply (filter_imp (fun x => (norm (h x) <= sqrt eps * norm (g x)) /\ (norm (g x) <= sqrt eps * norm (f x)))). intros x [H0 H1]. apply Rle_trans with (1 := H0). rewrite -{2}(sqrt_sqrt eps). rewrite Rmult_assoc. apply Rmult_le_compat_l. by apply sqrt_pos. apply H1. by apply Rlt_le, eps. apply filter_and. by apply (Hgh (mkposreal (sqrt eps) (sqrt_lt_R0 _ (cond_pos eps)))). by apply (Hfg (mkposreal (sqrt eps) (sqrt_lt_R0 _ (cond_pos eps)))). Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy