proposition: Lemma continuous_is_cvg {T : Type} {V U : topologicalType} [F : set_system T] (FF : Filter F) (f : T -> V) (h : V -> U) : (forall l, f x @[x --> F] --> l -> {for l, continuous h}) -> cvg (f x @[x --> F]) -> cvg ((h \o f) x @[x --> F]).
proof: Proof. move=> ach /cvg_ex[l fxl]; apply/cvg_ex; exists (h l). by apply: continuous_cvg => //; exact: ach. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed