proposition: Lemma homeomorphism_is_open_map: forall {X Y:TopologicalSpace} (f:X -> Y), homeomorphism f -> open_map f.
proof: Proof. intros. destruct H as [g]. red; intros. assert (Im U f = inverse_image g U). { extensionality_ensembles. - subst. constructor. now rewrite H1. - exists (g x); auto. } rewrite H4. auto. Qed.
imports: ZornsLemma(EnsemblesTactics Relation_Definitions_Implicit)