proposition: Lemma compact_hausdorff_homeo {X Y : TopologicalSpace} (f : X -> Y) : compact X -> Hausdorff Y -> bijective f -> continuous f -> homeomorphism f.
proof: Proof. intros. apply bijective_impl_invertible in H1. destruct H1 as [g Hgf Hfg]. exists g; auto. apply continuous_closed. intros. assert (compact (SubspaceTopology U)) as HU_compact. { apply closed_compact; auto. } replace (inverse_image g U) with (Im U f). 2: { extensionality_ensembles; subst. - constructor. rewrite Hgf. assumption. - exists (g x); auto. } apply compact_closed; auto. apply compact_image_ens; assumption. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)