proposition: Lemma cvg_fmap {T: topologicalType} {U : topologicalType} (F : set_system T) x (f : T -> U) : {for x, continuous f} -> F --> x -> f @ F --> f x.
proof: Proof. by move=> cf fx P /cf /fx. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed