proposition: Lemma sub_dominatedr (T : Type) (K : numDomainType) (V : pseudoMetricNormedZmodType K) (h : T -> V) (k : K) (f g : T -> V) (F : set_system T) (FF : Filter F) : (\forall x \near F, `|f x| <= `|g x|) -> dominated_by h k g F -> dominated_by h k f F.
proof: Proof. by move=> le_fg; apply: filterS2 le_fg => x; apply: le_trans. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule