proposition: Lemma continuous_closedP (S T : topologicalType) (f : S -> T) : continuous f <-> forall A, closed A -> closed (f @^-1` A).
proof: Proof. rewrite continuousP; split=> ctsf ? ?. by rewrite -openC preimage_setC; apply: ctsf; rewrite openC. by rewrite -closedC preimage_setC; apply: ctsf; rewrite closedC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed