proposition: Lemma __deprecated__ler_cvg_map (R : realFieldType) (T : topologicalType) (F : set_system T) (FF : ProperFilter F) (f g : T -> R) : (\forall x \near F, f x <= g x) -> cvg (f @ F) -> cvg (g @ F) -> lim (f @ F) <= lim (g @ F).
proof: Proof. by move=> ? ? ?; rewrite ler_lim. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms