proposition: Lemma open_comp {T U : topologicalType} (f : T -> U) (D : set U) : {in f @^-1` D, continuous f} -> open D -> open (f @^-1` D).
proof: Proof. rewrite !openE => fcont Dop x /= Dfx. by apply: fcont; [rewrite inE|apply: Dop]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed