proposition: Lemma connected_subsingleton {X : TopologicalSpace} : (forall x y : X, x = y) -> connected X.
proof: Proof. intros. red. intros. destruct (classic (Inhabited S)). - right. apply Extensionality_Ensembles; split; red; intros. { constructor. } destruct H1. replace x with x0; try assumption. apply H. - apply Powerset_facts.not_inhabited_empty in H1. left. assumption. Qed.
imports: TopologicalSpaces Homeomorphisms SubspaceTopology ZornsLemma(EnsemblesTactics Powerset_facts)