proposition: Lemma closure_impl_filter_limit: forall {X:TopologicalSpace} (S:Ensemble X) (x0:point_set X), In (closure S) x0 -> exists F:Filter X, In (filter_family F) S /\ filter_limit F x0.
proof: Proof. intros. assert (Inhabited S). { destruct (closure_impl_meets_every_open_neighborhood _ _ _ H Full_set). - apply open_full. - constructor. - destruct H0. exists x; trivial. } unshelve refine (let H1:=_ in let H2:=_ in let H3:=_ in let Sfilt := Build_Filter_from_basis (Singleton S) H1 H2 H3 in _). - exists S; constructor. - red; intro. inversion H2. rewrite H3 in H0. destruct H0. destruct H0. - intros. destruct H3. destruct H4. exists S; split; auto with sets. - unshelve refine (let H4:=_ in ex_intro _ (filter_sum (neighborhood_filter x0) Sfilt H4) _). + intros. simpl in H4. destruct H4 as [[U [[]]]]. simpl in H5. destruct H5 as [[T0 [[]]]]. destruct (closure_impl_meets_every_open_neighborhood _ _ _ H U); trivial. destruct H8. exists x; constructor; auto. + split. * simpl. constructor. exists S. split; auto with sets. exists ( (Full_set, S) ). -- constructor; split. ++ constructor. exists Full_set; repeat split. apply open_full. ++ constructor. exists S; split; auto with sets. -- symmetry. apply Intersection_Full_set. * red; red; intros U ?. constructor. exists U. split; auto with sets. exists ( (U, Full_set) ). -- constructor. split; trivial. constructor. exists S; split; auto with sets. -- rewrite Intersection_commutative. symmetry. apply Intersection_Full_set. Qed.
imports: ZornsLemma(Powerset_facts)