proposition: Lemma topological_property_connected : topological_property connected.
proof: Proof. intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hconn S HS. destruct (Hconn (inverse_image f S)) as [HfS|HfS]; [ | left | right ]; try extensionality_ensembles. - apply continuous_clopen; auto. - rewrite <- Hfg. apply in_inverse_image. rewrite inverse_image_empty, <- HfS. constructor. now rewrite Hfg. - constructor. - rewrite <- Hfg. apply in_inverse_image. rewrite HfS. constructor. Qed.
imports: TopologicalSpaces Homeomorphisms SubspaceTopology ZornsLemma(EnsemblesTactics Powerset_facts)