[B] Rename MetricTopology_metrizable

Renamed to `MetricTopology_metrized`. This was a misnomer, because
`metrizable` does not occur in the statement of this lemma.

theories/Topology/Completeness.v

@@ -18,7 +18,7 @@ Lemma convergent_sequence_is_cauchy:
   net_limit x x0 -> cauchy x.
 Proof.
 intros.
-destruct (MetricTopology_metrizable X d d_metric x0).
+destruct (MetricTopology_metrized X d d_metric x0).
 red; intros.
 destruct (H (open_ball d x0 (eps/2))) as [N].
 - Opaque In. apply open_neighborhood_basis_elements. Transparent In.
@@ -45,14 +45,14 @@ Lemma cauchy_sequence_with_cluster_point_converges:
 Proof.
 intros.
 apply metric_space_net_limit with d.
-- apply MetricTopology_metrizable.
+- apply MetricTopology_metrized.
 - intros.
   red; intros.
   destruct (H (eps/2)) as [N].
   + lra.
   + pose (U := open_ball d x0 (eps/2)).
     assert (open_neighborhood U x0 (X:=MetricTopology d d_metric)).
-  { apply MetricTopology_metrizable.
+  { apply MetricTopology_metrized.
     constructor.
     lra. }
     destruct H3.
@@ -116,12 +116,12 @@ destruct (H y) as [y0].
     destruct (x i); trivial. }
   exists (exist _ y0 H3).
   apply metric_space_net_limit with d_restriction.
-  + apply MetricTopology_metrizable.
+  + apply MetricTopology_metrized.
   + intros.
     unfold d_restriction; simpl.
     apply metric_space_net_limit_converse with
       (MetricTopology d d_metric); trivial.
-    apply MetricTopology_metrizable.
+    apply MetricTopology_metrized.
 Qed.
 
 Lemma complete_subset_is_closed:
@@ -140,7 +140,7 @@ cut (Included (closure F (X:=MetricTopology d d_metric)) F).
     (forall n:nat, In F (y n)) /\ net_limit y x).
 { apply first_countable_sequence_closure; trivial.
   apply metrizable_impl_first_countable.
-  exists d; trivial; apply MetricTopology_metrizable. }
+  exists d; trivial; apply MetricTopology_metrized. }
   destruct H1 as [y []].
   pose (y' := ((fun n:nat => exist _ (y n) (H1 n)) :
                Net nat_DS (MetricTopology d_restriction d_restriction_metric))).
@@ -163,14 +163,14 @@ cut (Included (closure F (X:=MetricTopology d d_metric)) F).
     apply normal_sep_impl_T3_sep.
     apply metrizable_impl_normal_sep.
     exists d; trivial.
-    apply MetricTopology_metrizable. }
+    apply MetricTopology_metrized. }
     now apply H7. }
     now rewrite H7.
   + apply metric_space_net_limit with d.
-    * apply MetricTopology_metrizable.
+    * apply MetricTopology_metrized.
     * exact (metric_space_net_limit_converse
         (MetricTopology d_restriction d_restriction_metric)
-        d_restriction (MetricTopology_metrizable _ d_restriction
+        d_restriction (MetricTopology_metrized _ d_restriction
                              d_restriction_metric)
         nat_DS y' (exist _ x0 i) H5).
 Qed.

theories/Topology/Completion.v

@@ -76,14 +76,14 @@ cut (exists Y:Type, exists i:X->Y, exists d':Y->Y->R,
             ** constructor.
             ** now apply subset_eq_compat.
       -- pose proof (metric_space_net_limit_converse (MetricTopology d' d'_metric) d'
-           (MetricTopology_metrizable _ d' d'_metric) nat_DS x0 x H4).
-         apply metric_space_net_limit with (1:=MetricTopology_metrizable _ _ d'_metric0).
+           (MetricTopology_metrized _ d' d'_metric) nat_DS x0 x H4).
+         apply metric_space_net_limit with (1:=MetricTopology_metrized _ _ d'_metric0).
          (*
          destruct (metric_space_net_limit (MetricTopology d' d'_metric)
-           d' (MetricTopology_metrizable _ d' d'_metric) nat_DS x0 x).
+           d' (MetricTopology_metrized _ d' d'_metric) nat_DS x0 x).
          pose proof (H6 H4); clear H6 H7.
          apply <- (metric_space_net_limit (MetricTopology _ d'_metric0)
-           _ (MetricTopology_metrizable _ _ d'_metric0) nat_DS). *)
+           _ (MetricTopology_metrized _ _ d'_metric0) nat_DS). *)
          intros.
          destruct (H6 eps H7).
          exists x1.
@@ -95,7 +95,7 @@ cut (exists Y:Type, exists i:X->Y, exists d':Y->Y->R,
          now apply H8.
     * apply metrizable_impl_first_countable.
       exists d'; trivial.
-      apply MetricTopology_metrizable.
+      apply MetricTopology_metrized.
   + intros.
     now simpl.
   + apply (closed_subset_of_complete_is_complete Y d' d'_metric F);

theories/Topology/MetricSpaces.v

@@ -102,7 +102,7 @@ Inductive metrizable (X:TopologicalSpace) : Prop :=
     metric d -> metrizes X d ->
     metrizable X.
 
-Lemma MetricTopology_metrizable: forall (X:Type) (d:X->X->R)
+Lemma MetricTopology_metrized: forall (X:Type) (d:X->X->R)
   (d_metric: metric d),
   metrizes (MetricTopology d d_metric) d.
 Proof.
@@ -112,6 +112,14 @@ intros.
 apply Build_TopologicalSpace_from_open_neighborhood_bases_basis.
 Qed.
 
+Corollary MetricTopology_metrizable X (d:X->X->R) d_metric :
+  metrizable (MetricTopology d d_metric).
+Proof.
+apply intro_metrizable with (d := d).
+- assumption.
+- apply MetricTopology_metrized.
+Qed.
+
 Lemma metric_open_ball_In X (d : X -> X -> R) :
   metric d -> forall x r,
     0 < r <->

theories/Topology/RTopology.v

@@ -594,7 +594,7 @@ destruct (bounded_real_net_has_cluster_point nat_DS x a b) as [x0].
 - exists x0.
   apply cauchy_sequence_with_cluster_point_converges; trivial.
   apply metric_space_net_cluster_point with R_metric;
-    try apply MetricTopology_metrizable.
+    try apply MetricTopology_metrized.
   intros.
   apply metric_space_net_cluster_point_converse with RTop; trivial.
   apply RTop_metrization.

theories/Topology/TietzeExtension.v

@@ -416,7 +416,7 @@ split.
             R_metric_is_metric X_nonempty).
   + apply (uniform_metric_is_metric _ _ R_metric (fun _:X => 0)
               R_metric_is_metric X_nonempty).
-  + apply MetricTopology_metrizable.
+  + apply MetricTopology_metrized.
 Defined.
 
 Lemma Tietze_extension_func_bound: forall x:X,
@@ -453,7 +453,7 @@ apply Rle_trans with (uniform_metric _ _ R_metric_is_metric X_nonempty
 - apply lt_plus_epsilon_le.
   intros.
   unshelve refine (let H1:=metric_space_net_limit_converse _ _ _ _ _ _ n eps H0 in _); [ | | clearbody H1 ]; shelve_unifiable.
-  { apply MetricTopology_metrizable. }
+  { apply MetricTopology_metrized. }
   destruct H1 as [N].
   refine (Rle_lt_trans _ _ _
     (triangle_inequality _ _ _ _ (convert_approx_to_uniform_space N) _) _).
@@ -495,7 +495,7 @@ unfold Tietze_extension_func;
 assert (eps/2 > 0) by lra.
 unshelve refine (let H1:=metric_space_net_limit_converse _ _ _ _ _ _ n (eps/2) H0
           in _); [ | | clearbody H1 ]; shelve_unifiable.
-{ apply MetricTopology_metrizable. }
+{ apply MetricTopology_metrized. }
 destruct H1 as [N1].
 assert (Rabs (2/3) < 1).
 { rewrite Rabs_right; lra. }
@@ -537,15 +537,15 @@ assert (continuous (fun x:R => x)
   apply metric_space_fun_continuity with R_metric R_metric;
     intros.
   - apply RTop_metrization.
-  - apply MetricTopology_metrizable.
+  - apply MetricTopology_metrized.
   - now exists eps. }
 assert (continuous (fun x:R => x)
   (X:=MetricTopology R_metric R_metric_is_metric) (Y:=RTop)).
 { apply pointwise_continuity.
   intros.
   apply metric_space_fun_continuity with R_metric R_metric;
     intros.
-  - apply MetricTopology_metrizable.
+  - apply MetricTopology_metrized.
   - apply RTop_metrization.
   - now exists eps. }
 intros.

theories/Topology/UniformTopology.v

@@ -125,7 +125,7 @@ assert (forall y:Net nat_DS (MetricTopology d d_metric), cauchy d y ->
     apply T3_sep_impl_Hausdorff.
     apply normal_sep_impl_T3_sep.
     apply metrizable_impl_normal_sep.
-    exists d; trivial; apply MetricTopology_metrizable.
+    exists d; trivial; apply MetricTopology_metrized.
 }
 red; intros f ?.
 unshelve refine (let H1 := _ in let H2 := _ in ex_intro _
@@ -166,7 +166,7 @@ unshelve refine (let H1 := _ in let H2 := _ in ex_intro _
     intros.
     destruct cauchy_limit; simpl.
     pose proof (metric_space_net_limit_converse _ _
-      (MetricTopology_metrizable _ d d_metric) nat_DS
+      (MetricTopology_metrized _ d d_metric) nat_DS
       (fun n:nat => proj1_sig (f n) x) x0 n).
     destruct (H7 eps H6) as [i0].
     pose (N' := max N i0).
@@ -201,7 +201,7 @@ unshelve refine (let H1 := _ in let H2 := _ in ex_intro _
   }
   auto with real.
 - apply metric_space_net_limit with uniform_metric.
-  { apply MetricTopology_metrizable. }
+  { apply MetricTopology_metrized. }
   intros.
   assert (eps/2 > 0) by lra.
   destruct (H0 (eps/2) H4) as [N].
@@ -217,7 +217,7 @@ unshelve refine (let H1 := _ in let H2 := _ in ex_intro _
   destruct (cauchy_limit (fun n:nat => proj1_sig (f n) x0) (H1 x0));
     simpl.
   pose proof (metric_space_net_limit_converse _ _
-    (MetricTopology_metrizable _ d d_metric) nat_DS
+    (MetricTopology_metrized _ d d_metric) nat_DS
     (fun n:nat => proj1_sig (f n) x0) x1 n).
   destruct (H9 eps0 H8) as [N'].
   pose (N'' := max N N').
@@ -276,22 +276,22 @@ red; intros f0 ?.
 red.
 apply first_countable_sequence_closure in H.
 - destruct H as [f []].
-  pose proof (MetricTopology_metrizable _ d d_metric
+  pose proof (MetricTopology_metrized _ d d_metric
     (proj1_sig f0 x0)).
   apply open_neighborhood_basis_is_neighborhood_basis in H1.
   apply continuous_at_neighborhood_basis with (1:=H1).
   intros.
   destruct H2.
   assert (r/3>0) by lra.
   destruct (metric_space_net_limit_converse _ _
-    (MetricTopology_metrizable _ _
+    (MetricTopology_metrized _ _
        (uniform_metric_is_metric _ _ d y0 d_metric X_inh))
     nat_DS f f0 H0 (r/3) H3) as [N].
   assert (neighborhood
     (inverse_image (proj1_sig (f N))
        (open_ball d (proj1_sig (f N) x0) (r/3))) x0).
   { apply H.
-    pose proof (MetricTopology_metrizable _ d d_metric
+    pose proof (MetricTopology_metrized _ d d_metric
       (proj1_sig (f N) x0)).
     apply open_neighborhood_basis_is_neighborhood_basis in H5.
     apply H5.
@@ -336,7 +336,7 @@ apply first_countable_sequence_closure in H.
 - apply metrizable_impl_first_countable.
   exists (uniform_metric d y0 d_metric X_inh).
   + exact (uniform_metric_is_metric _ _ d y0 d_metric X_inh).
-  + apply MetricTopology_metrizable.
+  + apply MetricTopology_metrized.
 Qed.
 
 Lemma continuous_functions_closed_in_uniform_metric: