proposition: Lemma metric_space_subspace_topology_metrizes : metrizes X d -> metrizes (SubspaceTopology F) d_restriction.
proof: Proof. intros HX. red. intros p. split. - intros U HU. destruct HU. split. + apply subspace_open_char. exists (open_ball d (proj1_sig p) r). split. * apply metric_space_open_ball_open; auto. * apply d_restriction_metric_open_ball. + constructor. rewrite metric_zero; auto. apply d_restriction_metric; assumption. - intros U [HU HUp]. rewrite subspace_open_char in HU. destruct HU as [V [HV HUV]]. subst. destruct HUp as [HVp]. pose proof (open_neighborhood_basis_cond _ _ (HX (proj1_sig p)) V) as [VV [HVV0 HrV]]. { split; auto. } destruct HVV0 as [r Hr]. exists (open_ball d_restriction p r). split. { constructor. assumption. } red; intros. destruct H. constructor. apply HrV. constructor. assumption. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)