proposition: Lemma net_limit_uniqueness_impl_Hausdorff: forall X:TopologicalSpace, (forall (I:DirectedSet) (x:Net I X), uniqueness (net_limit x)) -> Hausdorff X.
proof: Proof. intros. apply net_limit_is_unique_cluster_point_impl_Hausdorff. intros. pose proof (net_cluster_point_impl_subnet_converges _ _ _ _ H1). destruct H2 as [J [x' [? ?]]]. - destruct (H0 Full_set). + apply open_full. + constructor. + now exists. - assert (net_limit x' x0) by now apply subnet_limit with _ x. now apply H with _ x'. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)