proposition: Lemma continuous_cvg {T : Type} {V U : topologicalType} (F : set_system T) (FF : Filter F) (f : T -> V) (h : V -> U) (a : V) : {for a, continuous h} -> f @ F --> a -> (h \o f) @ F --> h a.
proof: Proof. move=> h_continuous fa fb; apply: (cvg_trans _ h_continuous). exact: (@cvg_comp _ _ _ _ h _ _ _ fa). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed