proposition: Lemma closed_comp {T U : topologicalType} (f : T -> U) (D : set U) : {in ~` f @^-1` D, continuous f} -> closed D -> closed (f @^-1` D).
proof: Proof. rewrite !closedE=> f_continuous D_cl x /= xDf. apply: D_cl; apply: contra_not xDf => fxD. have NDfx : ~ D (f x). by move: fxD; rewrite -nbhs_nearE nbhsE => - [A [? ?]]; apply. by apply: f_continuous fxD; rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed