proposition: Lemma homeomorphic_equiv: equivalence homeomorphic.
proof: Proof. constructor. - eexists; eapply homeomorphism_id. - intros X Y Z ? ?. destruct H as [f [finv]]. destruct H0 as [g [ginv]]. exists (fun x => g (f x)), (fun z => finv (ginv z)); congruence || now apply continuous_composition. - intros X Y ?. destruct H as [f [finv]]. now exists finv, f. Qed.
imports: ZornsLemma(EnsemblesTactics Relation_Definitions_Implicit)