proposition: Lemma Hausdorff_impl_net_limit_is_unique_cluster_point: forall {X:TopologicalSpace} {I:DirectedSet} (x:Net I X) (x0:point_set X), Hausdorff X -> net_limit x x0 -> forall y:point_set X, net_cluster_point x y -> y = x0.
proof: Proof. intros. destruct (net_cluster_point_impl_subnet_converges _ _ x y H1) 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 Hausdorff_impl_net_limit_unique with x'. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)