proposition: Lemma continuousP (S T : topologicalType) (f : S -> T) : continuous f <-> forall A, open A -> open (f @^-1` A).
proof: Proof. split=> fcont; first by rewrite !openE => A Aop ? /Aop /fcont. move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [Bop Bfs] sBA]. by exists (f @^-1` B); [split=> //; apply/fcont|move=> ? /sBA]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed