proposition: Lemma metrizable_separable_impl_second_countable: forall X:TopologicalSpace, metrizable X -> separable X -> second_countable X.
proof: Proof. intros. destruct H, H0 as [S []]. exists (Im [p:(Q*X)%type | let (r,x):=p in (r>0)%Q /\ In S x] (fun p:(Q*X)%type => let (r,x):=p in open_ball d x (Q2R r))). split. - constructor. + intros. destruct H3. subst. destruct x as [r x]. destruct H3 as [[]]. destruct (H1 x). destruct (open_neighborhood_basis_elements (open_ball d x (Q2R r))); trivial. constructor; try lra. rewrite <- RMicromega.Q2R_0. now apply Qlt_Rlt. + intros. destruct (H1 x). destruct (open_neighborhood_basis_cond U) as [V [[r]]]. { now split. } destruct (dense_meets_every_nonempty_open _ _ H2 (open_ball d x (r/2))). { apply metric_space_open_ball_open; auto. } { exists x. apply metric_open_ball_In; auto. lra. } destruct H7, H8. destruct (rationals_dense_in_reals (d x x0) (r - d x x0)) as [r']. { lra. } exists (open_ball d x0 (Q2R r')). repeat split. * exists ( (r', x0) ); trivial. constructor. split; trivial. assert (Q2R r' > 0). { apply Rgt_ge_trans with (d x x0). - apply H9. - now apply metric_nonneg. } apply Rlt_Qlt. unfold Q2R at 1. simpl. now ring_simplify. * red. intros y ?. destruct H10. apply H6. constructor. eapply Rle_lt_trans. -- now apply triangle_inequality. -- apply Rlt_trans with (d x x0 + Q2R r'); auto with real. lra. * destruct H9. now rewrite metric_sym. - apply countable_img. destruct H0 as [h]. destruct Q_countable as [f Hf]. destruct countable_nat_product as [g]. red. match goal with |- CountableT ?T => exists (fun x:T => match x with | exist (r, x0) (intro_characteristic_sat (conj r_pos i)) => g (h (exist _ x0 i), f r) end) end. red. intros x y H5. destruct x as [[r1 x1] [[pos_r1 i1]]]. destruct y as [[r2 x2] [[pos_r2 i2]]]. apply subset_eq. simpl. repeat match goal with | Hg : injective ?g, Heq : ?g ?a = ?g ?b |- _ => apply Hg in Heq | Heq : (_, _) = (_, _) |- _ => inversion Heq; subst; clear Heq | Heq : exist _ _ _ = exist _ _ _ |- _ => inversion Heq; subst; clear Heq end. reflexivity. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)