proposition: Lemma continuous_inP {U} A (f : T -> U) : open A -> {in A, continuous f} <-> forall X, open X -> open (A `&` f @^-1` X).
proof: Proof. move=> oA; rewrite -continuous_open_subspace// continuousP. by under eq_forall do rewrite -open_setSI//. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed