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