proposition: Lemma metrizable_impl_first_countable: forall X:TopologicalSpace, metrizable X -> first_countable X.
proof: Proof. intros. destruct H. red. intros. exists (Im [n:nat | (n>0)%nat] (fun n:nat => open_ball d x (/ (INR n)))). split. - apply open_neighborhood_basis_is_neighborhood_basis. constructor; intros. + destruct H1 as [n ? V]. destruct H1. apply H0. rewrite H2; constructor. auto with *. + destruct (H0 x). destruct (open_neighborhood_basis_cond U) as [V [[eps] ?]]; trivial. destruct (inverses_of_nats_approach_0 eps H2) as [n [? ?]]. exists (open_ball d x (/ (INR n))). split. * now exists n. * red. intros y ?. apply H3. destruct H6. constructor. now apply Rlt_trans with (/ INR n). - apply countable_img. apply countable_type_ensemble. now exists (fun n => n). Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)