proposition: Lemma first_countable_open_neighborhood_bases: forall X:TopologicalSpace, first_countable X -> forall x:point_set X, exists NBx:Family X, open_neighborhood_basis NBx x /\ Countable NBx.
proof: Proof. intros. destruct (H x) as [NBx [? ?]]. exists (@Im (Ensemble X) (Ensemble X) NBx (@interior X)). split. - constructor; intros. + destruct H2. split; rewrite H3. * apply interior_open. * now apply neighborhood_interior, H0. + destruct H0. destruct (neighborhood_basis_cond U) as [N]. * now apply open_neighborhood_is_neighborhood. * destruct H0. exists (interior N). split. ** now exists N. ** pose proof (interior_deflationary N). auto with sets. - now apply countable_img. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)