# Theory Metric_Completion

```(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
*)

section ‹The metric completion of a metric space›

theory Metric_Completion
imports Isometries
begin

text ‹Any metric space can be completed, by adding the missing limits of Cauchy sequences.
Formally, there exists an isometric embedding of the space in a complete space, with dense image.
In this paragraph, we construct this metric completion. This is exactly the same construction
as the way in which real numbers are constructed from rational numbers.›

subsection ‹Definition of the metric completion›

"nat ⇒ ('a::metric_space)" / partial: "λu v. (Cauchy u) ∧ (Cauchy v) ∧ (λn. dist (u n) (v n)) ⇢ 0"
unfolding part_equivp_def proof(auto intro!: ext)
show "∃x. Cauchy x"
by (rule exI[of _ "λ_. undefined"]) (simp add: convergent_Cauchy convergent_const)
fix x y z::"nat ⇒ 'a" assume H: "(λn. dist (x n) (y n)) ⇢ 0"
"(λn. dist (x n) (z n)) ⇢ 0"
have *: "(λn. dist (x n) (y n) + dist (x n) (z n)) ⇢ 0 + 0"
show "(λn. dist (y n) (z n)) ⇢ 0"
apply (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. dist (x n) (y n) + dist (x n) (z n)"])
using * by (auto simp add: dist_triangle3)
next
fix x y z::"nat ⇒ 'a" assume H: "(λn. dist (x n) (y n)) ⇢ 0"
"(λn. dist (y n) (z n)) ⇢ 0"
have *: "(λn. dist (x n) (y n) + dist (y n) (z n)) ⇢ 0 + 0"
show "(λn. dist (x n) (z n)) ⇢ 0"
apply (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. dist (x n) (y n) + dist (y n) (z n)"])
using * by (auto simp add: dist_triangle)
next
fix x y::"nat ⇒ 'a" assume H: "Cauchy x"
"(λv. Cauchy v ∧ (λn. dist (x n) (v n)) ⇢ 0) = (λv. Cauchy v ∧ (λn. dist (y n) (v n)) ⇢ 0)"
have "Cauchy x ∧ (λn. dist (x n) (x n)) ⇢ 0" using H by auto
then have "(λn. dist (y n) (x n))⇢ 0" using H by meson
moreover have "dist (x n) (y n) = dist (y n) (x n)" for n using dist_commute by auto
ultimately show "(λn. dist (x n) (y n)) ⇢ 0" by auto
qed

text ‹We have to show that the metric completion is indeed a metric space, that
the original space embeds isometrically into it, and that it is complete. Before we prove these
statements, we start with two simple lemmas that will be needed later on.›

lemma convergent_Cauchy_dist:
fixes u v::"nat ⇒ ('a::metric_space)"
assumes "Cauchy u" "Cauchy v"
shows "convergent (λn. dist (u n) (v n))"
proof (rule real_Cauchy_convergent, intro CauchyI)
fix e::real assume "e > 0"
obtain Nu where Nu: "∀n ≥ Nu. ∀m ≥ Nu. dist (u n) (u m) < e/2" using assms(1)
by (metis ‹0 < e› less_divide_eq_numeral1(1) metric_CauchyD mult_zero_left)
obtain Nv where Nv: "∀n ≥ Nv. ∀m ≥ Nv. dist (v n) (v m) < e/2" using assms(2)
by (metis ‹0 < e› less_divide_eq_numeral1(1) metric_CauchyD mult_zero_left)
define M where "M = max Nu Nv"
{
fix n m assume H: "n ≥ M" "m ≥ M"
have *: "dist (u n) (u m) < e/2" "dist (v n) (v m) < e/2"
using Nu Nv H unfolding M_def by auto
have "dist (u m) (v m) - dist (u n) (v n) ≤ dist (u m) (u n) + dist (v n) (v m)"
also have "... < e/2 + e/2"
using * by (simp add: dist_commute)
finally have A: "dist (u m) (v m) - dist (u n) (v n) < e" by simp

have "dist (u n) (v n) - dist (u m) (v m) ≤ dist (u m) (u n) + dist (v n) (v m)"
also have "... < e/2 + e/2"
using * by (simp add: dist_commute)
finally have "dist (u n) (v n) - dist (u m) (v m) < e" by simp
then have "norm(dist (u m) (v m) - dist (u n) (v n)) < e" using A by auto
}
then show "∃M. ∀m ≥ M. ∀n ≥ M. norm (dist (u m) (v m) - dist (u n) (v n)) < e"
by auto
qed

fixes u v::"nat ⇒ ('a::real_normed_vector)"
assumes "convergent u"
"(λn. v n - u n) ⇢ 0"
shows "convergent v" "lim v = lim u"
proof -
have "(λn. u n + (v n - u n)) ⇢ lim u + 0"
apply (rule tendsto_add) using assms convergent_LIMSEQ_iff by auto
then have *: "v ⇢ lim u" by auto
show "convergent v" using * by (simp add: Lim_def convergentI)
show "lim v = lim u" using * by (simp add: limI)
qed

text ‹Let us now prove that the metric completion is a metric space: the distance between two
Cauchy sequences is the limit of the distances of points in the sequence. The convergence follows
from Lemma~\verb+convergent_Cauchy_dist+ above.›

instantiation metric_completion :: (metric_space) metric_space
begin

lift_definition dist_metric_completion::"('a::metric_space) metric_completion ⇒ 'a metric_completion ⇒ real"
is "λx y. lim (λn. dist (x n) (y n))"
proof -
fix x y z t::"nat ⇒ 'a" assume H: "Cauchy x ∧ Cauchy y ∧ (λn. dist (x n) (y n)) ⇢ 0"
"Cauchy z ∧ Cauchy t ∧ (λn. dist (z n) (t n)) ⇢ 0"
show "lim (λn. dist (x n) (z n)) = lim (λn. dist (y n) (t n))"
show "convergent (λn. dist (y n) (t n))"
apply (rule convergent_Cauchy_dist) using H by auto

have a: "(λn. - dist (t n) (z n) - dist (x n) (y n)) ⇢ -0 -0"
apply (intro tendsto_intros) using H by (auto simp add: dist_commute)
have b:"(λn. dist (t n) (z n) + dist (x n) (y n)) ⇢ 0 + 0"
have I: "dist (x n) (z n) ≤ dist (t n) (y n) + (dist (t n) (z n) + dist (x n) (y n))" for n
using dist_triangle[of "x n" "z n" "y n"] dist_triangle[of "y n" "z n" "t n"]
show "(λn. dist (x n) (z n) - dist (y n) (t n)) ⇢ 0"
apply (rule tendsto_sandwich[of "λn. -(dist (x n) (y n) + dist (z n) (t n))" _ _ "λn. dist (x n) (y n) + dist (z n) (t n)"])
apply (auto intro!: always_eventually simp add: algebra_simps dist_commute I)
using a b by auto
qed
qed

lemma dist_metric_completion_limit:
fixes x y::"'a metric_completion"
shows "(λn. dist (rep_metric_completion x n) (rep_metric_completion y n)) ⇢ dist x y"
proof -
have C: "Cauchy (rep_metric_completion x)" "Cauchy (rep_metric_completion y)"
using Quotient3_metric_completion Quotient3_rep_reflp by fastforce+
show ?thesis
unfolding dist_metric_completion_def using C apply auto
using convergent_Cauchy_dist[OF C] convergent_LIMSEQ_iff by force
qed

lemma dist_metric_completion_limit':
fixes x y::"nat ⇒ 'a"
assumes "Cauchy x" "Cauchy y"
shows "(λn. dist (x n) (y n)) ⇢ dist (abs_metric_completion x) (abs_metric_completion y)"
apply (subst dist_metric_completion.abs_eq)
using assms convergent_Cauchy_dist[OF assms] by (auto simp add: convergent_LIMSEQ_iff)

text ‹To define a metric space in the current library of Isabelle/HOL, one should also introduce
a uniformity structure and a topology, as follows (they are prescribed by the distance):›

definition uniformity_metric_completion::"(('a metric_completion) × ('a metric_completion)) filter"
where "uniformity_metric_completion = (INF e∈{0 <..}. principal {(x, y). dist x y < e})"

definition open_metric_completion :: "'a metric_completion set ⇒ bool"
where "open_metric_completion U = (∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"

instance proof
fix x y::"'a metric_completion"
have C: "Cauchy (rep_metric_completion x)" "Cauchy (rep_metric_completion y)"
using Quotient3_metric_completion Quotient3_rep_reflp by fastforce+
show "(dist x y = 0) = (x = y)"
apply (subst Quotient3_rel_rep[OF Quotient3_metric_completion, symmetric])
unfolding dist_metric_completion_def using C apply auto
using convergent_Cauchy_dist[OF C] convergent_LIMSEQ_iff apply force
next
fix x y z::"'a metric_completion"
have a: "(λn. dist (rep_metric_completion x n) (rep_metric_completion y n)) ⇢ dist x y"
using dist_metric_completion_limit by auto
have b: "(λn. dist (rep_metric_completion x n) (rep_metric_completion z n) + dist (rep_metric_completion y n) (rep_metric_completion z n))
⇢ dist x z + dist y z"
apply (rule tendsto_add) using dist_metric_completion_limit by auto
show "dist x y ≤ dist x z + dist y z"
by (rule LIMSEQ_le[OF a b], rule exI[of _ 0], auto simp add: dist_triangle2)
qed (auto simp add: uniformity_metric_completion_def open_metric_completion_def)
end

text ‹Let us now show that the distance thus defined on the metric completion is indeed complete.
This is essentially by design.›

instance metric_completion :: (metric_space) complete_space
proof
fix X::"nat ⇒ 'a metric_completion" assume "Cauchy X"
have *: "∃N. ∀n ≥ N. dist (rep_metric_completion (X k) N) (rep_metric_completion (X k) n) < (1/Suc k)" for k
proof -
have "Cauchy (rep_metric_completion (X k))"
using Quotient3_metric_completion Quotient3_rep_reflp by fastforce+
then have "∃N. ∀m ≥ N. ∀n ≥ N. dist (rep_metric_completion (X k) m) (rep_metric_completion (X k) n) < (1/Suc k)"
unfolding Cauchy_def by auto
then show ?thesis by auto
qed
have "∃N. ∀k. ∀n ≥ N k. dist (rep_metric_completion (X k) (N k)) (rep_metric_completion (X k) n) < (1/Suc k)"
apply (rule choice) using * by auto
then obtain N::"nat ⇒ nat" where
N: "dist (rep_metric_completion (X k) (N k)) (rep_metric_completion (X k) n) < (1/Suc k)" if "n ≥ N k" for n k
by auto
define u where "u = (λk. rep_metric_completion (X k) (N k))"

have "Cauchy u"
proof (rule metric_CauchyI)
fix e::real assume "e > 0"
obtain K::nat where "K > 4/e" using reals_Archimedean2 by blast
obtain L::nat where L: "∀m ≥ L. ∀n ≥ L. dist (X m) (X n) < e/2"
using metric_CauchyD[OF ‹Cauchy X›, of "e/2"] ‹e > 0› by auto
{
fix m n assume "m ≥ max K L" "n ≥ max K L"
then have "dist (X m) (X n) < e/2" using L by auto
then have "eventually (λp. dist (rep_metric_completion (X m) p) (rep_metric_completion (X n) p) < e/2) sequentially"
using dist_metric_completion_limit[of "X m" "X n"] by (metis order_tendsto_iff)
then obtain p where p: "p ≥ max (N m) (N n)" "dist (rep_metric_completion (X m) p) (rep_metric_completion (X n) p) < e/2"
using eventually_False_sequentially eventually_elim2 eventually_ge_at_top by blast
have "dist (u m) (rep_metric_completion (X m) p) < 1 / real (Suc m)"
unfolding u_def using N[of m p] p(1) by auto
also have "... < e/4"
using ‹m ≥ max K L› ‹K > 4/e› ‹e > 0› apply (auto simp add: divide_simps algebra_simps)
by (metis leD le_less_trans less_add_same_cancel2 linear of_nat_le_iff mult_le_cancel_iff2)
finally have Im: "dist (u m) (rep_metric_completion (X m) p) < e/4" by simp
have "dist (u n) (rep_metric_completion (X n) p) < 1 / real (Suc n)"
unfolding u_def using N[of n p] p(1) by auto
also have "... < e/4"
using ‹n ≥ max K L› ‹K > 4/e› ‹e > 0› apply (auto simp add: divide_simps algebra_simps)
by (metis leD le_less_trans less_add_same_cancel2 linear of_nat_le_iff mult_le_cancel_iff2)
finally have In: "dist (u n) (rep_metric_completion (X n) p) < e/4" by simp

have "dist (u m) (u n) ≤ dist (u m) (rep_metric_completion (X m) p)
+ dist (rep_metric_completion (X m) p) (rep_metric_completion (X n) p) + dist (rep_metric_completion (X n) p) (u n)"
also have "... < e/4 + e/2 + e/4"
using In Im p(2) by (simp add: dist_commute)
also have "... = e" by auto
finally have "dist (u m) (u n) < e" by auto
}
then show "∃M. ∀m ≥ M. ∀n ≥ M. dist (u m) (u n) < e" by meson
qed
have *: "(λn. dist (abs_metric_completion u) (X n)) ⇢ 0"
proof (rule order_tendstoI, auto simp add: less_le_trans eventually_sequentially)
fix e::real assume "e > 0"
obtain K::nat where "K > 4/e" using reals_Archimedean2 by blast
obtain L::nat where L: "∀m ≥ L. ∀n ≥ L. dist (u m) (u n) < e/4"
using metric_CauchyD[OF ‹Cauchy u›, of "e/4"] ‹e > 0› by auto
{
fix n assume n: "n ≥ max K L"
{
fix p assume p: "p ≥ max (N n) L"
have "dist (u n) (rep_metric_completion (X n) p) < 1/(Suc n)"
unfolding u_def using N p by simp
also have "... < e/4"
using ‹n ≥ max K L› ‹K > 4/e› ‹e > 0› apply (auto simp add: divide_simps algebra_simps)
by (metis leD le_less_trans less_add_same_cancel2 linear of_nat_le_iff mult_le_cancel_iff2)
finally have *: "dist (u n) (rep_metric_completion (X n) p) < e/4"
by fastforce

have "dist (u p) (rep_metric_completion (X n) p) ≤ dist (u p) (u n) + dist (u n) (rep_metric_completion (X n) p)"
using dist_triangle by auto
also have "... < e/4 + e/4" using * L n p by force
finally have "dist (u p) (rep_metric_completion (X n) p) ≤ e/2" by auto
}
then have A: "eventually (λp. dist (u p) (rep_metric_completion (X n) p) ≤ e/2) sequentially"
using eventually_at_top_linorder by blast
have B: "(λp. dist (u p) (rep_metric_completion (X n) p)) ⇢ dist (abs_metric_completion u) (X n)"
using dist_metric_completion_limit'[OF ‹Cauchy u›, of "rep_metric_completion (X n)"]
unfolding Quotient3_abs_rep[OF Quotient3_metric_completion, of "X n"]
using Quotient3_rep_reflp[OF Quotient3_metric_completion] by auto
have "dist (abs_metric_completion u) (X n) ≤ e/2"
apply (rule LIMSEQ_le_const2[OF B]) using A unfolding eventually_sequentially by auto
then have "dist (abs_metric_completion u) (X n) < e" using ‹e > 0› by auto
}
then show "∃N. ∀n ≥ N. dist (abs_metric_completion u) (X n) < e"
by blast
qed
have "X ⇢ abs_metric_completion u"
apply (rule tendstoI) using * by (auto simp add: order_tendsto_iff dist_commute)
then show "convergent X" unfolding convergent_def by auto
qed

subsection ‹Isometric embedding of a space in its metric completion›

text ‹The canonical embedding of a space into its metric completion is obtained by taking
the Cauchy sequence which is constant, equal to the given point. This is indeed an isometric
embedding with dense image, as we prove in the lemmas below.›

definition to_metric_completion::"('a::metric_space) ⇒ 'a metric_completion"
where "to_metric_completion x = abs_metric_completion (λn. x)"

lemma to_metric_completion_isometry:
"isometry_on UNIV to_metric_completion"
proof (rule isometry_onI)
fix x y::'a
have "(λn. dist (x) (y)) ⇢ dist (to_metric_completion x) (to_metric_completion y)"
unfolding to_metric_completion_def apply (rule dist_metric_completion_limit')
unfolding Cauchy_def by auto
then show "dist (to_metric_completion x) (to_metric_completion y) = dist x y"
qed

lemma to_metric_completion_dense:
assumes "open U" "U ≠ {}"
shows "∃x. to_metric_completion x ∈ U"
proof -
obtain y where "y ∈ U" using ‹U ≠ {}› by auto
obtain e::real where e: "e > 0" "⋀z. dist z y < e ⟹ z ∈ U"
using ‹y ∈ U› ‹open U› by (metis open_dist)
have *: "Cauchy (rep_metric_completion y)"
using Quotient3_metric_completion Quotient3_rep_reflp by fastforce
then obtain N where N: "∀n ≥ N. ∀m ≥ N. dist (rep_metric_completion y n) (rep_metric_completion y m) < e/2"
using ‹e > 0› unfolding Cauchy_def by (meson divide_pos_pos zero_less_numeral)
define x where "x = rep_metric_completion y N"
have "(λn. dist x (rep_metric_completion y n)) ⇢ dist (to_metric_completion x) (abs_metric_completion (rep_metric_completion y))"
unfolding to_metric_completion_def apply (rule dist_metric_completion_limit')
using * unfolding Cauchy_def by auto
then have "(λn. dist x (rep_metric_completion y n)) ⇢ dist (to_metric_completion x) y"
unfolding Quotient3_abs_rep[OF Quotient3_metric_completion] by simp
moreover have "eventually (λn. dist x (rep_metric_completion y n) ≤ e/2) sequentially"
unfolding eventually_sequentially x_def apply (rule exI[of _ N]) using N less_imp_le by auto
ultimately have "dist (to_metric_completion x) y ≤ e/2"
using LIMSEQ_le_const2 unfolding eventually_sequentially by metis
then have "to_metric_completion x ∈ U"
using e by auto
then show ?thesis by auto
qed

lemma to_metric_completion_dense':
"closure (range to_metric_completion) = UNIV"
apply (auto simp add: closure_iff_nhds_not_empty) using to_metric_completion_dense by fastforce

text ‹The main feature of the completion is that a uniformly continuous function on the original space can be extended
to a uniformly continuous function on the completion, i.e., it can be written as the composition of
a new function and of the inclusion \verb+to_metric_completion+.›

lemma lift_to_metric_completion:
fixes f::"('a::metric_space) ⇒ ('b::complete_space)"
assumes "uniformly_continuous_on UNIV f"
shows "∃g. (uniformly_continuous_on UNIV g)
∧ (f = g o to_metric_completion)
∧ (∀x ∈ range to_metric_completion. g x = f (inv to_metric_completion x))"
proof -
define I::"'a metric_completion ⇒ 'a" where "I = inv to_metric_completion"
have "uniformly_continuous_on (range to_metric_completion) I"
using isometry_on_uniformly_continuous[OF isometry_on_inverse(1)[OF to_metric_completion_isometry]] I_def
by auto
then have UC: "uniformly_continuous_on (range to_metric_completion) (λx. f (I x))"
using assms uniformly_continuous_on_compose
by (metis I_def bij_betw_imp_surj_on bij_betw_inv_into isometry_on_inverse(4) to_metric_completion_isometry)
obtain g where g: "uniformly_continuous_on (closure(range to_metric_completion)) g"
"⋀x. x ∈ range to_metric_completion ⟹ f (I x) = g x"
using uniformly_continuous_on_extension_on_closure[OF UC] by metis
have "uniformly_continuous_on UNIV g"
using to_metric_completion_dense' g(1) by metis
moreover have "f x = g (to_metric_completion x)" for x
using g(2) by (metis I_def UNIV_I isometry_on_inverse(2) range_eqI to_metric_completion_isometry)
moreover have "g x = f (inv to_metric_completion x)" if "x ∈ range to_metric_completion" for x
using I_def g(2) that by auto
ultimately show ?thesis unfolding comp_def by auto
qed

text ‹When the function is an isometry, the lifted function is also an isometry (and its range is
the closure of the range of the original function).
This shows that the metric completion is unique, up to isometry:›

lemma lift_to_metric_completion_isometry:
fixes f::"('a::metric_space) ⇒ ('b::complete_space)"
assumes "isometry_on UNIV f"
shows "∃g. isometry_on UNIV g
∧ range g = closure(range f)
∧ f = g o to_metric_completion
∧ (∀x ∈ range to_metric_completion. g x = f (inv to_metric_completion x))"
proof -
have *: "uniformly_continuous_on UNIV f" using assms isometry_on_uniformly_continuous by force
obtain g where g: "uniformly_continuous_on UNIV g"
"f = g o to_metric_completion"
"⋀x. x ∈ range to_metric_completion ⟹ g x = f (inv to_metric_completion x)"
using lift_to_metric_completion[OF *] by blast
have *: "isometry_on (range to_metric_completion) g"
apply (rule isometry_on_cong[OF _ g(3)], rule isometry_on_compose[of _ _ f])
using assms isometry_on_inverse[OF to_metric_completion_isometry] isometry_on_subset by (auto) (fastforce)
then have "isometry_on UNIV g"
unfolding to_metric_completion_dense'[symmetric] apply (rule isometry_on_closure)
using continuous_on_subset[OF uniformly_continuous_imp_continuous[OF g(1)]] by auto

have "g`(range to_metric_completion) ⊆ range f"
using g unfolding comp_def by auto
moreover have "g`(closure (range to_metric_completion)) ⊆ closure (g`(range to_metric_completion))"
using uniformly_continuous_imp_continuous[OF g(1)]
by (meson closed_closure closure_subset continuous_on_subset image_closure_subset top_greatest)
ultimately have "range g ⊆ closure (range f)"
unfolding to_metric_completion_dense' by (simp add: g(2) image_comp)

have "range f ⊆ range g"
using g(2) by auto
moreover have "closed (range g)"
using isometry_on_complete_image[OF ‹isometry_on UNIV g›] by (simp add: complete_eq_closed)
ultimately have "closure (range f) ⊆ range g"
then have "range g = closure (range f)"
using ‹range g ⊆ closure (range f)› by auto
then show ?thesis using ‹isometry_on UNIV g› g by metis
qed

subsection ‹The metric completion of a second countable space is second countable›

text ‹We want to show that the metric completion of a second countable space is still
second countable. This is most easily expressed using the fact that a metric
space is second countable if and only if there exists a dense countable subset. We prove
the equivalence in the next lemma, and use it then to prove that the metric completion is
still second countable.›

lemma second_countable_iff_dense_countable_subset:
"(∃B::'a::metric_space set set. countable B ∧ topological_basis B)
⟷ (∃A::'a set. countable A ∧ closure A = UNIV)"
proof
assume "∃B::'a set set. countable B ∧ topological_basis B"
then obtain B::"'a set set" where "countable B" "topological_basis B" by auto
define A where "A = (λU. SOME x. x ∈ U)`B"
have "countable A" unfolding A_def using ‹countable B› by auto
moreover have "closure A = UNIV"
fix x::'a and e::real assume "e > 0"
obtain U where "U ∈ B" "x ∈ U" "U ⊆ ball x e"
by (rule topological_basisE[OF ‹topological_basis B›, of "ball x e" x], auto simp add: ‹e > 0›)
define y where "y = (λU. SOME x. x ∈ U) U"
have "y ∈ U" unfolding y_def using ‹x ∈ U› some_in_eq by fastforce
then have "dist y x < e"
using ‹U ⊆ ball x e› by (metis dist_commute mem_ball subset_iff)
moreover have "y ∈ A" unfolding A_def y_def using ‹U ∈ B› by auto
ultimately show "∃y∈A. dist y x < e" by auto
qed
ultimately show "∃A::'a set. countable A ∧ closure A = UNIV" by auto
next
assume "∃A::'a set. countable A ∧ closure A = UNIV"
then obtain A::"'a set" where "countable A" "closure A = UNIV" by auto
define B where "B = (λ(x, (n::nat)). ball x (1/n))`(A × UNIV)"
have "countable B" unfolding B_def using ‹countable A› by auto
moreover have "topological_basis B"
proof (rule topological_basisI)
fix x::'a and U assume "x ∈ U" "open U"
then obtain e where "e > 0" "ball x e ⊆ U"
using openE by blast
obtain n::nat where "n > 2/e" using reals_Archimedean2 by auto
then have "n > 0" using ‹e > 0› not_less by fastforce
then have "1/n > 0" using zero_less_divide_iff by fastforce
then obtain y where y: "y ∈ A" "dist x y < 1/n"
by (metis ‹closure A = UNIV› UNIV_I closure_approachable dist_commute)
then have "ball y (1/n) ∈ B" unfolding B_def by auto
moreover have "x ∈ ball y (1/n)" using y(2) by (auto simp add: dist_commute)
moreover have "ball y (1/n) ⊆ U"
proof (auto)
fix z assume z: "dist y z < 1/n"
have "dist z x ≤ dist z y + dist y x" using dist_triangle by auto
also have "... < 1/n + 1/n" using z y(2) by (auto simp add: dist_commute)
also have "... < e"
using ‹n > 2/e› ‹e > 0› ‹n > 0› by (auto simp add: divide_simps mult.commute)
finally have "z ∈ ball x e" by (auto simp add: dist_commute)
then show "z ∈ U" using ‹ball x e ⊆ U› by auto
qed
ultimately show "∃V∈B. x ∈ V ∧ V ⊆ U" by metis
ultimately show "∃B::'a set set. countable B ∧ topological_basis B" by auto
qed

lemma second_countable_metric_dense_subset:
"∃A::'a::{metric_space, second_countable_topology} set. countable A ∧ closure A = UNIV"
using ex_countable_basis by (auto simp add: second_countable_iff_dense_countable_subset[symmetric])

instance metric_completion::("{metric_space, second_countable_topology}") second_countable_topology
proof
obtain A::"'a set" where "countable A" "closure A = UNIV"
using second_countable_metric_dense_subset by auto
define Ab where "Ab = to_metric_completion`A"
have "range to_metric_completion ⊆ closure Ab"
unfolding Ab_def
by (metis ‹closure A = UNIV› isometry_on_continuous[OF to_metric_completion_isometry] closed_closure closure_subset image_closure_subset)
then have "closure Ab = UNIV"
by (metis (no_types) to_metric_completion_dense'[symmetric] ‹range to_metric_completion ⊆ closure Ab› closure_closure closure_mono top.extremum_uniqueI)
moreover have "countable Ab" unfolding Ab_def using ‹countable A› by auto
ultimately have "∃Ab::'a metric_completion set. countable Ab ∧ closure Ab = UNIV"
by auto
then show "∃B::'a metric_completion set set. countable B ∧ open = generate_topology B"
using second_countable_iff_dense_countable_subset topological_basis_imp_subbasis by auto
qed

instance metric_completion::("{metric_space, second_countable_topology}") polish_space
by standard

end (*of theory Metric_Completion*)
```