proposition: Lemma sub_dominatedl (T : Type) (K : numDomainType) (V W : pseudoMetricNormedZmodType K) (h : T -> V) (k : K) (F G : set_system T) : F `=>` G -> (@dominated_by T K V W h k)^~ G `<=` (dominated_by h k)^~ F.
proof: Proof. by move=> FG f; exact: FG. 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