proposition: Lemma sub_boundedl (T : Type) (K : numFieldType) (V : pseudoMetricNormedZmodType K) (f g : T -> V) (F : set_system T) (FF : Filter F) : (\forall x \near F, `|f x| <= `|g x|) -> bounded_near g F -> bounded_near f F.
proof: Proof. move=> le_fg; rewrite /bounded_near; apply: filterS => M. by 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