proposition: Lemma metrizable_Lindelof_impl_second_countable: forall X:TopologicalSpace, metrizable X -> Lindelof X -> second_countable X.
proof: Proof. intros X [d Hmetric Hmetrizes] HLindelof. pose (small_balls := (fun n : { n : nat | (n > 0)%nat } => Im Full_set (fun x : X => open_ball d x (/ (INR (proj1_sig n)))))). assert (forall n, open_cover (small_balls n)) as Hballs_cover. { destruct n as [n]. split. - intros U H. destruct H as [x ? U]. destruct (Hmetrizes x). subst. apply metric_space_open_ball_open; auto. - extensionality_ensembles. { constructor. } simpl. exists (open_ball d x (/ INR n)). + now exists x. + constructor. rewrite metric_zero; auto with real. } destruct (choice (fun (n:{n:nat | (n > 0)%nat}) (S:Family X) => subcover S (small_balls n) /\ Countable S)) as [choice_fun Hchoice_fun]. { intros. auto. } exists (IndexedUnion choice_fun). split. 2: { apply countable_indexed_union. - apply countable_type_ensemble. exists (fun n:nat => n). now red. - intro. apply Hchoice_fun. } split. { intros V HV. destruct HV as [n V HV]. apply (Hballs_cover n). apply (Hchoice_fun n). assumption. } intros. destruct (open_neighborhood_basis_cond _ x (Hmetrizes x) U) as [V [HVbasis HVU]]. { now split. } inversion HVbasis; subst; clear HVbasis. destruct (inverses_of_nats_approach_0 (r/2)) as [n [Hnpos ?]]. { lra. } pose (nsig := exist _ n Hnpos). destruct (Hchoice_fun nsig) as [[Hnsig_subcover0 Hnsig_subcover1] Hnsig_countable]. assert (In (FamilyUnion (choice_fun nsig)) x) as Hx. { apply Hnsig_subcover1. exists (open_ball d x (/ INR n)). { exists x; constructor. } apply metric_open_ball_In; auto. apply Rinv_0_lt_compat. apply lt_0_INR. lia. } destruct Hx as [W x HW_nsig HWx]. exists W. repeat split. { exists nsig. assumption. } 2: { assumption. } assert (Included W (open_ball d x r)); auto with sets. pose proof (Hnsig_subcover0 _ HW_nsig) as HW_small_balls. destruct HW_small_balls. subst. simpl in *. apply open_ball_half_radius_included; auto. split; auto with real. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)