proposition: Lemma open_char_neighborhood: forall {X:TopologicalSpace} (U : Ensemble X), open U <-> forall x, In U x -> neighborhood U x.
proof: Proof. split. - intros. exists U. auto with relations topology. - intros. assert (U = FamilyUnion (fun V => open V /\ Included V U)). 2: { rewrite H0. apply open_family_union. intuition. destruct H1. assumption. } apply Extensionality_Ensembles. split; red; intros; intuition. + specialize (H _ H0). destruct H. destruct H as [[? ?] ?]. exists x0; auto. constructor; auto. + destruct H0. destruct H0. intuition. Qed.
imports: TopologicalSpaces Ensembles InteriorsClosures ZornsLemma(EnsemblesImplicit)