proposition: Lemma continuous_clopen {X Y : TopologicalSpace} (f : X -> Y) (A : Ensemble Y) : continuous f -> clopen A -> clopen (inverse_image f A).
proof: Proof. intros. destruct H0. split; auto. apply continuous_closed; assumption. Qed.
imports: TopologicalSpaces Homeomorphisms SubspaceTopology ZornsLemma(EnsemblesTactics Powerset_facts)