English
Let α be a metric space and s ⊆ α an open set. There is a natural metric on the complete copy s that makes the boundary blow up so that Cauchy sequences stay inside s; this metric is given by dist'(x,y) = dist(x,y) + |1/dist(x, sᶜ) − 1/dist(y, sᶜ)|. Moreover, the topology induced by dist' on the complete copy is the same as the original topology on s.
Русский
Пусть α — метрическое пространство и s ⊆ α — открытое множество. На полном копировании s существует естественная метрика, которая «выплескивает» поведение на границе так, чтобы последовательности Коши оставались внутри s; метрика задаётся как dist'(x,y) = dist(x,y) + |1/dist(x, sᶜ) − 1/dist(y, sᶜ)|. Более того, топология, индуцированная dist' на CompleteCopy s, совпадает с исходной топологией на s.
LaTeX
$$$\exists d' : (s^\mathrm{CompleteCopy})^2 \to \mathbb{R}_{\ge 0},
\quad d'(x,y) = d(x,y) + \left| \dfrac{1}{\operatorname{dist}(x, s^c)} - \dfrac{1}{\operatorname{dist}(y, s^c)} \right| \\ && \wedge \, \mathcal{T}_{d'} = \mathcal{T}_{\text{orig}}|_{s^\mathrm{CompleteCopy}}$$$
Lean4
/-- A metric space structure on a subset `s` of a metric space, designed to make it complete
if `s` is open. It is given by `dist' x y = dist x y + |1 / dist x sᶜ - 1 / dist y sᶜ|`, where the
second term blows up close to the boundary to ensure that Cauchy sequences for `dist'` remain well
inside `s`.
This definition ensures the `TopologicalSpace` structure on
`TopologicalSpace.Opens.CompleteCopy s` is definitionally equal to the original one.
-/
instance instMetricSpace : MetricSpace (CompleteCopy s) :=
by
refine
@MetricSpace.ofT0PseudoMetricSpace (CompleteCopy s)
(.ofDistTopology dist (fun _ ↦ ?_) (fun _ _ ↦ ?_) (fun x y z ↦ ?_) fun t ↦ ?_) _
· simp only [dist_eq, dist_self, one_div, sub_self, abs_zero, add_zero]
· simp only [dist_eq, dist_comm, abs_sub_comm]
·
calc
dist x z = dist x.1 z.1 + |1 / infDist x.1 sᶜ - 1 / infDist z.1 sᶜ| := rfl
_ ≤
dist x.1 y.1 + dist y.1 z.1 +
(|1 / infDist x.1 sᶜ - 1 / infDist y.1 sᶜ| + |1 / infDist y.1 sᶜ - 1 / infDist z.1 sᶜ|) :=
(add_le_add (dist_triangle _ _ _) (dist_triangle (1 / infDist _ _) _ _))
_ = dist x y + dist y z := add_add_add_comm ..
· refine ⟨fun h x hx ↦ ?_, fun h ↦ isOpen_iff_mem_nhds.2 fun x hx ↦ ?_⟩
· rcases (Metric.isOpen_iff (α := s)).1 h x hx with ⟨ε, ε0, hε⟩
exact ⟨ε, ε0, fun y hy ↦ hε <| (dist_comm _ _).trans_lt <| (dist_val_le_dist _ _).trans_lt hy⟩
· rcases h x hx with ⟨ε, ε0, hε⟩
simp only [dist_eq, one_div] at hε
have :
Tendsto (fun y : s ↦ dist x.1 y.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist y.1 sᶜ)⁻¹|) (𝓝 x)
(𝓝 (dist x.1 x.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist x.1 sᶜ)⁻¹|)) :=
by
refine (tendsto_const_nhds.dist continuous_subtype_val.continuousAt).add (tendsto_const_nhds.sub <| ?_).abs
refine (continuousAt_inv_infDist_pt ?_).comp continuous_subtype_val.continuousAt
rw [s.isOpen.isClosed_compl.closure_eq, mem_compl_iff, not_not]
exact x.2
simp only [dist_self, sub_self, abs_zero, zero_add] at this
exact mem_of_superset (this <| gt_mem_nhds ε0) hε
