proposition: Lemma net_limits_determine_topology: forall {X:TopologicalSpace} (S:Ensemble X) (x0:X), In (closure S) x0 -> exists I:DirectedSet, exists x:Net I X, (forall i:DS_set I, In S (x i)) /\ net_limit x x0.
proof: Proof. intros. assert (forall U:Ensemble X, open U -> In U x0 -> Inhabited (Intersection S U)). { intros. apply NNPP. intro. assert (Included (closure S) (Complement U)). { apply closure_minimal; red. - now rewrite Complement_Complement. - intros. intro. contradiction H2. exists x. auto with sets. } contradict H1. now apply H3. } pose (Ssel := fun n:neighborhood_net_DS_set X x0 => match n with | intro_neighborhood_net_DS V y _ _ _ => (In S y) end). pose (our_DS_set := {n:neighborhood_net_DS_set X x0 | Ssel n}). pose (our_DS_ord := fun (n1 n2:our_DS_set) => neighborhood_net_DS_ord X x0 (proj1_sig n1) (proj1_sig n2)). assert (preorder our_DS_ord). { constructor; red. - intros. red. apply preord_refl. apply (@DS_ord_cond (neighborhood_net_DS X x0)). - intros x y z. unfold our_DS_ord. apply preord_trans. apply (@DS_ord_cond (neighborhood_net_DS X x0)). } assert (forall i j:our_DS_set, exists k:our_DS_set, our_DS_ord i k /\ our_DS_ord j k). { destruct i, x, j. destruct x. assert (open (Intersection U U0)) by now apply open_intersection2. assert (In (Intersection U U0) x0) by auto with sets. assert (Inhabited (Intersection S (Intersection U U0))) by now apply H0. destruct H4. destruct H4. pose (k0 := intro_neighborhood_net_DS X x0 (Intersection U U0) x H2 H3 H5). assert (Ssel k0). { red. now unfold k0. } exists (exist _ k0 H6). split; red; simpl; auto with sets. } pose (our_DS := Build_DirectedSet our_DS_set our_DS_ord H1 H2). exists our_DS. exists (fun i:our_DS_set => neighborhood_net X x0 (proj1_sig i)). split. - intros. now destruct i, x. - red. intros. assert (Inhabited (Intersection S U)) by now apply H0. destruct H5. destruct H5. pose (i0 := intro_neighborhood_net_DS X x0 U x H3 H4 H6). assert (Ssel i0) by trivial. exists (exist _ i0 H7). intros. destruct j, x1. simpl in H8. red in H8. simpl in H8. simpl. auto with sets. Qed.